A proof of cut-elimination theorem in simple type-theory
Moto-o Takahashi · Journal of the Mathematical Society of Japan · 1967
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 constructivelyhave not yet succeeded.On the other hand, W. Tait [3] proved the cut- elimination 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 Pro- fessor T. Nishimura, Mr. K. Namba and Mr. T. Uesu for their kind advice and assistance.\S 1. Complexes The system of simple type-theory we shall use is Sch\"utte's system in $[2]^{2)}$ .We shall use the notations in [2].Let $V$ be a semi-valuation3).We shall define V-complexes of type $\tau$ by induction on types.1.1.A V-complex of type $0$ is a pair $[e^{0},0]$ , where $e^{0}$ is an expression of type $0$ . A V-complex of type 1 is a pair$[A, p]$ , where $A$ is a well-formed formula and $p$ is $t$ or $f$ satisfying the following conditions. If2) For the sake of brevity, constants (except function constants) are omitted, since they can be identified with free variables.3) Our proof remains valid, if the term " semi-valuation " is replaced by " partial valuation" throughout this paper.But we use only the conditions 6.1.1.-6.1.7. in [2] but do not use 6.2.1.-6.2.7. in [2].