Consistency of Heyting arithmetic in natural deduction

Mathematical Logic Quarterly 56 (6):611-624 (2010)
  Copy   BIBTEX

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.

Categories

Keywords

Reprint years

DOI

10.1002/malq.200910118

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

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.
"True" arithmetic can prove its own consistency.Andrew Boucher -
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
2013-12-01

Downloads
34 (#458,553)

6 months
6 (#504,917)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

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

References found in this work

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.
For Oiva Ketonen's 85th birthday.Sara Negri & Jan von Plato - 1998 - Bulletin of Symbolic Logic 4 (4):418-435.

View all 7 references / Add more references