WESSELS considered in [8] cut elimination in a Gentzen-style &-calculus without equality. But MINC pointed out in [6] that the proof in [8] is defective and mentions that the cut elimination theorem in a modified system can be proved model-theoretically. The work in 3 1, perhaps, carries out exactly what Mwc had in mind. This is, so to speak, a preliminary to 5 2 in which the theorem in question is shown for a system with e and equality. (WESSELS left this as an open problem in [S].) I n the presence of the &-operation, the calculus with equality is not a conservative extension of that without equality. (See the beginning of 5 2.) So, one cannot formulate a system for the former in which the subformula property holds, in particular with respect to the equality symbol. (Nevertheless, the author wonders if there cannot be a more smooth formulation than that in 5 2.) This phenomenon, further, forces us to give separate proof? of the cut elimination theorem for systems with and without equality, thus justifying the work in 5 1.
Unfortunately, our systems lack the subformula property, and so we cannot obtain various consequences of the cut elimination theorem in the usual manner. For instance, further work is needed to know if the interpolation theorem holds in &-calculi.
Since our purpose is merely to show that cut elimination theorems do hold in two systems, we use model-theoretic means and show completeness of systems without cut rule. If one is interested in a constructive proof, it would, perhaps, be more appropriate to give a consistency proof of ACXERMANN'S (or HILBERT'S!) formulation of Penno arithmetic in [l] (or some reforniulation of it) by means of a cut elimination theorem. We recall that HINATA [4] has recently done this for a system without the &-symbol.
51. System without equality
Nye follow [8] in notation and symbolism. However, for simplicity, we use only 1 , v, 3 and E as connectives. So the following is the list of rules of inference.
We call the second to last rule (el), because we need another rule for e in the next section. Xote, also, that this rule is suggested in [6]. I n ( 1 3 ) and ( e l ) , a is an eigenvariable, and in ( e l ) A must be nonempty. I n an axiom sequent, there must occur an