Published Work
The Potential in Frege’s Theorem, The Review of Symbolic Logic (publisher, preprint)
Proof-Theoretic Validity and Inquisitive Logic, The Journal of Philosophical Logic, 50, 1199–1229 (2021). (publisher, preprint)
Find me
PhilPeople—ORCID—arXiv—Academia.edu
Projects
Proof-Theoretic Validity
The logic of proof-theoretic validity
What is proof-theoretic validity? Prawitz proposed proof-theoretic validity in the 1970s as an explication of Gentzen’s claim logic follows from the rules that introduction terms. Prawitz (1973) conjectured that intuitionistic logic was the unique strongest proof-theoretically valid logic (PTV). But it took till 2019 for Piecha and Schroeder-Heister to show that this was false. Building on this work I demonstrated that the strongest PTV logic for Prawitz’s 1973 definition is the extension of intuitionistic logic called generalised inquisitive logic (“Proof-Theoretic Validity and Inquisitive Logic” Journal of Philosophical Logic, 2021). I have also shown when PTV is decidable (“It’s a small world after all; decidability of proof-theoretic validity”, in preparation; awarded Otto Shalar scholarship for completion).
Fixing proof-theoretic validity. The failure of Prawitz’s conjecture undermines the philosophical defence of constructive logic that Prawitz (1980) and Dummett (1991) have offered. However, I have shown that a modification of Prawitz’s definition results in a generalised notion of proof-theoretic validity which is complete for intuitionistic logic (“Generalised Proof-Theoretic Validity for Intuitionistic Logic”, manuscript). And there are good reasons to prefer this definition (“Proof-Theoretic Validity and Prawitz’s Conjecture”, manuscript; awarded the Werner Fellowship for completion). This demonstrates that intuitionistic logic is privileged with regards to proof-theoretic validity when understood more generally.
Analyticity and proof-theoretic validity. This developed understanding of PTV’s relation to logic allows for an assessment of whether it shows logic is analytic. Both Dummett (1991) and Prawitz (1973, 2014) have offered arguments in favour of this conclusion. I ultimately find these arguments unacceptable (“Reducing an assumption; proof-theoretic semantics and analyticity”, manuscript). However, Prawitz’s justifications can be used to develop a defence of type theory.
Martin-Löf type theory (MLTT). Constructive type theories differ from standard logics by being annotated by terms that can be thought of as standing for names of proofs. Martin-Löf type theory is a variety that has been very influential in computer science and parts of mathematics and philosophy. For example, it forms the basis of Homotopy type theory which is being defended as a new foundation for mathematics (Voevodsky 2014, HoTT Book 2013). I have draft chapters with Sean Walsh (UCLA) of a book introducing philosophers to the philosophical and technical aspects of MLTT.
Proof-theoretic semantics for mathematics
Can a proof-theoretic semantics for mathematics be offered? Proof-theoretic semantics for mathematics faces more difficulties than for logic. This is because mathematical theories often cannot be given by the well-behaved harmonious inference rules required for proof-theoretic semantics. An example of this can be found with arithmetic (the lower bar logicism passed). The difficulty is caused by the axiom for mathematical induction, which is not well behaved, or harmonious, as Steinberger (2011) has argued.
Arithmetic in type theory. I intend to investigate whether the problem with arithmetic can be side-stepped by looking at typed rather than untyped mathematical theories. There are good reasons to think that typed theories like Martin-Löf Type Theory are more in the spirit of proof-theoretical semantics than their untyped counterparts. So, investigating whether proof-theoretic semantics for arithmetic is possible for typed theories will offer the best opportunity to give a proper evaluation of this. Part of this project will also assess Tennant’s (1989) alternative approach which marries PTS and logicism.
Future work on this topic would look at extensions to constructive set theory and other more powerful mathematical theories and examine whether the weak constructive logics can be traded for classical logic and so the full power of the mathematical theories more commonly used.
Proof-theoretic semantics for truth
The problem for deflationism. Deflationism holds that truth is a logical notion. But it is hard to substantiate what this involves. Proof-theoretic semantics offers a compelling picture of how a notion can be logical in terms of having well-behaved rules. There has not yet been a proof-theoretic semantics for truth offered in the constructive tradition. There are several barriers to this stemming from the well-known difficulties with formalising truth.
Proof-theoretic deflationism. I propose to offer a proof-theoretic semantics for truth. This will require also producing work on formal theories of truth in intuitionistic logic and its extensions, intermediate logics. The capstone of this project would be an assessment of whether proof-theoretic semantics can offer a good foundation for making sense of deflationism about truth. I have received a Marie Curie fellowship at Bristol for this project from 2022-24.
Other work:
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).