A proof of cut-elimination theorem in simple type-theory
A proof of cut-elimination theorem in simple type-theory
复制标题
简单类型论中割消除定理的证明
DOI：
10.2969/jmsj/01940399
复制
发表时间：
1967
影响因子：
0.7
通讯作者：
Moto
中科院分区：
文献类型：
--
作者：
Moto
1990年，G. Takeuti推测切消定理在他的系统GLC和LK中都成立。许多建设性地证明它的尝试尚未成功。另一方面，W. Tait[3]用非构造方法证明了二阶谓词逻辑的消去定理。本文也用非构造方法证明了简单类型论中的切消定理。我们的证明将在Zermelo的集合论中形式化，该集合论既不包含替换公理，也不包含选择公理。作者谨对西村教授、南波先生和上津先生的友好建议和帮助表示感谢。
In [4], G. Takeuti cor1jectured that the cut-elimination theorem would hold in his system GLC as well as in LK. Many attempts to prove it constructively have not yet succeeded. On the other hand, W. Tait [3] proved the cutelimination theorem for the second order predicate logic by a non-constructive method. In this paper, we shall prove the cut-elimination theorem in simple type-theory also by a non-constructive method. Our proof will be formalizable in Zermelo’s set theory, which contains neither the axiom of replacement nor the axiom of choice1). The author wishes to express his thanks to Professor T. Nishimura, Mr. K. Namba and Mr. T. Uesu for their kind advice and assistance.