Geodesic
The Dialectica interpretation of first-order classical affine logic
Theory and applications of categories, Chu spaces: theory and applications, Tome 17 (2006), pp. 49-79 Cet article a éte moissonné depuis la source Theory and Applications of Categories website

Voir la notice de l'article

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.

Classification : 03B47
Keywords: linear logic, dialectica interpretation, categorical logic 
@article{TAC_2006_17_a3,
     author = {Masaru Shirahata},
     title = {The {Dialectica} interpretation of first-order classical affine logic},
     journal = {Theory and applications of categories},
     pages = {49--79},
     year = {2006},
     volume = {17},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_2006_17_a3/}
}
TY  - JOUR
AU  - Masaru Shirahata
TI  - The Dialectica interpretation of first-order classical affine logic
JO  - Theory and applications of categories
PY  - 2006
SP  - 49
EP  - 79
VL  - 17
UR  - http://geodesic.mathdoc.fr/item/TAC_2006_17_a3/
LA  - en
ID  - TAC_2006_17_a3
ER  - 
%0 Journal Article
%A Masaru Shirahata
%T The Dialectica interpretation of first-order classical affine logic
%J Theory and applications of categories
%D 2006
%P 49-79
%V 17
%U http://geodesic.mathdoc.fr/item/TAC_2006_17_a3/
%G en
%F TAC_2006_17_a3
Masaru Shirahata. The Dialectica interpretation of first-order classical affine logic. Theory and applications of categories, Chu spaces: theory and applications, Tome 17 (2006), pp. 49-79. http://geodesic.mathdoc.fr/item/TAC_2006_17_a3/