Page 30 - Textos de Matemática Vol. 38

22 FERNANDO FERREIRA
In the framework of pure logic we must define Ag as ¬¬A for atomic A, but this is not needed in the current framework because atomic formulas are decidable. The result of Go¨del-Gentzen states that if a formula A is clas- sically provable from Γ then Ag is intuitionistically provable from Γg, where Γg = {Bg : B ∈ Γ}. This result extends to HAω0 because the negative transla- tion of an induction axiom is still an induction axiom and because the remainder axioms are universal formulas. It does not extend to HAω0 + ACω + IPω∀ + MPω due to the axiom of choice (the other principles pose no problem since they are laws of classical logic). However, the restriction of the axiom of choice for quantifier-free matrices ACωqf behaves well under the negative translation pro- vided that Markov’s principle MPω is present in the verifying theory (as well as ACωqf itself). In fact:
Theorem 3.4. Suppose that P A ω0 + A C ωq f + ∆ ⊢ A ,
where ∆ is a set of universal sentences and A is an arbitrary sentence. Then HAω0 +ACωqf +MPω +∆⊢Ag.
Let us analyze the negative translation of ACωqf . It is, ∀x¬∀y¬Bqf (x, y) → ¬∀f ¬∀xBqf (x, f x),
where Bqf is a quantifier-free formula (we are using the fact that quantifier-free formulas are decidable). It is easy to check that this translation is provable in HAω0 + ACωqf + MPω . Assume ∀x¬∀y¬Bqf (x, y). By MPω , we get ∀x∃yBqf (x, y). By ACωqf, ∃f∀xBqf(x,fx) and, a fortiori, ¬∀f¬∀xBqf(x,fx).
We may now state an extraction and conservation result which is applicable to a classical theory:
Proposition 3.5 (Extraction and conservation). Suppose that PAω0 + ACωqf + ∆ ⊢ ∀x∃yAqf (x, y),
where ∆ is a set of universal sentences 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).
This is an easy corollary of the properties of the negative translation and the soundness of the Dialectica interpretation. If ∀x∃yAqf(x,y) is provable in PAω0 + ACωqf + ∆ then, by the previous theorem, ∀x¬∀y¬Aqf (x, y) is provable in HAω0 + ACωqf + MPω + ∆. Then so is ∀x∃yAqf (x, y) (because MPω is available!). At this point, we use the soundness theorem.