I n an earlier paper [2], using ZERMELO-FRAENXEL set theory (ZF) as metalanguage, for each ordinal 6 2 1, I introduced a system TTo of transfinite type theory formulated in GENTZEN'S sequentzen style [3]. The notion of sequent and the rules of inference were straightforward generalizations of those for LK . Thus it appeared natural to consider a system JITTe derived from TTe in the same manner that GENTZEN derived his intuitionistic logic LJ from LK: sequents are allowed to contain at most one formula in the consequent. While I hesitate to call such a system "intuitionistic" (particularly when 0 is not a constructive ordinal), I feel the system has some interest in its own right, especially in view of Theorem 4.12 below. The system JITTe and a variant JzTTe are introduced in Section 1, while the notion of a model is considered in Section 2. I n Sections 3 and 4, I extend the methods of PRAWITZ [9] to prove completeness and cut-elimination theorems for these systems. The systems MTTe and S4TTe are versions of TTe in which the underlying logics are sequentzen versions of von WRIGHT'S M and 54, respectively (cf. [7]). These systems are introduced in Section 5 and completeness and cute-limination theorems are obtained for each. Finally in Section 6, I provide a translation of JzTTe in S4TTe which is an extension of GODEL'S [4] translation of the intuitionistic propositional calculus in S 4. As in [2], throughout this paper our metalanguage will be ZF.
51. The basic systems
The system JITT' is obtained from the system TTe of [2] by adding the sole restriction that in a sequent r => A , A contain a t most one element. As observed by PRAWITZ [8] for second-order intuitionistic logic, the symbols A, v and 3 can be defined in JITTe by means of 2 and V.
The system JzTTe differs from JITT' in one essential aspect: it allows the consequent of a sequent to contain more than one formula, as in the system TT'. However, it does not adopt the full rules of TTe for introducing logical symbols in the consequent, but instead requires that in the rules 2-IS, and V-IS, the premiss (upper sequent) contain only one formula to the right of +, and that in the rule 7 -1 8 , no formulas occur to the right of =>. The remaining rules of JzTTe are exactly those of JITTe. Clearly, any sequent provable in JITTe (without cut) is provable in JzTTe (without cut). Conversely, it is easily shown by induction on the lengths of proofs, that if T* A is provable in JzTTe (without cut), then there is a formula A ELI such that F + A is provable in JITTe (without cut). Thus we have L e m m a 1.1. A sequent of the form r=> A is provable in JITTe iff it i s provable in J2TTe. l ) Some of these results were presented in April, 1970 a t the Conference on Recent Research