Research

Hilbert’s Program in the 1920s aimed to give finitary consistency proofs for infinitary mathematics, thus putting infinitary mathematics on a more secure footing. There is a popular narrative that Hilbert’s Program was decisively refuted by Gödel’s incompleteness theorems in 1931. However, Gödel himself, in a remarkable paper of 1958, pursues a modified version of Hilbert’s Program: he presents his Dialectica interpretation as a new, Hilbert-style consistency proof for arithmetic based on “an extension of the finitary standpoint,” and he clearly regards this proof as epistemologically significant. In this essay, I explain and assess the epistemological project that Gödel sets out in his Dialectica paper. Ultimately, I argue that the Dialectica interpretation is best understood, not as a consistency proof, but as a way of assigning a constructive meaning to arithmetic.    Preprint

Neologicists have claimed that Hume's Principle (HP) may be taken as a stipulative definition of cardinal number. This claim is threatened by the fact that HP is not conservative over pure second-order logic. I argue that the dominant neologicist response to the conservativeness objection is not satisfactory. Then I propose a novel version of neologicism, based on Heck's Two-sorted Hume's Principle (2HP), which does meet the conservativeness objection—provided that conservativeness is understood semantically and not deductively. I also argue that on my proposal, the Bad Company problem is solved by conservativeness.

It has long been known that in the context of axiomatic second-order logic (SOL), Hume's Principle (HP) is mutually interpretable with "the universe is Dedekind infinite" (DI). I offer a more fine-grained analysis of the logical strength of HP, measured by deductive implications rather than interpretability. The main result is that HP is not deductively conservative over SOL + DI.  Arguably, then, HP is not just a pure axiom of infinity but rather carries additional logical content. Next, I establish some limits to the non-conservativeness of HP.  Lastly, I show that SOL + HP does not prove any of the simplest and most natural forms of the axiom of choice, nor any natural axioms of infinity stronger than DI.    Preprint.  Image credit: xkcd

Online resource

Neologicists claim that Hume's Principle (HP) may be taken as an implicit, stipulative definition of cardinal number, true simply by fiat. However, HP is not deductively conservative over pure second-order logic. This seems to preclude HP from being true by fiat. In this paper, we study Richard Kimberly Heck's Two-sorted Frege Arithmetic (2FA), a variation on HP which has been thought to be deductively conservative over second-order logic. We show that it isn't. In fact, 2FA is not conservative over $n$-th order logic, for all $n \geq 2$. It follows that in the usual one-sorted setting, HP is not deductively Field-conservative over second- or higher-order logic.    Published in Open Access

We show that any coherent complete partial order (ccpo) is obtainable as the fixed-point poset of the strong Kleene jump of a suitably chosen first-order ground model. This is a strengthening of Visser's result that any finite ccpo is obtainable in this way. The same is true for the van Fraassen supervaluation jump, but not for the weak Kleene jump.    Preprint

Gödel intended his Dialectica translation to provide a reduction of first-order arithmetic to a quantifier-free theory T.  It has widely been objected, however, that this theory T tacitly presupposes the very quantificational logic that Gödel was trying to eliminate, hidden within its complicated definition of "computable function of finite type." This would render the translation philosophically circular. Gödel was adamant that there was no circularity here, but so far an explicit analysis has been wanting. I vindicate Gödel, showing that there is no circularity and answering a longstanding exegetical question in Gödel scholarship. The foundations of Gödel's theory T are much stranger than meets the eye; they utilize a Leibnizian notion of analyticity in a surprising way.