ABSTRACT
Since D has a good endsequent, I can form the derivation D j = D C(D ). Let D 2 be obtained from D 1 by replacing all good sequents of Dj by their a-im ages and om itting all non-good sequents. I claim that D 2 is an L^Mor Lt J-d erivation . If M = } u in Dj is a good generalized axiom M = 4 u then M is good, and since u occurs in M also u is good, hence distinct from A. Thus M + =/■ u + in D j is an LM -axiom . Instances of structural rules and of rules for A, V and -i have the property that good conclusions come from good p rem isses; hence they remain in effect between the cr-images in D 2 . If (AINA) in K Jot produced a good M u from M = ) A then also this pre m iss is good, and thus (AIN) in LJ leads from M + = $ to M + = > u +. If a sequent M = > v->w arises by (I-*) from v,M = $ w and is good, then this prem iss is good; hence the a-images form an instance of (I-*) if w^A and an instance of ( In ) if w = A . Consider now a good K -sequent v-*w,M u obtained w ith (E->) from M = $ v and w ,M = } u . Then the first prem iss is good also; the left will be good if w /A , and in this uncritical case I can apply (E->) to the cr-images. In the semicritical case w = A , u = A the good left prem iss has the cr-image M + = > v + from where (E n ) leads to the image i v +,M + = 4 of the conclusion. Fully critical instances of (E->) do not occur in D j. [In the case of K Jot the operator D c is actually not needed since fully critical instances of (E->) can be treated d irectly : the good left prem iss again gives _w + ,M + = $ and thus ~iv + ,M + = 4 u + by (AIN).]
The use of L -sequents makes it possible to formulate minimal and intuitionistic calculi for the language Fm( n) in a convenient manner. S till, it possible to formulate such calculi also with K -sequent s. For the sake of convenience, I restrict m yself to the case of t-seq u en ts.
