Proof-Theoretic Validity and Inquisitive Logic, The Journal of Philosophical Logic (preprint)
Gentzen famously suggested that the laws of logic could be shown to be analytic if the rules for introducing logical connectives provide the meaning of said connectives. Proof-theoretic validity, first proposed by Prawitz, is a formal explication of what it means to give the introduction rules this privileged status. In its original formulation, Prawitz conjectured that the logic justified by proof-theoretic validity would be intuitionistic—a logic that formalises the ideas of constructive mathematics. Piecha and Schröder-Heister disproved this. This raises the question of what logics are justified by proof-theoretic validity. I have shown that the logic of proof-theoretic validity is a generalised version of inquisitive logic (“Proof-Theoretic Validity and Inquisitive Logic” Journal of Philosophical Logic, forthcoming). Inquisitive logic is a formalism designed to offer a unified treatment of questions and assertions and has several properties that might worry the advocate of proof-theoretic validity, as it is an intermediate logic not closed under substitution. However, careful examination of the proof of this result shows that it follows from the treatment of the atomic formulas, not the logical connectives, and there are plausible modifications of the treatment of the atomic formulas that can remedy this (“In Defence of Proof-Theoretic Validity” in preparation).
Frege’s Theorem and Potential Infinities
The great promise of logicism is that, via a result called Frege’s Theorem, the truths of arithmetic may be reduced to definitions, the rules of logic, and Hume’s Principle, a principle that says that two concepts have the same number if and only if there is a bijection between them. Logicists claim our concept of number makes Hume’s Principle analytic. However, a major objection to logicism is that if Hume’s Principle is analytic, then it is an analytic truth that there are infinitely many objects. Building on recent interest in potential infinities in the foundations of mathematics (such as in the work of Linnebo), I have shown that first-order arithmetic is reducible to Hume’s Principle in a modal theory representing potential infinities, but the stronger arithmetic theory that Frege’s Theorem usually treats is not (“The Potential in Frege’s Theorem” Review of Symbolic Logic, forthcoming). The assumption of a potential infinity of objects is far more circumspect than the assumption of an actual infinity. In other words, the logicist can avoid the commitment to an actual infinity, but at the cost of only claiming elementary arithmetic to be analytic on that basis.
Property Theory with Currying Types and Formal Semantics
My third project documents difficulties with using Property Theory with Currying Types (PTCT) to explicate meaning-as-use. PTCT, as proposed by Fox and Lappin (2008), takes the untyped lambda calculus and adds types. The untyped lambda calculus is intended to formalise a notion of generalised computation which does not rule out functions being applied to themselves: one can think of it as a “naïve” notion of procedures. I argue that its use as a formal semantics is vitiated by its Turing completeness: for, PTCT can represent every computable function. By Rice’s theorem there will be no computable procedure for deciding when two terms in PTCT are identical, and so there will be no uniform way to decide when two meanings are the same. A further effect of Rice’s theorem is that we cannot, in general, have a decidable procedure to find if a term is a member of a type. As types give us our grammatical categories, this means we have no general way to decide if a term is e.g. a noun or not. Syntactic matters, such as grammatical category, are thus not decidable in this formalism, which is an undesirable result.
Genus as a Complexity Measure for Proofs
Traditional measures of proof complexity use measures of length. However, these measures have been claimed to be inadequate for several reasons—for example, such measures do not account for how difficult proofs are to find. Carbone (2009) claims that the genus of a proof graph is an alternative geometric measure of discovermental complexity which overcomes some of these difficulties. I have, in collaboration with Andrew Arana (Lorrain), evaluated Carbone’s method. We argue that Carbone’s proposed method for evaluating the degree of complexity of a proof is only a measure of the proof’s structural complexity, that is it measures the complexity of the structural rules such as cut but not the rules for the logical connectives (“Genus as a Measure of Discovermental Complexity” in preparation).