Stephen Mackereth

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.

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.

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). In this paper, we offer a more fine-grained analysis of the logical strength of HP, measured by deductive implications rather than interpretability. Our main result is that HP is not deductively conservative over SOL + DI. That is, SOL + HP proves additional theorems in the language of pure second-order logic that are not provable from SOL + DI alone. Arguably, then, HP is not just a pure axiom of infinity, but rather it carries additional logical content. On the other hand, we show that HP is \(\Pi ^1_1\) conservative over SOL + DI, and that HP is conservative over SOL + DI + “the universe is well ordered” (WO). Next, we show that SOL + HP does not prove any of the simplest and most natural versions of the axiom of choice, including WO and weaker principles. Lastly, we discuss other axioms of infinity. We show that HP does not prove the Splitting or Pairing principles (axioms of infinity stronger than DI).

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.

Neo-Fregean logicists claim that Hume’s Principle (HP) may be taken as an implicit definition of cardinal number, true simply by fiat. A long-standing problem for neo-Fregean logicism is that HP is not deductively conservative over pure axiomatic 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.