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
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: 69,043
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

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.

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.
Gentzen’s Consistency Proof Without Heightlines.Annika Siders - 2013 - Archive for Mathematical Logic 52 (3-4):449-468.
Normalization Proof for Peano Arithmetic.Annika Siders - 2015 - Archive for Mathematical Logic 54 (7-8):921-940.

Add more citations

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.
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.
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 )

How can I increase my downloads?

Downloads

My notes