The cut elimination theorem in the unary second order language
Mitsuru Yasuhara · Proceedings of the American Mathematical Society · 1966
ln [T], Takeuti has conjectured that the cut elimination theorem holds for the simple theory of types cast in the sequent calculus. This conjecture is true for the first order language, as Gentzen had shown in [G]. (Indeed, the conjecture was made after Gentzen had proved his Hauptsatz.) The purpose of this Note is to show that the conjecture is true for the unary second order language U (Theorem II). Our proof is based on another result of the Note which concerns the unary second order language with equality U+. This theorem shows that the requirement of is not really a restriction on deducibility in U+. In showing this, an essential use is made of the decision procedure for this language (cf. [A], for instance). The Note ends with a Remark in which the negative answer is given to a few possible extensions of above results. The fact that predicativity is an essential restriction on deducibility in U seems to deserve mentioning here. The primitive symbols of U consist of free and of bound variables for elements, for propositions, and for sets, and symbols for negation, for disjunction, and for existential quantification. These symbols will be denoted by a, b, * *,x, y,* . ; P, Q, , S, T,.. *; A(), B( ), * * *, X( ), Y( ), * -* ; v, and 3, respectively. Symbols for other logical connectives may be used as abbreviations. The language U+ is richer than U in that the symbol for equality, * = *, is included. The well formed formulae and the sequents are defined in the standard way. We use German capitals and Greek capitals to denote formulae and finite sequences of formulae, respectively. A well formed formula is naturally called of first order if no bound variables for propositions or for sets occur in it. The sequents 2f-*2f are taken as the axioms of U, for all primitive formulae 21. The rules of U which are not found in [G] are those about variables for propositions and for sets. They are as follows: