Kennedy develops formalism freeness and logical entanglement to study the relation between informal mathematical contents and the formalisms that attempt to capture them, suggesting that these notions can lay down a road to content. I reconstruct Kennedy's outlook and argue that whether logical entanglement signals a breakdown in the adequacy of formalisms depends in part on the role of formalization. I then use a language-first perspective to clarify this dependence, vindicate Kennedy's claim that some mathematics must be done in informal language, and show how her notions can contribute to an account of content.
Abstract In 1936 Gentzen gave a proof of the consistency of Peano Arithmetic. While its validity is not in doubt, this paper asks whether it is a proof in the epistemic sense — an argument that can generate or enhance justification for its conclusion. Gentzen claimed it was a ‘real vindication’ of arithmetic, while many later critics judged it circular or inert. I argue that the truth lies in between: the proof is non-trivial, yet falls short of a real vindication of the consistency of arithmetic. Along the way, I provide a framework for assessing the epistemic status of consistency proofs.
Abstract 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 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.
