Consistency proof via pointwise induction

Archive for Mathematical Logic 37 (3):149-165 (1998)


We show that the consistency of the first order arithmetic $PA$ follows from the pointwise induction up to the Howard ordinal. Our proof differs from U. Schmerl [Sc]: We do not need Girard's Hierarchy Comparison Theorem. A modification on the ordinal assignment to proofs by Gentzen and Takeuti [T] is made so that one step reduction on proofs exactly corresponds to the stepping down $\alpha\mapsto\alpha [1]$ in ordinals. Also a generalization to theories $ID_q$ of finitely iterated inductive definitions is proved

Download options


    Upload a copy of this work     Papers currently archived: 72,805

External links

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

Through your library


Added to PP

20 (#563,435)

6 months
1 (#386,499)

Historical graph of downloads
How can I increase my downloads?

References found in this work

A New System of Proof-Theoretic Ordinal Functions.W. Buchholz - 1986 - Annals of Pure and Applied Logic 32:195-207.

Add more references

Similar books and articles

Pointwise Hereditary Majorization and Some Applications.Ulrich Kohlenbach - 1992 - Archive for Mathematical Logic 31 (4):227-241.
Gentzen’s Consistency Proof Without Heightlines.Annika Siders - 2013 - Archive for Mathematical Logic 52 (3-4):449-468.
Ordinal Diagrams for Recursively Mahlo Universes.Toshiyasu Arai - 2000 - Archive for Mathematical Logic 39 (5):353-391.
Consistency, Models, and Soundness.Matthias Schirn - 2010 - Axiomathes 20 (2-3):153-207.
Propositional Proof Systems and Fast Consistency Provers.Joost J. Joosten - 2007 - Notre Dame Journal of Formal Logic 48 (3):381-398.
On the Philosophical Significance of Consistency Proofs.Michael D. Resnik - 1974 - Journal of Philosophical Logic 3 (1/2):133 - 147.
A Simple Proof That Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.