Please do not distribute the work found here. Click the relevant title to access the PDF.
The Potential in Frege’s Theorem (Published Review of Symbolic Logic)
Abstract: Is a logicist bound to the claim that as a matter of analytic truth there is an actual infinity of objects? If Hume’s Principle is analytic then in the standard setting the answer appears to be yes. Hodes’s work pointed to a way out by offering a modal picture in which only a potential infinity was posited. However, this project was abandoned due to apparent failures of cross-world predication. We re-explore this idea and discover that in the setting of the potential infinite one can interpret first-order Peano arithmetic, but not second-order Peano arithmetic. We conclude that in order for the logicist to weaken the metaphysically loaded claim of necessary actual infinities, they must also weaken the mathematics they recover.
Proof-Theoretic Validity and Inquisitive Logic (Published Journal of Philosophical Logic)
Abstract: Prawitz (1971) conjectured that proof-theoretic validity offers a semantics for intuitionistic logic. This conjecture has recently been proven false by Piecha and Schroeder-Heister (2019). This article resolves one of the questions left open by this recent result by showing the extensional alignment of proof-theoretic validity and general inquisitive logic. General inquisitive logic is a generalisation of inquisitive semantics, a uniform semantics for questions and assertions. The paper further defines a notion of quasi-proof-theoretic validity by restricting proof-theoretic validity to allow double negation elimination for atomic formulas and proves the extensional alignment of quasi-proof-theoretic validity and inquisitive logic.
Decidability in Proof-Theoretic Validity (Published Logica Yearbook 2021 [Peer Reviewed])
Abstract: Proof-theoretic validity has proven a useful tool for proof-theoretic semantics, as it explains the harmony found in the introduction and elimination rules for the intuitionistic calculus. However, the demonstration that a rule of proof is proof-theoretically valid requires checking an infinity of cases. This raises the question of whether proof-theoretic validity is decidable. It is proven here that it is for the formulations most prominent in the literature.
Generalised Proof-Theoretic Validity (Minor Revisions Analysis)
Abstract: Prawitz conjectured that proof-theoretic validity is complete for intuitionistic logic. Recent work on proof-theoretic validity has resulted in a demonstration that most varieties are not. In fact, most known systems are not even closed under substitution. In this paper, we make a minor modification to the definition of proof-theoretic validity found in Prawitz (1973) and refined by Schroeder-Heister. We will call the new notion ‘generalised proof-theoretic validity’ and we will show that it is in fact complete for intuitionistic logic.
Proof-Theoretic Validity and Prawitz’s Conjecture (Under review Australasian Journal of Philosophy)
Abstract: Several recent results bring into focus the superintuitionistic nature of most notions of proof-theoretic validity, but little work has been done evaluating the consequences of these results. Proof-theoretic validity claims to offer a formal explication of how inferences follow from the definitions of logic connectives (which are defined by their introduction rules). This paper explores whether the new results undermine this claim. It is argued that, while the formal results are worrying, superintuitionistic inferences are valid because the treatments of atomic formulas are insufficiently general, and a resolution to this issue is proposed.
Proof-Theoretic Validity and Analyticity (Under review Erkenntnis)
Abstract: Proof-theoretic semantics is intended to demonstrate that logic is self-justifying. While the naıve approach to proof-theoretic semantics offers a prima facie attractive explanation of the analyticity of logic, it is inconsistent. Attempts to fix this by requiring proof rules in definitions to be harmonious either fail or are ad hoc. This leaves proof-theoretic validity which requires proof rules to be reducible to the rules that introduce terms. This paper considers three explanations of why reduction to introduction rules justifies proof rules, by Dummett and Prawitz. In each case the role of reduction in the justification of proof rules is inadequate. It is concluded that there is not currently an explanation of how proof-theoretic semantics justifies logic. Finally, we note that the prospects of justifying type theory are better, as it allows relations between proofs to be included in definitions.
The Untyped λ-Calculus as a Foundation for Natural Language Semantics
Abstract: Natural language contains hyperintensional settings, but it is difficult to formalise hyperintensionality using Montague’s approach to formal semantics. Fox and Lappin (2005) have proposed Property Theory with Curry Types (PTCT) as an alternative foundation for natural language. They claim that PTCT formalises hyperintensionality and polymorphism but is a computationally weaker system than the traditional Montague grammars. In this paper, we dispute their claim to have generated a computationally weaker system. Firstly, their argument is based on Montague grammars being second-order and PTCT a first-order. Only second-order systems with full semantics are stronger than first-order systems. So Montague grammars are of equivalent strength to PTCT if they use a weaker semantics. Secondly, PTCT uses the untyped λ-calculus while Montague grammars uses the typed λ-calculi. The untyped calculus is Turing complete, while the typed systems are not. From this point of view, we see that PTCT is the stronger formal system.
Genus as a Measure of Discovermental Complexity (Under review Synthese)
Abstract: An account of mathematical understanding should account for the differences between theorems whose proofs are “easy” to discover, and those whose proofs are difficult to discover. Though Hilbert seems to have created proof theory with the idea that it would address this kind of “discovermental complexity”, much more attention has been paid to the lengths of proofs, a measure of the difficulty of verifying of a given formal object that it is a proof of a given formula in a given formal system. In this paper we will shift attention back to discovermental complexity, by addressing a “topological” measure of proof complexity recently highlighted by Alessandra Carbone (2009). Though we will contend that Carbone’s measure fails as a measure of discovermental complexity, it forefronts numerous important formal and epistemological issues that we will discuss, including the structure of proofs and the question of whether impure proofs are systematically simpler than pure proofs.