Mathematical Logic Quarterly 56 (6):611-624 (2010)
| Authors | |
| Abstract |
A proof of the consistency of Heyting arithmetic formulated in natural deduction is given. The proof is a reduction procedure for derivations of falsity and a vector assignment, such that each reduction reduces the vector. By an interpretation of the expressions of the vectors as ordinals each derivation of falsity is assigned an ordinal less than ε 0, thus proving termination of the procedure.
|
| Keywords | Heyting arithmetic natural deduction Consistenc |
| Categories | (categorize this paper) |
| DOI | 10.1002/malq.200910118 |
| Options |
Mark as duplicate
Export citation
Request removal from index
|
Download options
References found in this work BETA
Die Widerspruchsfreiheit der Reinen Zahlentheorie.Gerhard Gentzen - 1936 - Journal of Symbolic Logic 1 (2):75-75.
Cut Elimination in the Presence of Axioms.Sara Negri & Jan Von Plato - 1998 - Bulletin of Symbolic Logic 4 (4):418-435.
Beweisbarkeit Und Unbeweisbarkeit von Anfangsfallen der Transfiniten Induktion in der Reinen Zahlentheorie.Gerhard Gentzen - 1944 - Journal of Symbolic Logic 9 (3):70-72.
Neue Fassung des Widerspruchsfreiheitsbeweises Für Die Reine Zahlentheorie. [REVIEW]Rózsa Péter - 1939 - Journal of Symbolic Logic 4 (1):31-32.
Der erste Widerspruchsfreiheitsbeweis für die klassische Zahlentheorie.Gerhard Gentzen - 1974 - Archive for Mathematical Logic 16 (3-4):97-118.
View all 6 references / Add more references
Citations of this work BETA
Gentzen's Proof Systems: Byproducts in a Work of Genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
Fermat’s Last Theorem Proved in Hilbert Arithmetic. I. From the Proof by Induction to the Viewpoint of Hilbert Arithmetic.Vasil Penchev - 2021 - Logic and Philosophy of Mathematics eJournal (Elsevier: SSRN) 13 (7):1-57.
Gentzen’s Consistency Proof Without Heightlines.Annika Siders - 2013 - Archive for Mathematical Logic 52 (3-4):449-468.
Constructivity and Computability in Historical and Philosophical Perspective.Jacques Dubucs & Michel Bourdeau (eds.) - 2014 - Dordrecht, Netherland: Springer.
Normalization Proof for Peano Arithmetic.Annika Siders - 2015 - Archive for Mathematical Logic 54 (7-8):921-940.
Similar books and articles
On the Structure of Kripke Models of Heyting Arithmetic.Zoran Marković - 1993 - Mathematical Logic Quarterly 39 (1):531-538.
Closed Fragments of Provability Logics of Constructive Theories.Albert Visser - 2008 - Journal of Symbolic Logic 73 (3):1081-1096.
Gentzen’s Consistency Proof Without Heightlines.Annika Siders - 2013 - Archive for Mathematical Logic 52 (3-4):449-468.
Classical and Intuitionistic Models of Arithmetic.Kai F. Wehmeier - 1996 - Notre Dame Journal of Formal Logic 37 (3):452-461.
A Natural First-Order System of Arithmetic Which Proves Its Own Consistency.Andrew Boucher - manuscript
Intermediate Logics and the de Jongh Property.Dick de Jongh, Rineke Verbrugge & Albert Visser - 2011 - Archive for Mathematical Logic 50 (1-2):197-213.
A Brief History of Natural Deduction.Francis Jeffry Pelletier - 1999 - History and Philosophy of Logic 20 (1):1-31.
Gentzen's Proof Systems: Byproducts in a Work of Genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
Optimal Natural Dualities for Varieties of Heyting Algebras.B. A. Davey & H. A. Priestley - 1996 - Studia Logica 56 (1-2):67 - 96.
Provably Recursive Functions of Constructive and Relatively Constructive Theories.Morteza Moniri - 2010 - Archive for Mathematical Logic 49 (3):291-300.
Sequent Calculus in Natural Deduction Style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.
Finite Sets and Natural Numbers in Intuitionistic TT.Daniel Dzierzgowski - 1996 - Notre Dame Journal of Formal Logic 37 (4):585-601.
Analytics
Added to PP index
2013-12-01
Total views
23 ( #489,937 of 2,498,579 )
Recent downloads (6 months)
1 ( #426,098 of 2,498,579 )
2013-12-01
Total views
23 ( #489,937 of 2,498,579 )
Recent downloads (6 months)
1 ( #426,098 of 2,498,579 )
How can I increase my downloads?
Downloads
