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 first-order 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 D-translation uses the same construction as de Paiva's dialectica category struck G signℂ and we show how our D-translation extends double struck G signℂ 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.
| Original language | English |
|---|---|
| Pages (from-to) | 49-79 |
| Number of pages | 31 |
| Journal | Theory and Applications of Categories |
| Volume | 17 |
| Publication status | Published - 2006 Dec 16 |
Fingerprint
Keywords
- Categorical logic
- Dialectica interpretation
- Linear logic
ASJC Scopus subject areas
- Mathematics(all)
Cite this
The Dialectica interpretation of first-order classical affine logic. / Shirahata, Masaru.
In: Theory and Applications of Categories, Vol. 17, 16.12.2006, p. 49-79.Research output: Contribution to journal › Article
}
TY - JOUR
T1 - The Dialectica interpretation of first-order classical affine logic
AU - Shirahata, Masaru
PY - 2006/12/16
Y1 - 2006/12/16
N2 - 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 ∃∀- 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 struck G signℂ and we show how our D-translation extends double struck G signℂ 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.
AB - 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 ∃∀- 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 struck G signℂ and we show how our D-translation extends double struck G signℂ 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.
KW - Categorical logic
KW - Dialectica interpretation
KW - Linear logic
UR - http://www.scopus.com/inward/record.url?scp=33846486940&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33846486940&partnerID=8YFLogxK
M3 - Article
AN - SCOPUS:33846486940
VL - 17
SP - 49
EP - 79
JO - Theory and Applications of Categories
JF - Theory and Applications of Categories
SN - 1201-561X
ER -