Gödel intended his Dialectica interpretation to provide a foundational 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. He sketched a defense of this claim in a page-long footnote, which however has left readers baffled. In this talk, I will explain Gödel’s footnote and show that there really is no circularity here. Thus, Gödel has achieved a significant foundational reduction. The foundations of T turn out to be stranger than meets the eye; they utilize a (broadly) Leibnizian notion of analyticity in a surprising way.