Explicit Composition and Its Application in Proofs of Normalization
Jan von Plato · Trends in logic · 2015
The class of derivations in a system of logic has an inductive definition. One would thus expect that crucial properties of derivations, such as normalization in natural deduction or cut elimination in sequent calculus or consistency in arithmetic be proved by induction on the last rule applied. So far it has not been possible to implement this simple requirement uniformly. It is suggested that such proofs can be carried through by a ‘Hilfssatz’ methodology that is hidden in Gentzen’s original unpublished proof of the consistency of arithmetic: to prove that a suitably chosen property of derivations is maintained under the composition of two derivations. As examples, new proofs by induction on the last rule in a derivation are given for normalization and strong normalization in natural deduction.