The Dialectica interpretation of first-order classical affine logic

Research output: Contribution to journalArticle

7 Citations (Scopus)

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 languageEnglish
Pages (from-to)49-79
Number of pages31
JournalTheory and Applications of Categories
Volume17
Publication statusPublished - 2006 Dec 16

Fingerprint

Logic
First-order
Interpretation
Contraction
Duality

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 journalArticle

@article{b9011666f94846759d06fa5fe3c4edf7,
title = "The Dialectica interpretation of first-order classical affine logic",
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{\"o}del's original D-translation.",
keywords = "Categorical logic, Dialectica interpretation, Linear logic",
author = "Masaru Shirahata",
year = "2006",
month = "12",
day = "16",
language = "English",
volume = "17",
pages = "49--79",
journal = "Theory and Applications of Categories",
issn = "1201-561X",
publisher = "Mount Allison University",

}

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 -