Reduction of finite and infinite derivations
G. E. Mints · Annals of Pure and Applied Logic · 2000
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 (finite) derivation Φ(d)∈S of Γ. Three simple conditions on Φ(d) 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 Σ10-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 BI1∗ of W. Buchholz having the strength of ID1, again for derivations of Σ10-sentences. Finally, we return to the first-order arithmetic to illustrate changes needed to treat derivations of arbitrary formulas.