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

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. (C) 2002 Published by Elsevier Science B.V.