8.

THE ABSOLUTELY STRICT SYSTEMS -- MODAL SEQUENT-LOGIC

Introduction

AS we have seen, both the classical and the intuitionist propositional calculi may be formulated as sequent-logics, in the manner of Gentzen 1934. The same holds, it turns out, for a fair number of modal systems, including those we have been discussing in the last few chapters. The classical and the intuitionist sequent-logics are distinguished, of course, by differences in certain of their rules; specifically, in the rule of weakening and in the rule ®N. In both of these rules in the intuitionist system, the succedent of the premiss must be null; in the classical system there is no such restriction. As might be expected, the sequent-logics corresponding to our modal systems will have -- in addition to the rules of the ordinary classical sequent-logic -- rules governing the insertion of operators which are specifically modal; the sequent-logics corresponding to the various modal systems will be distinguished -- as are the classical and the intuitionist systems -- by varying one or the other of the rules governing modal connectives.

The formulations of the ordinary modal systems with which we shall compare our modal sequent-logics will be, basically, those of the last chapter. As it happens, another advantage of the 'Lemmon-Zeman-Thomas' formulations is that they permit easy comparison of those modal systems to appropriate sequent-logics. The specific primitive modal operator we shall use will be L, the sign of necessity. Each of the systems will be formulated by adding to the classical sequent-logic a rule primarily intended to govern insertion of L into the succedent of a sequent and -- for the systems S1, S2, and T -- a rule to govern insertion of L into the antecedent. These rules will be respectively ®L and L®; it is the rule ®L which will, by its varying form, distinguish between the various systems; L® will be the same in all the systems containing it.

We look first at the latter of these rules. What -- at the very least -- might we expect to be a premiss that would justify the generation of a sequent with one of its antecedent formulas prefixed by an L? On the very simplest level, what would be the premiss most likely to lead to the sequent

La ® b?

With our intuitive notion of necessity, it would seem that certainly, if the formula a itself yields b, then La will do so as well. With this concept of necessity, the simplest premiss leading to the above sequent by way of L® would be

a ® b.

(This concept of necessity is, as one might expect, foreign to the systems S1°, S2°, and T°.) In its most general form, the suggested rule L® would be

And this is indeed the form of the rule which will be used for the sequent-logics corresponding to S1, S2, and T.

The rule L® permits us to pick out one of any number of formulas in the antecedent of a sequent and prefix to that formula an L. Will the rule ®L give us similar licence for the succedent? Suppose that it did. The succedent of a sequent is interpreted as the disjunction of the formulas composing it. If we were permitted to prefix an L to one of the disjuncts when there are several formulas in the succedent, it would be like saying that if the formula a yields the disjunction Abg, then it also yields the disjunction ALbg. But this is contrary to what must be considered a sound intuitive notion of necessity; a disjunction may follow without any of its disjuncts necessarily following. A clear case of this is the law of excluded middle in the classical PC. Since ApNp is a PC theorem, LApNp is a thesis even of S1°, but neither p nor Np is necessary -- ALpLNp, ALpNp, and ApLNp are all unacceptable as theses in a standard modal system (the determination of why is left to the reader). So our rule of ®L cannot have as its conclusion anything like

G -- Q, La

For the systems we are considering, then, we shall be forced to employ a restriction on ®L not unlike that on the rule ®N in the intuitionistic sequent-logic: the succedent into which the L is introduced will have to be singular, that is, it will have one and only one member.

Let us now consider the conditions under which we may introduce L into a succedent. Under what circumstances may a formula La be correctly deduced from a set of given formulas? This question might be answered in as many ways as there are modal systems with sequent-logic versions, and each of these answers will have a certain degree of reasonableness. For the systems we are now considering, however, the basic answer is that a set of formulas is the minimum set sufficient to yield La if

1. Each of the formulas in the set begins with L.

2. The set of formulas formed by stripping each of the original formulas of its initial L yields a.

Or, to view this as a movement from premiss to conclusion rather than vice versa, an application of the suggested rule would have the effect of prefixing an L to each of the formulas in the premiss-sequent of the rule, to the formulas in the antecedent as well as in the succedent. The basic rule would then have the form (note that LG is the sequence formed by prefixing each of the formulas of G with an L):

