Reduction of finite and infinite derivations Original Research Article

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 counterpartsView the MathML source. We consider a new system View the MathML source with essentially the same rules as View the MathML source but different derivable objects: a derivation View the MathML source of a sequent Γ contains a (finite) derivation Φ(d)∈S of Γ. Three simple conditions on Φ(d) including a normal form theorem for View the MathML source 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 View the MathML source-sentences. In this case it is possible to take View the MathML source to be essentially standard formulation of View the MathML source. Next, we illustrate extension to subsystems of analysis and consider the system View the MathML source of W. Buchholz having the strength of View the MathML source, again for derivations of View the MathML source-sentences. Finally, we return to the first-order arithmetic to illustrate changes needed to treat derivations of arbitrary formulas.