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 turned 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 Godel's original D-translation.
Keywords: linear logic, dialectica interpretation, categorical logic
2000 MSC: 03B47
Theory and Applications of Categories,
Vol. 17, 2006,
No. 4, pp 49-79.
http://www.tac.mta.ca/tac/volumes/17/4/17-04.dvi
http://www.tac.mta.ca/tac/volumes/17/4/17-04.ps
http://www.tac.mta.ca/tac/volumes/17/4/17-04.pdf
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/17/4/17-04.dvi
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/17/4/17-04.ps