Appendix A3 - Strong normalization proofs

Summary

As we have seen in Chapter 10, the main property of typed systems not possessed by untyped systems is that all reductions are finite, and hence every typed term has a normal form. In this appendix we shall prove this theorem for the simply typed systems in Chapter 10, and for an extended system from which the consistency of first-order arithmetic can be deduced.

The proofs will be variations on a method due to W. Tait, [Tai67]. (See also [TS00, Sections 6.8, 6.12.2] or [SU06, Sections 5.3.2–5.3.6].) Simpler methods are known for pure λ and CL, but Tait's is the easiest to extend to more complex type-systems.

We begin with two definitions which have meaning for any reduction concept defined by sequences of replacements. The first is a repetition of Definition 10.14. The second is the key to Tait's method.

Definition A3.1 (Normalizable terms) A typed or untyped CL-or λ-term X is called normalizable or weakly normalizable or WN with respect to a given reduction concept, iff it reduces to a normal form. It is called strongly normalizable (SN) iff all reductions starting at X are finite.

As noted in Chapter 10, SN implies WN. Also the concept of SN involves the distinction between finite and infinite reductions, whereas WN does not, so SN is a fundamentally more complex concept than WN.