Reduction of finite and infinite derivations

✍ Scribed by G. Mints

• Publisher: Elsevier Science
• Year: 2000
• Tongue: English
• Weight: 161 KB
• Volume: 104
• Category: Article
• ISSN: 0168-0072
• DOI: 10.1016/s0168-0072(00)00011-7

✦ Synopsis

We present a general schema of easy normalization proofs for ÿnite systems S like ÿrst-order arithmetic or subsystems of analysis, which have good inÿnitary counterparts S∞. We consider a new system S + ∞ with essentially the same rules as S∞ but di erent derivable objects: a derivation d ∈ S + ∞ of a sequent contains a (ÿnite) 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 0 1 -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 ID1, again for derivations of 0 1 -sentences. Finally, we return to the ÿrst-order arithmetic to illustrate changes needed to treat derivations of arbitrary formulas.