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

Mitsuhiro Okada

Research output: Contribution to journalArticlepeer-review

38 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)471-498
Number of pages28
JournalTheoretical Computer Science
Volume281
Issue number1-2
DOIs
Publication statusPublished - 2002 Jun 3

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A uniform semantic proof for cut-elimination and completeness of various first and higher order logics'. Together they form a unique fingerprint.

Cite this