The Dialectica interpretation of first-order classical affine logic
Masaru Shirahata · Theory and applications of categories · 2006
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.I would like to thank Valeria de Paiva and anonymous referees for their helpful comments.