Constructive Sequent Reduction in Gentzen’s First Consistency Proof for Arithmetic

  • Maurizio Negri
Part of the Boston Studies in the Philosophy of Science book series (BSPS, volume 47)


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.


Natural Number Reduced Form Free Variable Reduction Step Ordinal Number 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Bernays, P. (1970), ‘On the originals Gentzen consistency proof’, in Intuitionism and Proof Theory. Amsterdam, North-Holland. pp. 409–17.Google Scholar
  2. Gentzen, G. (1969), Collected Papers, ed. by M.E. Szabo. Amsterdam, North Holland.Google Scholar
  3. Kreisel, G. (1971), ‘Book review of Gentzen’s Collected Papers,’ Journal of Philosophy, 68, 238–65.CrossRefGoogle Scholar
  4. Kreisel, G. (1976), ‘Wie die Beweistheorie zu ihren Ordinalzahlen kam und kommt’, Jahresbericht der Deutschen Mathematiker-Vereinigung 78, 177–223.Google Scholar
  5. Tait,W.W. (1961), ‘Nested recursion,’ Mathematische Annalen 143, 236–50.CrossRefGoogle Scholar
  6. Tait, W.W. (1965), ‘Functional defined by transfinite recursion’, Journal of Symbolic Logic 30, 155–192.CrossRefGoogle Scholar

Copyright information

© D. Reidel Publishing Company 1980

Authors and Affiliations

  • Maurizio Negri

There are no affiliations available

Personalised recommendations