Logic Journal of the IGPL 12 (6):549-560 (2004)

María Fernanda Pallares
Universidad de la Republica Oriental del Uruguay
In the antology of Gentzen's works made by M.E.Szabo and published in 1969, we find out in an appendix, some passages presented by Bernays to the editor. These texts belong to a first proof of Peano's Arithmetic consistency that Gentzen had not published. In a different way from the other proofs of consistency made by Gentzen and already known in the thirties, this proof does not use the procedure of transfinite induction up to ε0. On the contrary, it is based on the definition of a reduction process for sequents that is systematically associated to every derivable sequent allowing us to recognize it as a true sequent. We make some variations of the technique used in the classic version and employ them to the intuitionistic case. This proof is interesting because it is related with other results such as completeness proofs and cut-elimination theorems.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1093/jigpal/12.6.549
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 51,668
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Gentzen’s Consistency Proof Without Heightlines.Annika Siders - 2013 - Archive for Mathematical Logic 52 (3-4):449-468.
Gentzen's Proof Systems: Byproducts in a Work of Genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
A Cut-Elimination Proof in Intuitionistic Predicate Logic.Mirjana Borisavljević - 1999 - Annals of Pure and Applied Logic 99 (1-3):105-136.
Consistency Proof Via Pointwise Induction.Toshiyasu Arai - 1998 - Archive for Mathematical Logic 37 (3):149-165.
Proof Theory for Admissible Rules.Rosalie Iemhoff & George Metcalfe - 2009 - Annals of Pure and Applied Logic 159 (1-2):171-186.
Intuitionistic Socratic Procedures.Tomasz F. Skura - 2005 - Journal of Applied Non-Classical Logics 15 (4):453-464.
On the Original Gentzen Consistency Proof for Number Theory.Manfred Szabo - 1970 - In A. Kino, John Myhill & Richard Eugene Vesley (eds.), Intuitionism and Proof Theory. Amsterdam: North-Holland Pub. Co.. pp. 409.
A Simple Proof That Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
A Survey of Nonstandard Sequent Calculi.Andrzej Indrzejczak - 2014 - Studia Logica 102 (6):1295-1322.


Added to PP index

Total views
2 ( #1,333,317 of 2,331,429 )

Recent downloads (6 months)
1 ( #588,490 of 2,331,429 )

How can I increase my downloads?


My notes