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

Research output: Contribution to journalArticle

37 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

Fingerprint

Higher-order Logic
Cut-elimination
First-order Logic
Completeness
Semantics
Higher Order
First-order
Linear Logic
Theorem
Logic

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. / Okada, Mitsuhiro.

In: Theoretical Computer Science, Vol. 281, No. 1-2, 03.06.2002, p. 471-498.

Research output: Contribution to journalArticle

@article{24a333f9312d42a69ebdd87919f8b265,
title = "A uniform semantic proof for cut-elimination and completeness of various first and higher order logics",
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.",
author = "Mitsuhiro Okada",
year = "2002",
month = "6",
day = "3",
doi = "10.1016/S0304-3975(02)00024-5",
language = "English",
volume = "281",
pages = "471--498",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1-2",

}

TY - JOUR

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

AU - Okada, Mitsuhiro

PY - 2002/6/3

Y1 - 2002/6/3

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0037014252&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0037014252&partnerID=8YFLogxK

U2 - 10.1016/S0304-3975(02)00024-5

DO - 10.1016/S0304-3975(02)00024-5

M3 - Article

VL - 281

SP - 471

EP - 498

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1-2

ER -