The Dialectica interpretation of first-order classical affine logic

研究成果: Article査読

9 被引用数 (Scopus)

抄録

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.

本文言語English
ページ(範囲)49-79
ページ数31
ジャーナルTheory and Applications of Categories
17
出版ステータスPublished - 2006 12月 16

ASJC Scopus subject areas

  • 数学(その他)

フィンガープリント

「The Dialectica interpretation of first-order classical affine logic」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル