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: 93,296

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

Normalization proof for Peano Arithmetic.Annika Siders - 2015 - Archive for Mathematical Logic 54 (7-8):921-940.
Gentzen’s consistency proof without heightlines.Annika Siders - 2013 - Archive for Mathematical Logic 52 (3-4):449-468.
Strong Normalization via Natural Ordinal.Daniel Durante Pereira Alves - 1999 - Dissertation,
Gentzen's proof systems: byproducts in a work of genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
Harmony in Multiple-Conclusion Natural-Deduction.Nissim Francez - 2014 - Logica Universalis 8 (2):215-259.
An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs.Paolo Mancosu, Sergio Galvan & Richard Zach - 2021 - Oxford: Oxford University Press. Edited by Sergio Galvan & Richard Zach.
A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević - 2006 - Archive for Mathematical Logic 45 (2):113-148.
Commentary and Illocutionary Expressions in Linear Calculi of Natural Deduction.Moritz Cordes & Friedrich Reinmuth - 2017 - Logic and Logical Philosophy 26 (2).
Decoding Gentzen's Notation.Luca Bellotti - 2018 - History and Philosophy of Logic 39 (3):270-288.
Normal derivability in classical natural deduction.Jan Von Plato & Annika Siders - 2012 - Review of Symbolic Logic 5 (2):205-211.

Analytics

Added to PP
2013-12-01

Downloads
9 (#1,281,906)

6 months
39 (#100,216)

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.
A Mathematical Model of Quantum Computer by Both Arithmetic and Set Theory.Vasil Penchev - 2020 - Information Theory and Research eJournal 1 (15):1-13.
The Quantum Strategy of Completeness: On the Self-Foundation of Mathematics.Vasil Penchev - 2020 - Cultural Anthropology eJournal (Elsevier: SSRN) 5 (136):1-12.

View all 9 citations / 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