Page 32 - Textos de Matemática Vol. 38

24 FERNANDO FERREIRA
of the language of first-order arithmetic is provable in PA (first-order Peano arithmetic). Then there are closed terms t0 , . . . , tk of Lω0 such that
HAω0 ⊢ ∀f0 ...∀fk Aqf(t0(f),f0(t0(f)),...,tk(f),fk(t0(f),...,tk(f))).
Proof. Note that ∃x0 ...∃xk Aqf(x0,f0(x0),...,xk,fk(x0,...,xk)) follows from ∃x0∀y0 ...∃xk∀yk Aqf(x0,y0,...,xk,yk) by logic alone. Therefore, the former formula is provable in PAω0 . We now use the extraction theorem of the previous section.
To make sense of the name of the theorem, we may think of the sym- bols f0, . . . , fk as denoting functions in S1 that attempt to provide a coun- terexample to the truth of ∃x0∀y0 ...∃xk∀yk Aqf(x0,y0,...,xk,yk), by mak- ing A(n0,f0(n0),...,nk,fk(n0,...,nk)) false for any given numerical values n0, . . . , nk. However, such counterexample must fail because it does not work for
the values n = tSω(f),...,n = tSω(f). As we have already argued, the func- Sω0Sω0 kk
tions t0 , . . . , tk are computable (the closed terms t0, . . . , tk are, essentially, of type 2). Hence, the above theorem says that values that defeat a purported coun- terexample may be effectively constructed from the attempted counterexample and that the effective computations are specified by closed terms of Lω0 .
3.4 Elimination of extensionality
Full extensionality is not a universal scheme and, in fact, it is not inter- preted by a functional of Lω0 . The introduction of the notion of majorizability by William Howard in 1973 was made in order to show this non-interpretability re- sult. Already the simplest non-trivial form of extensionality is not interpretable:
∀Φ2∀x1, y1(∀k0(xk = yk) → Φx = Φy).
To see this, consider the D-interpretation of this sentence. It is:
∃F2110∀Φ2∀x1,y1(x(F(Φ,x,y)) = y(F(Φ,x,y)) → Φx = Φy).
Hence, if the above form of extensionality were interpreted by a closed
term of Lω0 , there would be t of type 2 → 1 → 1 → 0 such that ∀Φ2∀x1, y1(x(t(Φ, x, y)) = y(t(Φ, x, y)) → Φx = Φy).
Take q a monotone closed term such that t ≤∗ q (Howard’s majorizability result). Consider the natural number n = q(12,11,11). It immediately follows that
∀Φ≤∗2 12∀x≤∗1 11∀y≤∗1 11(∀k≤n(xk=yk)→Φx=Φy). This is obviously false for Φ defined by:
Φ(w)= 0 if∀k≤n+1(w(n)=1), 1 otherwise.