Page 29 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 21
(with the advent of Linear Logic in the late eighties, we learned that contraction is not that innocuous). On the one hand, the choice of witnessing functionals is not canonical at this point. On the other hand, it involves a definition by cases functional. The interpretation of the hypothesis is ∃x∀yAD(x, y) and that of the conclusion is
∃x1∃x2∀y1∀y2(AD(x1, y1) ∧ AD(x2, y2)).
We must define functionals f1, f2 and g such that
AD(x, g(x, y1, y2)) → AD(f1(x), y1) ∧ AD(f2(x), y2).
We take f1 and f2 as λx.x. Suppose that y1 and y2 are of type σ. In order to definegweneedaclosedtermCσ oftype0→σ→σ→σwhichsatisfiesin HAω0 the following “definition by cases” requirements:
B[Cσ(0,u,v)/w] ↔ B[u/w] and B[Cσ(Sz0,u,v)/w] ↔ B[v/w],
where w is a distinguished variable of type σ and B is a quantifier-free for- mula. The functional Cσ can be defined with the aid of the recursor Rσ by Rσ(z,u,λwλs.v). Note that the checking of the contraction axiom needs a recursor, not merely the combinators. Since AD is quantifier-free, there is a closed term t of Lω0 such that HAω0 ⊢ t(x,y) = 0 ↔ ¬AD(x,y). It is easy to see that g can be taken to be λxλy1λy2.Cσ(t(x,y1),y1,y2). But, as re- marked, the choice is not canonical at this point: we can also take the term λxλy1λy2.Cσ(t(x,y2),y2,y1).
3.2 Negative translation
We define G¨odel-Gentzen’s negative translation in the framework of arith- metic.
Definition 3.3. To each formula A of the language Lω0 we associate its (G¨odel- Gentzen) negative translation Ag according to the following clauses:
i. Ag is A, for atomic formulas A, ii. (A ∧ B)g is Ag ∧ Bg,
iii. (A ∨ B)g is ¬(¬Ag ∧ ¬Bg), iv. (A → B)g is Ag → Bg,
v. (∀xA)g is ∀xAg, vi. (∃xA)g is ¬∀x¬Ag.