The Dialectica interpretation of first-order classical affine logic

Masaru Shirahata

We give a Dialectica-style interpretation of first-order classical affine logic. By moving to a contraction-free logic, the translation (a.k.a. D-translation) of a first-order formula into a higher-type $\exists\forall$-formula can be made symmetric with respect to duality, including exponentials. It turned out that the propositional part of our D-translation uses the same construction as de Paiva's dialectica category GC and we show how our D-translation extends GC to the first-order setting in terms of an indexed category. Furthermore the combination of Girard's ?!-translation and our D-translation results in the essentially equivalent $\exists\forall$-formulas as the double-negation translation and Godel's original D-translation.

Keywords: linear logic, dialectica interpretation, categorical logic

2000 MSC: 03B47

Theory and Applications of Categories, Vol. 17, 2006, No. 4, pp 49-79.

TAC Home