Constructive Sequent Reduction in Gentzen’s First Consistency Proof for Arithmetic
The purpose of this paper is to discuss Gentzen’s first consistency proof for arithmetic, the ‘galley proof’ (published for the first time in the Collected Papers, Amsterdam, 1969), by analyzing its methods of proof. Opposing positions on this subject have been taken by Bernays (1970) and Kreisel (1971). According to Kreisel’s analysis, which uses a result of Tait, it turns out that the ‘galley proof’ does not involve methods of proof exceeding transfinite induction up to ε0.
Unable to display preview. Download preview PDF.
- Bernays, P. (1970), ‘On the originals Gentzen consistency proof’, in Intuitionism and Proof Theory. Amsterdam, North-Holland. pp. 409–17.Google Scholar
- Gentzen, G. (1969), Collected Papers, ed. by M.E. Szabo. Amsterdam, North Holland.Google Scholar
- Kreisel, G. (1976), ‘Wie die Beweistheorie zu ihren Ordinalzahlen kam und kommt’, Jahresbericht der Deutschen Mathematiker-Vereinigung 78, 177–223.Google Scholar