Thus ®L affects not only the succedent, but the antecedent as well. This rule is open to a variety of restrictions, each of which results in a different sequent-logic. Suppose we allowed this rule to be applied with no restrictions at all; it would then be applicable even when G is empty and would be, in those cases, an analogue of the rule RL, 'If a, then La', which holds in T° and T. As a matter of fact, the classical sequent-logic plus the thus unrestricted ®L is indeed the sequent-logic analogue of T°, and this system plus L® is equivalent to T.

By suitably restricting ®L, we may generate sequent-logics equivalent to various of the proper subsystems of T. There are, for example, systems related to S2 (these systems will be discussed in more detail in a later chapter) called E2 (Lemmon 1957) and E2° (Thomas 1964) which have as a distinctive feature the fact that none of their theses begin with L. If our rule ®L is taken in such a manner that its application is forbidden when G is empty, then it plus LPC gives a system equivalent to E2°, and that system plus L® is equivalent to E2. In S1°, S1, S2°, and S2, theses may begin with L, and so we shall need some means -- for their sequent-logic analogues -- of generating sequents of form ® La; in these systems, however, no thesis begins with more than one L, and so the totally unrestricted form of ®L will not do. The problem is basically one of so stating ®L that it may be applied once and only once with empty G, and further restricting it so that once it has been so applied an effective application of it with empty P cannot be 'sneaked in' indirectly.

Sequent-logic versions of Sl° and S1

The form of the rule ®L for S1° and S1 will incorporate the above-mentioned restriction and more besides. The rule in the form

bears a strong resemblance to one of Becker's rules, 'If LCab then LCLaLb', when it is applied with G non-empty. This strongly suggests that ®L in this form cannot be a rule of the sequent-logic version of S1 or S1°, since Becker's rules do not hold in those systems. But a weaker version of Becker's rule, the BKW of the last chapter, does hold in S1°. This rule is: `If both LCab and LCba, then LCLaLb.' This would suggest that a possibility for the rule ®L might be the following:

A bit of reflection will reveal that the rule in this form is too weak; among other things, it will not permit the generation of key theses like pqCLpLq and Kpqqrpr. But an examination of these two formulas gives us the clue we need for properly restricting ®L for S1°. Each of these formulas has, essentially, two antecedents -- pq and Lp for the former, and pq and qr for the latter. The peculiarity of these pairs of antecedents is that if they are stripped of their initial L's, they form pairs of formulas the disjunctions of which are S1° (indeed, here, PC) theses; ApCpq and ACpqCqr are both provable in PC. This suggests that ®L might be designed to permit deductions such as

and this is the case. The rule in its final form will include both the above-mentioned case and the previously stated analogue of BKW; it is

The rule is a two-premiss version of the basic rule mentioned in the introduction to this chapter. The sequences D and Q are as follows:

1. If G is singulary or empty, Q = G and D = a;

2. In all other cases, D is empty and Q has as its members two and only two of the formulas belonging to G.

Since S1° and S1 contain formulas beginning with L, this rule must be applicable in some cases in which G is empty, without permitting the generation of sequents of form LLa; this and other characteristic features of S1° are handled in the following restriction to this rule:

The left premiss is optional; however, if the rule is once applied with the left premiss not holding, it may not be used again at all in the same proof string.

This restriction covers the application of this rule with empty G; if G is empty, the left premiss is a®; since the right premiss here -- which is ® a -- must always hold, a® can never be provable, and so when G is empty, the left premiss cannot hold. This restriction not only prevents the generation of sequents like ® LLa, but it also permits the derivation of those like ® CLKpqLp while barring their strict implication versions, like ® LKpqLp.

Let us agree to call the sequent-logic version of Sl° LS1°; LS1° is formed by adding to the classical sequent-logic LPC the rule ®L discussed above. The sequent-logic version of S1 is LS1, and results when the rule L® of the introduction to this chapter is added to LS1°.

The normal form theorem in LS1° and LS1

