×

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
PDF BibTeX XML Cite
Full Text: EMIS EuDML