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

We present a natural generalization of Girard's (first-order) phase semantics of linear logic [\textit{J.-Y. Girard}, Theor. Comput. Sci. 50, 1--102 (1987; Zbl 0625.03037)] 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.