Phase Semantics for Higher Order Completeness, Cut-Elimination and Normalization Proofs (Extended 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.