The proof of the normal-form theorem in these systems will be a continuation of the proof of that meta.theorem in Chapter 3. As it turns out, all we need do is supply cases covering the operator L analogous to those of Chapter 2 for the PC operators in which the mix's rank = 2 and grade ³ 1. The cases we must examine are those in which the principal formula of the mix begins with an L which has been inserted as follows; either

1. into both premises of the mix by ®L, or

2. into the left premiss by ®L and into the right by L® . Only case 1 applies to LSl°, of course; both cases must be considered for LS1.

Case 1 may be broken down into several subcases; in any of them the general form of the relevant proof figure, which includes the mix to be eliminated and the applications of ®L creating its premises is:

We shall break case 1 into subcases as follows:

We examine the subcases individually. For case la, replace the general proof figure above by the following:

The rule ®L has, of course, been applied here without left premiss, thus barring its later application in the same proof string. But since one or the other of the left premises in the original proof figure did not hold, the situation with the end sequent there was precisely as that here. We have thus attained the same result with a mix of lower grade, and so in this subcase, the mix is redundant by the induction hypothesis.

In case 1b, the general case 1 form will be, in particular:

This may be replaced by the following:

We have again achieved the results of the original proof with mixes of lower grade, showing that the mix of subcase 1b is eliminable; note that in the replacing proof the holding of the left premiss is maintained.

We now turn to subcase lc; here in the general case 1 format we note the following: If G₁ has two or more members, then by the definition of D and Q in the statement of ®L, D_l is empty and ® Q₁ is a provable sequent. If G₁ has only one member, then G₂ will have one member or more, and so D₂ will be empty and ® Q₂ is provable. Let, then, Q_x be Q₁ if G₁ has two members or more, and be Q₂ otherwise, and replace the original proof figure by:

Whether x = 1 or 2 in the above, the left premiss of the ®L will hold, and  Q_x will consist of precisely two of the member formulas of the combined  G₁ and  G₂. We have then replaced the mix of subcase lc by a mix of lower grade, and so shown that it may be eliminated. The reader may satisfy himself that the rest of the proof of the normal form theorem may be carried out as in Chapter 3.

If we add the rule L® to LS1°, we get the system LS1. To show that the normal form theorem holds in LS1, then, we must show that the mixes of the previously mentioned case 2 are eliminable, that is, the mixes whose left premiss is generated by ®L and right premises by L®; recall again that this is the induction step in the induction on grade at the point where rank = 2. The one relevant proof ending will have the form:

This may be replaced by:

So here too the original mix is replaceable by one of lower grade and is eliminable. Whether or not the left premiss of the original ®L holds or not is here irrelevant; the replacing proof is actually more general than that which it replaces, since in not using ®L at all, it guarantees that that rule may be used later on in the proof. We call attention to the fact that at the stage of the induction step in the rank induction within the induction step in the grade induction, neither L® nor ®L need be considered. If ®L generates one premiss of a mix, that side of the mix cannot be of grade > 1; L® is handled like other single-premiss rules. We may now state:

Equivalence of the systems

The notion of equivalence of a sequent-logic to an ordinary logic will be as in Chapter 3. We shall first show that if a is a thesis of S1°, then ® a is provable in LS1°. We assume as our formulation of S1° that of Chapter 7. If a is a theorem of PC, then ® a is provable in LS1° by LPC. So far as L1, the proper axiom of S1° in this formulation, is concerned, note that the top two sequents of the following proof are LPC theorems, and so provable in LS1°:

The final sequent in this proof corresponds to L1, the proper axiom of S1°. Consider now rule RLR of S1°, which permits the inference of La when a is a PC thesis or the above axiom L1. Note that in the above proof, rule ®L has been applied only with left premiss holding; thus it may now be applied again, making

®  LCKLCpqLCqrLCpr

a theorem of the system. The same applies to the sequents ® a where a is a PC theorem. Since no applications of ®L are needed to prove such sequents, we may always move from such ® a to ® La by an application of ®L. We then have an analogue of rule RLR as it applies in S1°.

