# zbMATH — the first resource for mathematics

The Dialectica interpretation of first-order classical affine logic. (English) Zbl 1115.03087
Summary: 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 turns 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 Gödel’s original D-translation.

##### MSC:
 03F52 Proof-theoretic aspects of linear logic and other substructural logics 03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) 03G30 Categorical logic, topoi
##### Keywords:
linear logic; Dialectica interpretation; categorical logic
Full Text: