The Dialectica Interpretation of First-Order Classical Affine Logic

Abstract. 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 firstorder formula into a higher-type ∃∀-formula can be made symmetric with respect to duality, including exponentials. It turned out that the propositional part of our Dtranslation 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 ∃∀-formulas as the double-negation translation and Gödel’s original D-translation