Completeness of Second-Order Intuitionistic Propositional Logic with Respect to Phase Semantics for Proof-Terms
Completeness of Second-Order Intuitionistic Propositional Logic with Respect to Phase Semantics for Proof-Terms
复制标题
二阶直觉命题逻辑关于证明项阶段语义的完备性
DOI：
10.1007/s10992-018-9484-z
复制
发表时间：
2018
影响因子：
1.5
通讯作者：
Yuta Takahashi and Ryo Takemura
中科院分区：
文献类型：
--
作者：
Kana GOTO;Hiroki NAKAMOTO;Shiro MORI;Yuta Takahashi and Ryo Takemura
吉拉德引入了相语义作为线性逻辑的完备集合论语义，冈田修正了相语义完备性证明以获得规范形式定理。在此基础上，Okada和Takemura重新表述了吉拉德的阶段语义学，使之成为证明项的阶段语义学，即，- 条款他们制定了Laird的对偶仿射/直觉主义的代数演算的证明项的相位语义，并通过完备性定理证明了Laird演算的规范形式定理。它们的语义是通过可计算性谓词的应用获得的。本文首先通过对Tait-Girard饱和集方法的改进，给出了二阶直觉命题逻辑证明项的阶段语义。接下来，我们证明了这个语义的完备性定理，这意味着一个强规范化定理。
Girard introduced phase semantics as a complete set-theoretic semantics of linear logic, and Okada modified phase-semantic completeness proofs to obtain normal-form theorems. On the basis of these works, Okada and Takemura reformulated Girard’s phase semantics so that it became phase semantics for proof-terms, i.e., lambda-terms. They formulated phase semantics for proof-terms of Laird’s dual affine/intuitionistic lambda-calculus and proved the normal-form theorem for Laird’s calculus via a completeness theorem. Their semantics was obtained by an application of computability predicates. In this paper, we first formulate phase semantics for proof-terms of second-order intuitionistic propositional logic by modifying Tait-Girard’s saturated sets method. Next, we prove the completeness theorem with respect to this semantics, which implies a strong normalization theorem.