Let us now suppose the sequent ®  La to be a theorem of LS1°. Since the normal-form theorem holds in LS1° by *8.1, this sequent must be provable in a proof having the subformula property; the only way to derive this sequent, then, is by an application of ®L, and the premiss for that application must be ® a. If, then, ® La is an LS1° theorem, so too must be ® a, and LS1° contains an analogue of rule RLE.

Now suppose that the sequents ®  LCab and ®  LCba are both provable in LS1°. By the considerations of the above paragraph, ®  Cab and ®  Cba are also provable, and provable with no application of ®L with non-holding left premiss (else the sequents ®  LCab and ®  LCba could not have been generated by the necessary application of ®L). Taking the proof of these sequents back one step further, we see that a ® b and b ® a are also theorems, and provable without use of ®L with non-holding left premiss. We may then construct the following proof figure:

It then follows that LS1° has an analogue of rule BKW. This means that the entire basis of S1° is reflected in LS1°, and so if a is an S1° thesis, ® a must be provable in LS1°.

We now turn to the converse of what we proved above. As in Chapter 3, we approach this question through the notion of interpretation of a sequent in an ordinary logic, employing the same definition of interpretation as does chapter 3. We, then, shall show first of all that if G ® Q is provable in LS1° without application of ®L with non-holding left premiss, then Li(G ® Q), the necessity of the interpretation of that sequent, is a thesis of S1°.

The proof is by course-of-values induction on the number of times the rules, logical or structural, are applied in the proof of the sequent in question. Let this number be n, and first let n = 0. Here, of course, the sequent can only be an axiom of the system and so of form a ® a, which has Caa as its interpretation. But LCaa is an S1° thesis.

On the assumption that our assertion holds when n < k, we let n = k + 1. The (k + 1)th rule application will be either one of the logical or structural rules of LPC, the base system, or it will be an application of ®L with left premiss holding. The reader may easily establish for himself that if b is derivable from a in PC, then Lb follows from La in S1°. This means that if the (k + 1)th step is by an LPC rule, our assertion holds. Suppose now that this step is by ®L with left premiss holding. We consider first the case in which G in the statement of that rule has one and only one member; here the rule takes the form:

By the induction hypothesis, LCab and LCba are both S1° theses; by BKW, then, so too is LCLaLb, the necessity of the interpretation of the conclusion of the (k + 1)th step.

We now examine the more involved case in which P is not singulary. Here the rule takes nn the form:

Here a and b are formulas belonging to G. By the induction hypothesis, we shall have LCCppAab and LCgq as S1° theses, with g a conjunction of G's formulas. We now take these formulas as hypotheses in a proof in S1°:

8.1	LCCppAab	Hyp.
8.2	LCgq	Hyp.

In S1°  we easily move from 8.1 to

8.3

LAab

and from 8.2 to

8.4	gKgq
8.5	KgqqCLKgqLq	5.61, p / Kgq, q / q
8.6	gKgq	J(8.4)(M2), Df.
8.7	KgqqCLgLq	8.5, 8.6, SSE

Since pp strictly implies Kgqq, 8.7 yields

8.8

ppCLgLq

(assume p in neither g nor q). Now let g₁. . . ., g_n be the n members of the sequence G; g is then a conjunction of those formulas, and the following is easily derivable in S1°:

8.9

g1Cg2 . . . CgngCLg1CLg2 . . .  CLgnLg

We note that the antecedent of 8.9 is strictly implied by pp; thus we write:

8.10

ppCLg1CLg2 . . .  CLgnLg

Now let g* be the conjunction of the formulas Lg_l, . . ., Lg_n.; we may then move in S1° from 8.10 to

8.11

ppCg*Lg

S1° enables us to get from 8.8 and 8.11 to

8.12

ppCppCg*Lg

and ultimately to

8.13

ppCg*Lg

We now make use of the interpretation of the left premiss of ®L. By 8.3 and the S1° thesis LApqCpqq and commutativity of alternation, we have both

8.14

Cabb

and

8.15

Cbaa

Since pCqp holds in S1°, by BKW we move from 8.15 to

8.16

