Gödel's Footnote

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.