Page 31 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 23
On the other hand:
Proposition 3.6. Let t[x1, . . . , xk] be a term with its (free) variables as shown, all of which are of type 0. The theory HAω0 proves the Π02-sentence saying that for
all natural numbers n1,...,nk the closed term t[ As a consequence, so does the theory HA.
n1/x1,...,nk/xk] normalizes.
Notice that PAω0 does not prove that every closed term of Lω0 has a normal form because this would imply that PAω0 proves its own consistency, an impossi- bility by Go¨del’s second incompleteness theorem. To see this, suppose that PAω0 proves “0=1”. By the proof of the soundness of the Dialectica interpretation there would be a sequence of closed terms tn of Lω0 and a sequence of quantifier-
, y) ending in “0=1” such that An(tn, q) holds for each list of free formulas An(x
closed terms q of appropriate types. Well, a truth predicate for these (universal) statements can be defined within PAω0 provided that each closed term normalizes (reducing the verifications of the quantifier-free matrices to checking whether pairs of numerals are, or are not, the same), and this would yield a consistency proof.
The following corollary is immediate, but worth an explicit formulation:
Corollary 3.7. Let us fix a closed term t of type 1. The theory HAω0 proves the
n), has a normal form Π02-sentence saying that, for each numeral n, the term t(
(necessarily a numeral). As a consequence, so does the theory HA.
The previous corollary and Proposition 3.5 imply that the provably total Σ01-functions of PA are given by the closed terms of type 1 of Lω0 . This provides an alternative characterization of the referred provably total functions to the one stemming from Gentzen’s analysis of the consistency of Peano arithmetic in terms of transfinite induction up to the ordinal ε0.
3.3 The no-counterexample interpretation
It is a basic observation in pure logic that a first-order formula in prenex normal form
∃x0∀y0∃x1∀y1 ...∃xk∀yk Aqf(x0,y0,x1,y1,...,xk,yk), is classically valid if, and only if, its Herbrandization
∃x0∃x1 ...∃xk Aqf(x0,f0(x0),x1,f1(x0,x1),...,xk,fk(x0,...,xk))
is classically valid, where f0, f1, . . . , fk are new function symbols of appropriate arities (known as index functions). Perhaps the most intuitive way of seeing this is to show that the negation of the former formula is satisfiable if, and only if, the negation of the latter one is.
Theorem 3.8 (No-counterexample interpretation). Suppose that the sentence ∃x0∀y0 ...∃xk∀yk Aqf(x0,y0,...,xk,yk),