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.

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
Full Text: EMIS EuDML