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. (shrink)

The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.Through the condition that in a cut-free derivation of the sequent Γ⇒C, no inactive weakening (...) or contraction formulas remain in Γ, a correspondence with the formal derivability relation of natural deduction is obtained: All formulas of Γ become open assumptions in natural deduction, through an inductively defined translation. Weakenings are interpreted as vacuous discharges, and contractions as multiple discharges. In the other direction, non-normal derivations translate into derivations with cuts having the cut formula principal either in both premisses or in the right premiss only. (shrink)