Page 17 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 9
A term t reduces to another term q in one step if q is obtained from t by contracting a single sub-term of t. A term is said to be in normal form if it does not admit reductions in one step. A reduction sequence is a sequence of terms t0, . . . , tn such that each term reduces in one step to the next. In this case, we say that t0 reduces to tn. If tn cannot be reduced further then tn is in normal form and the sequence is called terminating.
Theorem 1.6 (Strong normalization). Every term reduces to a unique term in normal form. Moreover, every reduction sequence eventually terminates.
The uniqueness result is the Church-Rosser theorem for this reduction cal- culus. Normalization strictu sensu is the fact that every term has a terminating reduction sequence (strong normalization is the fact that every reduction se- quence eventually terminates). Proofs of normalization are bound to use strong forms of induction (viz. induction on non-arithmetical predicates), because it is known that it (elementarily) implies the consistency of first-order Peano arith- metic. This fact follows from Go¨del’s functional interpretation, discussed in the third lesson.
A corollary of the normalization theorem is that every closed term r of type 0 reduces to a numeral n and, clearly, HAω0 ⊢ r = n. Therefore, we can assign to each closed term t of type 1 a number theoretical function that maps each k ∈ N to the unique natural number n such that tk reduces to n. As we will comment, closed terms of type 1 give exactly what are dubbed the provably recursive functions of PAω0 (and, actually, of PA).
Let CTσ be the set of closed terms of type σ, and let CTω be ⟨CTσ⟩σ∈T . Given closed terms t, q of type zero, we say that t =CTω q if the normal forms oftandqarethesameterm.Ift∈CTρ→τ andq∈CTρ thenAppCTω(t,q)is defined as the term App(t,q). With these specifications and the interpretation of constants by themselves, CTω is a model of HAω0 .
A modification of the reduction calculus above has an interesting appli- cation. Let T be a closed term of type 2. The interpretation of T in the full set-theoretical model Sω , denoted by T Sω , is a function from S1 to N. We claim that this function is continuous. In fact, we claim more: TSω is a computable function (such functions are, of necessity, continuous since each computation only depends on a finite initial segment of the input, which is considered an oracle for effecting the computation). Fix a distinguished variable xˇ of type 1. Take any α ∈ S1. We complement the previous normalization calculus with a new contraction rule:
n) and q is α(n). (v)α tisxˇ(
This α-normalization calculus enjoys the property of strong normalization. Therefore, the type 0 term T xˇ has a (unique) normal form which (it may easily be argued) must be a numeral n. Due to the semantical soundness of the con- traction procedure, it is clear that T Sω (α) = n. It is also clear that the process of