Laba

and from 8.14 to

8.17

Lbab

By the proper axiom of S1° and RLR, with substitutions p / a, q / b, r / a we have

8.18

abCbaaa

In the presence of 8.16 and 8.17 this yields

8.19

LbCLaaa

Making the substitution p / a in 8.13 and using that formula and 8.19, we get

8.20

LbCLaCg*Lq

We recall that g* is a conjunction of the formulas of LG, and that by hypothesis La and Lb belong to that sequence. The explicit occurrences of La and Lb in formula 8.20 are then redundant and may be dropped by Sl° methods, giving

8.21

g*Lq

But 8.21 is the formula La  where a is the interpretation of the conclusion of the rule ®L for this case. We have thus shown that the assertion we wished to prove holds in case the (k + 1)th step is by ®L with left premiss holding. This exhausts all the cases, and so if G ® Q is provable in LS1° with no applications of ®L with non-holding left premiss, Li(G ® Q) will be an S1° thesis.

It then follows that in the situation mentioned above, i(G ® Q) will also be provable, by RLE. Let us now consider the case in which there has been an application of  ®L with non-holding left premiss in the proof of G ® Q. By the restriction on this rule, this application must be the last application of ®L in the proof; all the steps that follow it are LPC steps; say that there are m such LPC steps. If m = 0, the very last step is the application of ®L with non-holding left premiss, and is

By the restriction on this rule, the right premiss of this application must be provable without the use of ®L with non-holding left premiss, and so by our earlier work, LCgq must be an S1° thesis. But then by CLCpqCLpLq, CLgLq is an S1° theorem, and so too then must be Cg*Lq, which is the interpretation of the conclusion of the above rule application. We might easily extend this result to cover cases when m > 0; details left to reader. We may then assert:

We glance now at S1 and LS1; it should be evident, and it is left to the reader to verify, that LS1° plus L® is equivalent to S1° plus Lpp. On the basis of *8.2 and our earlier proof that if a holds in S1°, ® a holds in LS1°, we assert:

This means that LS1° and LS1 are equivalent to S1° and S1 in the appropriate sense.

