Page 43 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 35
Now, remark that min1(x1, yM(k)) ✂1 yM(k). Therefore, we have the desired consequent (#).
We have showed the following:
PAω✂ + bACωbd,✂ + MAJω✂ ⊢ ∀x0/1∃yAqf (x, y).
The result follows from the extraction and conservation result of the pre- vious section and the flattening lemma.
A Kohlenbach-type result, in which the extracted bound is independent of a type 1 bounded input, easily follows:
Proposition 4.11. Suppose that
E-PAω +bAC0,1+AC1,0+Σ1-UB⊢∀x1∀z≤ sx∃y0A (x,y,z),
≤ qf qf 0 1 qf
where Aqf is a quantifier-free formula with free variables among x, y and z, and s is a closed term of type 1 → 1. Then there is a closed monotone term t of type 2 such that
PAω≤ ⊢ ∀x1∀z ≤1 sx∃y ≤0 tx Aqf (x, y, z).
Proof. It follows from the previous proposition that there is a closed monotone term q such that PAω≤ ⊢ ∀x1∀z ≤1 sx∃y ≤0 qxz Aqf (x, y, z). By Howard’s ma- jorizability result (Theorem 1.5), take s˜ a closed term majorizing s. Clearly, the term λx1.q(xM, s˜xM) does the job.
The previous proofs are unable to deal with bAC1,1 because this princi- qf
ple is not eliminated via Luckhardt’s technique. Nevertheless, the result is still true with AC1,1 present. The reason is simple: It can be shown that the theory
qf
E-PAω + AC1,0 + Σ1-UB proves AC1,1. ≤qf0 qf
Proposition 4.12. The theory E-PAω≤ + Σ10-UB proves the following sentence: ∀Φ2∃n0∀α, β ≤1 1(∀k < n(αk = βk) → Φ(α) = Φ(β)).
Proof. We reason inside E-PAω≤ + Σ10-UB. Take an arbitrary Φ2. Given α1 and β1 there is, by extensionality and classical logic, a natural number m such that ∀k ≤ m(αk = βk) → Φ(α) = Φ(β). In particular, by restricting α and β to the Cantor space, we get:
∀α,β≤1 1∃m(∀k≤m(αk=βk)→Φ(α)=Φ(β)). Using Σ10-UB it is not difficult to argue that
∃n0∀α,β ≤1 1∃m ≤ n(∀k ≤ m(αk = βk) → Φ(α) = Φ(β)).
The proposition follows.