Page 39 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 31
consider the function f1 which has the value 0 for the natural numbers up to m and is equal to 1 afterwards (note that, with suitable definition, HAω✂ proves that f ✂1 1).
By internalizing and adapting the argument given in Section 3.4, it can also be shown that HAω✂ + bACω✂ + MPω✂ refutes the following form of extensionality:
∀Φ2∀x1, y1(∀k0(xk = yk) → Φx = Φy).
Hence, as opposed to G¨odel’s Dialectica interpretation, in the present setting there cannot hold an elimination of extensionality result.
It is pressing to show that HAω✂ + bACω✂ + bIPω✂ + MPω✂ + bBCCω✂ + MAJω✂ is consistent. This follows from the soundness theorem below.
Theorem 4.5 (Soundness of bounded functional interpretation). Suppose that
HAω✂ +bACω✂ +bIPω✂ +MPω✂ +bBCCω✂ +MAJω✂ +∆ ⊢ A(z
where ∆ is a set of universal sentences and A is an arbitrary formula (with the free variables as shown). Then there are closed monotone terms of appropriate types such that
HAω✂ +∆⊢∀˜a∀z✂a∀˜cAB(t(a),c,z
As usual, the proof is by induction on the length of formal proofs, and the terms are effectively constructed from the formal proofs. However, for the bounded functional interpretation the choice of the witnessing terms is always canonical and there is no need for a definition by cases functional.
Question 4. Find a semantics for the theory HAω✂ + bACω✂ + bIPω✂ + MPω✂ + bBCCω✂ + MAJω✂.
The problem in addressing positively the above question does not lie solely in that the above theory is classically inconsistent and refutes a mild form of ex- tensionality. It is also due to the fact that its “flattened” version is inconsistent. We explain this observation in the next section.
4.3 Extraction and conservation for the bounded functional in- terpretation
The negative translation of G¨odel-Gentzen can be easily extended to the language Lω✂ according to the extra clauses:
vii. (∀x✂tA)g is ∀x✂tAg, viii. (∃x✂tA)g is¬∀x✂t¬Ag.
),
).