As earlier promised, we now turn to the proof in S1° and S1 of the rule RL1 of the previous chapter; we noted that the present sequent-logics would facilitate that proof, as will the sequent-logic for S2° the proof of RL2. We shall execute the proof by showing that where a gives La by RL1 in S1° or S1, ® a permits us to infer ® La in LS1° or LS1 respectively. First of all, clause (a) of RL1 involves the situation in which a is a PC thesis; there ® a is clearly derivable in LS1° with no use of ®L, and so ® La results from the permissible application of that rule. Next look at clause (b); here LAbg holds in S1° or S1; ® b, g then holds in LS1° or LS1; since ® LAbg also must hold there and is the conclusion of ®L which has ® b, g in the proof above it, that latter sequent must be provable without the use of ®L with empty left premiss. Since by clause (b) CLbCLgd is provable in S1° or S1, Lb, Lg ® d is provable in LS1° or LS1 respectively. Suppose that this latter sequent has in its proof an application of ®L with empty left premiss. Since ® b, g holds with no such application, one or both of b or g must be missing from the antecedent of the premiss of this rule application. By weakening, then, insert the missing one or both of these formulas in the antecedent of the premiss of this rule application; the rule then is applied with non-empty left premiss, by the fact that ® b, g holds. The Lb and Lg are carried as parameters, then, up until the point at which, in the original proof, Lb and/or Lg were introduced (note that in the original proof there can be no ®L's following the one referred to above). There will at this point be a duplicate of Lb and/or Lg in the antecedent of the sequent in question, which copy is simply removed by contraction. The proof is then carried out to the point at which we have Lb, Lg ® d, which is then provable without using ®L with empty left premiss. ® CLbCLgd is then also so provable, making ®L applicable to this last sequent to get ® CLbCLgd as required. Clause (c) applies to S1; since b ® b is an axiom, Lb ® b and so ® CLbb are provable with no use of ®L in LS1 and so ® LCLbb is provable.

Sequent-logic versions of S2° and S2

The form of the rule ®L as employed for S2° will be restricted, but not so sharply as is that rule for S1°. The rule in this case will be a single-premiss rule, and will take the basic form for the absolutely strict systems

This rule for the sequent-logic corresponding to S2° is subject to the following restriction:

®L may be applied with the sequence G empty; however, if it is once so applied, it may not be applied again at all in the same proof string.

The system resulting from the addition of this rule to LPC will be called LS2° (see Thomas 1964); if rule L® is added to LS2°, the result is the system LS2 (see Ohnishi 1961).

The proof of the normal-form theorem for these systems is a mere variation of that for LSl° and LS1. Specifically, the case in which both premises of the mix to be eliminated are generated by ®L and one or the other of the premisses of the ®L's has empty antecedent follows exactly like subcase la in the proof for LS1°. In case both premises are generated by ®L and neither has empty antecedent, the proof parallels case1c, except that no consideration need be made of any left premiss (considerably simplifying the proof). In case the left premiss of the mix is generated by ®L and the right by L®, the proof follows case 2 above, again deleting all reference to left premisses. We then assert:

We may now examine the question of the equivalence of the systems. First of all, it is evident that any deduction that can be performed with LS1°'s version of ®L can be performed with the present version. This means that LS1° is included in LS2°. We now note the following proof in LS2° (the top sequent is provable in LPC):

Kpq ® p
	®L
LKpq ® Lp C® ® CLKpqLp ®L ® LKpqLp

The last application of ®L is with empty G. The formula ® LKpqLp, of course, when added to S1° gives S2°; note that in LS1° the first application of ®L above would have barred the second. We see, then, that with the above result and the inclusion of LS1° in LS2°, it is the case that if a is an S2° thesis, ® a is provable in LS2°.

To carry the proof in the other direction, we follow the same method used for S1° and LS1°, that is, first we show that if G ® Q is provable in LS2° without the use of  ®L with empty antecedent of premiss, then Li(G ® Q) is an S2° thesis. This involves only an extension of the induction step of the analogous proof of the last section. If the (k + 1)th step is by ®L (with non-empty premiss antecedent, of course), then the premiss of that step, G ® q, falls within the induction hypothesis and its interpretation, prefixed by an L, is an S2° theorem ® LCgq. To this we apply rule BKR, giving LCLgLq. Since (LpLqLKpq holds in S2°, by SSS we obtain LCg*Lq as a thesis, and this is the L-prefixed interpretation of the (k + 1)th step of the LS2° proof in question. The rest of the proof for LS2° and its extension to LS2 follow just as in the previous section for LS1° and LS1. We then assert:

We may note at this point a certain relationship between S1° (S1) and S2° (S2). Recall that certain formulas provable in strict implication form in S2° are provable only in material form in S1°; among these are formulas like LKpqLp; the difference in structure between the S1° rule ®L and that rule for S2° tells why this is the case. The proof in LS2° for this last-mentioned formula will include two applications of ®L, the premiss for the first being the sequent Kpq ® p; the later application of this rule creating the strict implication is permitted in LS2° but not in LS1°. But note that if the formula 1 (where 1 is any PC thesis) is inserted into the antecedent of the premiss of the first ®L (by weakening), that premiss becomes 1, Kpq ® p, which is provable in LS1°. Also provable in LS1° is the sequent ® 1, Kpq; this means that in this case we have both left and right premises for application of LS1°'s ®L, so that ultimately we may prove ® KL1LKpqLp in that system. The same applies to many of the formulas provable only as material implications in S1° but as strict in S2°. The strict forms become provable in S1° provided the formula L1 is added as a conjunct to the antecedent of the implication. These formulas were called `T-theorems' in Feys 1965.

It will be recalled that in Chapter 7 we employed in our PC based formulation of S2° (and S2) the rule

RL2:	If a is a PC theorem or a theorem of form CLbg, La.

We asserted there that that rule is derivable in the original formulation of S2°, but deferred the proof of this rule to the present chapter. Note first that if a is a PC thesis, ® a is provable without any use of ®L, and so ® La is provable in LS2° and La in S2°. Now, CLbg is a thesis of S2° iff ® CLbg is derivable in a cut-free proof in LS2°. Suppose ® CLbg is provable in LS2° without the use of ®L with empty antecedent. Then ®L may be so applied to ® CLbg, making ® CLbg a theorem of LS2° and so CLbg a thesis of S2°. On the other hand, suppose that ® CLbg is provable with the use of ®L with empty antecedent. The proof then ends

There is somewhere above this point the proof step

Between this step and the end sequent, there can be no application of ®L. Replace this last-mentioned step with

Since in the original proof ®L is not used between this point and the end, the occurrence of Lb may now be carried parametrically through the proof, duplicating the steps in the original proof. Note that the above ®L is now with non-empty antecedent, and so does not bar later applications of ®L. If we carry out the whole proof as originally except for the above considerations, we arrive at the sequent Lb, Lb ® g -- provable with no use of ®L with empty antecedent -- where the original has Lb ® g. Then we may conclude the proof:

Thus it is the case that whenever ® CLbg is provable in LS2°, ® LCLbg also holds there, and so rule RL2 will hold in S2°.

Sequent-logic versions of T° and T

The sequent-logics paralleling T° and T will again differ from the others of this chapter only in their rule ®L; as we have indicated, it is in these systems that this rule stands in its simplest form. The rule is exactly as stated for S2°, except that it is completely unrestricted; no application of it, even with empty premiss antecedent, bars its later use. Call the system formed by adding this ®L to LPC LT°, and call LT° + L® LT. It is clear that the normal-form theorem is provable for these systems just as for LS2° and LS2; thus:

As was the case with the ordinary propositional calculi IC and PC and their related sequent-logics LIC and LPC, we can now show that a decision procedure exists for the ordinary modal systems we have been studying; to this end, we direct our attention to the rule of contraction in the modal sequent-logics of this chapter. It will be recalled that each of the rules of LPC is simply invertible with respect to each of the others, making the rule of contraction redundant. If the rules added to form modal sequent-logic are also invertible, then those logics will also have contraction as an eliminable rule. A little reflection will show that the rule L® is indeed simply invertible with respect to each of the rules of LPC (and with respect to itself), and that each of the rules of LPC is simply invertible with respect to it. But when we turn to the rule ®L as discussed in this chapter, we find a more complex situation. We call this rule what we do only because we are primarily interested in its role in L-introduction in the succedent. But the rule -- in each of the absolutely strict systems --prefixes an L not only to the formula in the succedent of its premiss, but to every formula in that sequent. There are, therefore, no formulas in its premiss that this rule treats as parameters. It follows immediately that ®L for these systems is simply invertible with respect to no other rule, and no other rule is invertible with respect to it. But paradoxically, this property of ®L does not affect at all the status of the rule of contraction in the systems in which ®L is the only modal rule. So far as contraction in the succedent goes, this rule is like the succedent rules of IC in being not contraction relevant because of the requirement that formulas involved in this rule have singulary succedent. (We informally note at this point that once again, if the rule of weakening is used to introduce a first or a second contracted constituent into either the antecedent or the succedent of a sequent, the contraction in question may be eliminated simply by omitting the weakening step.) This leaves us with the situation in which both contracted constituents are in the antecedent, and both are presumably introduced by ®L. Here the first contracted constituent is, say, La, and is carried as a parameter from its introduction to the introduction of the second contracted constituent by another ®L. But as the second constituent is introduced, the first will always become LLa, and so will be lost as a constituent to be contracted. Thus the rule ®L for these systems can never be used to introduce both contracted constituents. (There is, of course, the trivial case in which both La as contracted constituents are introduced in the same application of ®L. But here the formulas in the premiss which become the La will fall into the scope of the induction hypothesis for contraction elimination and so a sequent like the original premiss but having just one of the a is provable without contraction, and then a sequent like the original conclusion except for having just one La may be generated without contraction by an application of ®L.) The proof of the eliminability of contraction in the systems having just ®L as a modal rule, then, may be carried out just as in LPC, and we may state: