Reduction of finite and infinite derivations

Annals of Pure and Applied Logic 104 (1-3):167-188 (2000)
  Copy   BIBTEX

Abstract

We present a general schema of easy normalization proofs for finite systems S like first-order arithmetic or subsystems of analysis, which have good infinitary counterparts S ∞ . We consider a new system S ∞ + with essentially the same rules as S ∞ but different derivable objects: a derivation d∈S ∞ + of a sequent Γ contains a derivation Φ∈S of Γ . Three simple conditions on Φ including a normal form theorem for S ∞ + easily imply a weak normalization theorem for S . We give three examples of application of this schema. First, we take S≡PA but restrict the attention to derivations of Σ 1 0 -sentences. In this case it is possible to take S ∞ + to be essentially standard formulation of PA ∞ . Next, we illustrate extension to subsystems of analysis and consider the system BI 1 ∗ of W. Buchholz having the strength of ID 1 , again for derivations of Σ 1 0 -sentences. Finally, we return to the first-order arithmetic to illustrate changes needed to treat derivations of arbitrary formulas

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 103,449

External links

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

Through your library

Similar books and articles

Solovay's theorem cannot be simplified.Andrew Arana - 2001 - Annals of Pure and Applied Logic 112 (1):27-41.
Multifunction algebras and the provability of PH↓.Chris Pollett - 2000 - Annals of Pure and Applied Logic 104 (1-3):279-303.
A First-order Conditional Probability Logic.Miloš Milošević & Zoran Ognjanović - 2012 - Logic Journal of the IGPL 20 (1):235-253.
Successor-invariant first-order logic on finite structures.Benjamin Rossman - 2007 - Journal of Symbolic Logic 72 (2):601-618.
Remarks on Herbrand normal forms and Herbrand realizations.Ulrich Kohlenbach - 1992 - Archive for Mathematical Logic 31 (5):305-317.
On the no-counterexample interpretation.Ulrich Kohlenbach - 1999 - Journal of Symbolic Logic 64 (4):1491-1511.

Analytics

Added to PP
2014-01-16

Downloads
29 (#812,446)

6 months
9 (#328,796)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Die Widerspruchsfreiheit der reinen Zahlentheorie.Gerhard Gentzen - 1936 - Journal of Symbolic Logic 1 (2):75-75.
The formulæ-as-types notion of construction.W. A. Howard - 1995 - In Philippe De Groote, The Curry-Howard isomorphism. Louvain-la-Neuve: Academia.
Intensional interpretations of functionals of finite type I.W. W. Tait - 1967 - Journal of Symbolic Logic 32 (2):198-212.
A survey of proof theory.G. Kreisel - 1968 - Journal of Symbolic Logic 33 (3):321-388.
Proof-theoretic analysis of KPM.Michael Rathjen - 1991 - Archive for Mathematical Logic 30 (5-6):377-403.

View all 7 references / Add more references