Page 33 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 25
In spite of Howard’s non-interpretability result, it is still possible to extract computational information from certain classical proofs that use full extension- ality.
Definition 3.9. We define, by recursion on the type:
a) x ≈0 y ≡ x = y,
b) x≈ρτ y≡∀uρ,vρ(u≈ρ v→xu≈τ yv).
Let the expression E(x) abbreviate x ≈ x and, given a formula A of Lω0 , let AE be the relativization of A to the predicate E. The following result, due to Horst Luckhardt, is not difficult to prove:
Theorem 3.10 (Elimination of extensionality). Suppose that
an arbitrary formula with its free variables as shown and ACi,j , i, j ∈ {0, 1}, is qf
the form of choice ∀xi∃yjAqf(x,y) → ∃f∀xAqf(x,fx). Then,
PAω +AC0,1 +AC1,0 +∆⊢E(z)→AE(z qf qf
The combination of G¨odel’s Dialectica interpretation with G¨odel-Gentzen’s negative translation and Luckhardt’s technique of elimination of extensionality, yields:
Proposition 3.11 (Extraction and conservation). Suppose that E-PAω +AC0,1 +AC1,0 +∆⊢∀x0/1∃yAqf(x,y),
where ∆ is a set of universal sentences with only variables of type 0 or 1 and Aqf is a quantifier-free formula with free variables among x and y. Then there is a closed term t of appropriate type such that
HAω0 +∆⊢Aqf(x,tx).
3.5 Fragments and Parsons’ result
In this section, we will briefly consider a very natural subsystem of HAω0 . The theory PRAωi differs from HAω0 by only having the recursor R0 and, corre- spondingly, induction in the following restricted form:
Aqf (0) ∧ ∀x0(Aqf (x) → Aqf (Sx)) → ∀xAqf (x),
where Aqf is quantifier-free. Due to the absence of higher-order recursors, in order to interpret the contraction axioms we need primitive constants Cσ in the language satisfying the “decision by cases” requirements discussed in Section 3.1.
The combination of G¨odel’s Dialectica interpretation and the G¨odel-Gentzen negative translation yields,
E-PAω +AC0,1 +AC1,0 +∆⊢A(z qf qf
),
where ∆ is a set of universal sentences with only variables of type 0 or 1, A is
).
qf qf