Page 42 - Textos de Matemática Vol. 38

34 FERNANDO FERREIRA
We finish with a result, essentially due to Kohlenbach, that refines the above proposition and can be proved with the combination of the bounded functional interpretation, the negative translations and Luckhardt’s technique of elimination of extensionality. Let us consider Kohlenbach’s principle Σ10-UB of uniform boundedness (see Section 2.5)
∀k0∀x ≤1 yk∃z0Aqf(x,y,k,z) → ∃χ1∀k0∀x ≤1 yk∃z ≤ χkAqf(x,y,k,z),
for quantifier-free Aqf (possibly with higher-order parameters) and y of type 0 → 1.
We state the result for the theory PAω≤ instead of PRAω: Proposition 4.10 (Extraction and conservation). Suppose that
E-PAω + bAC0,1 + AC1,0 + Σ1-UB ⊢ ∀x0/1∃yA (x, y), ≤ qf qf 0 qf
where Aqf is a quantifier-free formula with free variables among x and y, and E-PAω≤ is just PAω≤ together with full extensionality. Then there is a closed mono- tone term t of appropriate type such that
PAω≤ ⊢ ∀x0/1∃y ≤∗ tx Aqf (x, y).
Proof. Without loss of generality, we may suppose that Σ10-UB is:
∀k0∀x ≤1 yM(k) ∃z0Aqf (x, y, k, z) → ∃χ1∀k0∀x ≤1 yM(k) ∃z ≤ χk Aqf (x, y, k, z),
in the conditions of the proposition. In the presence of full extensionality, we may replace the consequent above by,
(#) : ∃χ1∀k0∀x1 ∃z ≤ χk Aqf (min1(x, yM(k)), y, k, z).
Let (⋆) be the above conditional statement with the modified consequent
(#). By Luckhardt’s technique of elimination of extensionality, we have PAω + bAC0,1 + AC1,0 + (⋆) ⊢ ∀x0/1∃yA (x, y).
≤ qf qf qf
As already discussed (viz. Section 4.2), PAω + bAC0,1 + AC1,0 is a subtheory of
ω ω ω ≤ qf qf
PA✂ +bACbd,✂ +MAJ✂. We claim that this latter theory proves (⋆). To see this,
assume ∀k0∀x ≤1 yM(k) ∃z0Aqf (x, y, k, z). In particular, ∀k0∀x✂1 yM(k)∃z0Aqf(x,y,k,z).
By intensional bounded collection for bounded matrices, we may infer that ∀k0∃m0∀x ✂1 yM(k) ∃z ≤ m Aqf (x, y, k, z).
We may now use bACωbd,✂ to conclude ∃χ1∀k0∀x ✂1 yM(k) ∃z ≤ χk Aqf (x, y, k, z).