A uniform semantic proof for cut-elimination and completeness of various first and higher order logics
A uniform semantic proof for cut-elimination and completeness of various first and higher order logics
复制标题
各种一阶和高阶逻辑的割除消除和完备性的统一语义证明
DOI：
10.1016/s0304-3975(02)00024-5
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
M. Okada
中科院分区：
文献类型：
--
作者：
M. Okada
我们提出了一个自然的推广吉拉德的（一阶）阶段语义的线性逻辑（理论。Sci. 50（1987））到直观和高阶相位语义。然后，我们表明，这个语义框架，使我们能够得到一个统一的语义证明的（一阶和）高阶切割消除定理（以及（一阶和）高阶阶段语义完备性定理）在不同的逻辑系统在同一时间。我们的语义证明在很强的意义上一致地适用于各种不同的逻辑系统（不改变证明的自变量）：它对一阶和高阶版本都有效，对线性、子结构和标准逻辑都有效，对直觉和经典版本都有效。
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.