Phase Semantics for Higher Order Completeness, Cut-Elimination and Normalization Proofs (Extended Abstract)

Research output: Contribution to journalArticle

9 Citations (Scopus)

Abstract

We give a natural extension of Girard phase semantics of the linear logic [1] to the classical and intuitionistic higher order linear logics and give a uniform phase-semantic proof of the higher order cut-elimination theorem as well as the completeness theorem. Although our proof in this paper is mainly concentrated on the framework of linear logic, the proof technique works for various different logical systems uniformly, too. We also extend our phase semantics for provability to phase semantics for proofs, by modifying the phase space of monoid domain to that of proofs domain, in a natural way. The resulting phase semantics for proofs provides various versions of proof-normalization theorem. The details of this extension will appear in the full-version of this paper. The author would like to express his thanks to Mr. Kazushige Terui for his careful reading of the earlier draft and for his valuable comments. The author also would like to express his thanks to Drs. Jean-Yves Girard, Max Kanovitch, and Andre Scedrov for stimulating discussions and encouragements during the preparation of this paper.

Original languageEnglish
Pages (from-to)154
Number of pages1
JournalElectronic Notes in Theoretical Computer Science
Volume3
Issue numberC
DOIs
Publication statusPublished - 1996

Fingerprint

Cut-elimination
Normalization
Completeness
Semantics
Higher Order
Linear Logic
Express
Theorem
Higher-order Logic
Natural Extension
Monoid
Phase Space
Preparation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)
  • Computer Science (miscellaneous)

Cite this

@article{2be2d6dd234441f9a816ec45ac00b6af,
title = "Phase Semantics for Higher Order Completeness, Cut-Elimination and Normalization Proofs (Extended Abstract)",
abstract = "We give a natural extension of Girard phase semantics of the linear logic [1] to the classical and intuitionistic higher order linear logics and give a uniform phase-semantic proof of the higher order cut-elimination theorem as well as the completeness theorem. Although our proof in this paper is mainly concentrated on the framework of linear logic, the proof technique works for various different logical systems uniformly, too. We also extend our phase semantics for provability to phase semantics for proofs, by modifying the phase space of monoid domain to that of proofs domain, in a natural way. The resulting phase semantics for proofs provides various versions of proof-normalization theorem. The details of this extension will appear in the full-version of this paper. The author would like to express his thanks to Mr. Kazushige Terui for his careful reading of the earlier draft and for his valuable comments. The author also would like to express his thanks to Drs. Jean-Yves Girard, Max Kanovitch, and Andre Scedrov for stimulating discussions and encouragements during the preparation of this paper.",
author = "Mitsuhiro Okada",
year = "1996",
doi = "10.1016/S1571-0661(05)80414-1",
language = "English",
volume = "3",
pages = "154",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "C",

}

TY - JOUR

T1 - Phase Semantics for Higher Order Completeness, Cut-Elimination and Normalization Proofs (Extended Abstract)

AU - Okada, Mitsuhiro

PY - 1996

Y1 - 1996

N2 - We give a natural extension of Girard phase semantics of the linear logic [1] to the classical and intuitionistic higher order linear logics and give a uniform phase-semantic proof of the higher order cut-elimination theorem as well as the completeness theorem. Although our proof in this paper is mainly concentrated on the framework of linear logic, the proof technique works for various different logical systems uniformly, too. We also extend our phase semantics for provability to phase semantics for proofs, by modifying the phase space of monoid domain to that of proofs domain, in a natural way. The resulting phase semantics for proofs provides various versions of proof-normalization theorem. The details of this extension will appear in the full-version of this paper. The author would like to express his thanks to Mr. Kazushige Terui for his careful reading of the earlier draft and for his valuable comments. The author also would like to express his thanks to Drs. Jean-Yves Girard, Max Kanovitch, and Andre Scedrov for stimulating discussions and encouragements during the preparation of this paper.

AB - We give a natural extension of Girard phase semantics of the linear logic [1] to the classical and intuitionistic higher order linear logics and give a uniform phase-semantic proof of the higher order cut-elimination theorem as well as the completeness theorem. Although our proof in this paper is mainly concentrated on the framework of linear logic, the proof technique works for various different logical systems uniformly, too. We also extend our phase semantics for provability to phase semantics for proofs, by modifying the phase space of monoid domain to that of proofs domain, in a natural way. The resulting phase semantics for proofs provides various versions of proof-normalization theorem. The details of this extension will appear in the full-version of this paper. The author would like to express his thanks to Mr. Kazushige Terui for his careful reading of the earlier draft and for his valuable comments. The author also would like to express his thanks to Drs. Jean-Yves Girard, Max Kanovitch, and Andre Scedrov for stimulating discussions and encouragements during the preparation of this paper.

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

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

U2 - 10.1016/S1571-0661(05)80414-1

DO - 10.1016/S1571-0661(05)80414-1

M3 - Article

AN - SCOPUS:19144372424

VL - 3

SP - 154

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - C

ER -