#
The Dialectica interpretation of first-order classical affine logic

##
Masaru Shirahata

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

TAC Home