Gentzen’s 1935 Consistency Proof and the Interpretation of its Implication

In this paper, I will argue from a historical perspective that Gentzen’s 1935 consistency proof of 1st order Peano Arithmetic PA principally aimed to give a finitist interpretation of implication and this aspect of the 1935 proof emerged as the attempt to cope with the non-finiteness in BHK-interpretation of implication. My argument consists of two parts. First, I will explain that the fundamental idea of the 1935 proof is to show the soundness of PA on some finitist interpretation and Gentzen had attempted to use BHK-interpretation as such an interpretation. It is claimed that he eventually thought that there is a ‘circularity’ which is due to the non-finiteness of BHK-interpretation of implication, so it cannot be used as a finitist interpretation. Secondly, I will argue that the principal aim of the 1935 proof is to give his own finitist interpretation of implication which avoids such a ‘circularity’. Finally, this paper’s conclusion and an open question are presented.
Keywords Conference Proceedings  Contemporary Philosophy
Categories (categorize this paper)
ISBN(s) 978-1-63435-038-9
DOI 10.5840/wcp232018551191
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 49,066
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

Decoding Gentzen's Notation.Luca Bellotti - 2018 - History and Philosophy of Logic 39 (3):270-288.
Consistency, Models, and Soundness.Matthias Schirn - 2010 - Axiomathes 20 (2-3):153-207.
A Dynamic Characterization of the Pure Logic of Relevant Implication.Diderik Batens - 2001 - Journal of Philosophical Logic 30 (3):267-280.
Gentzen’s Consistency Proof Without Heightlines.Annika Siders - 2013 - Archive for Mathematical Logic 52 (3-4):449-468.
Unifying Functional Interpretations.Paulo Oliva - 2006 - Notre Dame Journal of Formal Logic 47 (2):263-290.
Surveyability and Mathematical Certainty.Kai Büttner - 2017 - Axiomathes 27 (1):113-128.


Added to PP index

Total views

Recent downloads (6 months)

How can I increase my downloads?


Sorry, there are not enough data points to plot this chart.

My notes

Sign in to use this feature