A uniform semantic proof for cut-elimination and completeness of various first and higher order logics

Mitsuhiro Okada

研究成果: Article査読

43 被引用数 (Scopus)

抄録

We present a natural generalization of Girard's (first order) phase semantics of linear logic (Theoret. Comput. Sci. 50 (1987)) to intuitionistic and higher-order phase semantics. Then we show that this semantic framework allows us to derive a uniform semantic proof of the (first order and) higher order cut-elimination theorem (as well as a (first order and) higher order phase-semantic completeness theorem) for various different logical systems at the same time. Our semantic proof works for various different logical systems uniformly in a strong sense (without any change of the argument of proof): it works for both first order and higher order versions and for linear, substructural, and standard logics uniformly, and for both their intuitionistic and classical versions uniformly.

本文言語English
ページ(範囲)471-498
ページ数28
ジャーナルTheoretical Computer Science
281
1-2
DOI
出版ステータスPublished - 2002 6月 3
外部発表はい

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「A uniform semantic proof for cut-elimination and completeness of various first and higher order logics」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル