## THE SYSTEMS OF COMPLETE MODALIZATION -- SEQUENT-LOGIC, THE BASIC SYSTEMS

Sequent-logic for S3° and S4°

WE continue the general pattern we have established for this book by casting the systems of the last several chapters as Gentzen-style sequent-logics. We shall recall that at the heart of the Gentzenization of the absolutely strict systems was the rule ®L which -- subject to restrictions depending on the system involved -- permits the inference of LG ® La from  G ® a. The basic function of this rule for the systems of the present chapter will be similar; the main difference will be that the rule ®L for the systems of the present chapter will permit certain formulas in the sequent which is premiss of this rule to be carried as parameters into the conclusion, without having L prefixed to them. For the present systems, the formulas which may be so treated are those in the antecedent of the premiss which happen already to begin with L. The basic form of this rule for these systems then will be

 D, LG ® a ®L LD, LG ® La

Note that the succedent of the sequent involved here again has but one member. The formulas LG are those carried as parameters. If this rule is added in the above unrestricted form to LPC, the result will be a system LS4°, which will correspond to S4°. As might be expected, the above rule will have to be restricted to make it correspond to S3°; the restriction is of a fair degree of complexity. To form a sequent logic LS3°, add to LPC the rule

 D, G ® LQ, a D, LG ® a

®L
LD, LG ® La

We shall explain the above:

 (a) Each formula of LQ is a subformula of a or a subformula of LG or LD; the left premiss is provable in LPC. (b) Either D or G may be empty, but if both of these sequences are empty, rule ®L may not be applied again in the same proof string.

Let us give a few examples of proofs in LS3° employing this somewhat complicated rule. For our first example we wish to prove the sequent LLp ® LLLp.

 Lp ® Lp WK Lp ® Lp, LLp

LLp ® LLp

®L

LLp ® LLLp

Let us note the identity of the formulas in the above proof. The sequence D  indicated in the statement of the rule is, in our above example, empty. LG is then LLp, and so G is Lp. The sequence LQ is composed of the formula Lp, and the formula a is then LLp. The application of ®L, then, corresponds to the format set down in our statement of that rule. Suppose now we had tried to prove as above the related sequent Lp ® LLp. The right premiss of the required ®L would again have D empty and would be LG ® a (= Lp ® LLp). The left premiss would then have to be of form p ® LQ, Lp. Since we shall be able to prove the normal form theorem for this system, it should be clear that a sequent of this last form will not be provable without the use of ®L with empty D and G; the rule as stated here, then, permits the derivation of LLp ® LLLp, but not of its brother sequent Lp ® LLp.

Let us try another example; construct a proof for the sequent ® Lp LqLp (take = LC). The axioms for this proof will be the sequents Lq ® Lq and Lp ® Lp:

 Lq ® Lq WK Lq, p ® Lq, Lp

®C
p ® Lq, CLqLp
 Lp ® Lp WK Lq, Lp ® Lp

®C
Lp ® CLqLp

®L
Lp ® LCLqLp

Here again D is empty, LG = Lp, a is CLqLp, and Q contains just q. Note that an application of ®C to the end sequent of the above proof gives us CLpLCLqLp; since ®L has been used in this proof only within the scope of its restrictions, it may be applied again to give us the sequent ® Lp LqLp as required.

The examples we have been considering have the sequent D empty; let us quickly note what the situation is if the sequent I' has no members; in this case the general form of the rule becomes

 D ® LQ, a D ® a

®L
LD ® La

It is easy to see, then, that the rule with G empty becomes essentially ®L for LS2°; the left premiss here follows from the right by weakening. LS3° then contains LS2°. We note that the sequent LCpCqr ® CLpCLqLr is easily provable in LS2°; we shall use this fact in the proof example to follow.

 Lp ® Lp WK Lp, CpCqr ® Lp, CLqLr

®C

CpCqr ® Lp, CLpCLqLr

LCpCqr ® CLpCLqLr
(holds in LS2°)

®L
 LCpCqr ® LCLpCLqLr ®C ® CLCpCqrLCLpCLqLr

We note that the end sequent above is analogous to formula L4, proper axiom for S3° and S4° in our Lemmon-style bases.

The normal form theorem in LS3° and LS4°

The proof of the normal form theorem here will be an extension of its proof for LPC. The main case to be considered is the induction step of the induction on grade at the base case of the induction on rank. We assume, then, that the normal form theorem holds when grade of mix is £ k, and investigate the situation in which grade = k + 1 and rank = 2. Here one case beyond those of Chapter 3 need be considered for each of LS3° and LS4°; this is when the main connective of the mix formula is L and that formula has just been inserted on each side of the mix by ®L. Let us examine the situation in LS3°. The mix in question is as follows, with La the mix formula:

 D, G ® LQ, a D, LG ® a

®L

LD, LG  ® La

 a, F, Y ® LL, b a, F, LY ® b

®L

La, LF, LY ® Lb

MIX

LD, LF, LG, L ® Lb

We note first that we may mix (and possibly use weakening on) the left premises of each of the above ®L to give

D, F, G, Y ® LQ, LL, b;

since the premises of this mix were LPC theorems, this last sequent is provable without the use of mix. Suppose now that there is a formula Ll belonging to LQ and (it would have to be a subformula of a) a subformula of none of G, D, F, Y, or b. Since this formula begins with an L, it was not inserted by an LPC logical rule, and so it was inserted by weakening or as the succedent of an axiom. But if the latter, then Ll the antecedent of the axiom must also appear in the sequent, in an antecedental position in a formula in the succedent or in a consequential position in a formula in the antecedent. But if it does, then Ll is a subformula of a formula of the sequent other than those in LQ, which is contrary to the supposition. Ll in LQ was then inserted by weakening. Let that weakening be omitted, and the sequent in question less Ll is LPC provable. LQ may then be replaced by a sequence LX containing no formula not a subformula of b or of a member of G, D, F, or Y. We then shall have the sequent

D, F, G, Y ® LL, LX, b

provable in LPC. We then may replace the proof ending with the mix above with:

D, F, G, Y ® LL, LX, b
 D, LG ® a a, F, LY ® b

MIX

D, F, LG, LY ® b

®L

LD, LF, LG, LY ® Lb

We note that the above mix might have to be followed by applications of weakening to restore occurrences of a if that formula occurs in F or LY. Under any circumstances, the new mix is of grade k and so may be eliminated by the induction hypothesis.

The situation for the same case in the system LS4° is similar and simpler. Indeed, we might give the necessary proof figures for LS4° simply by erasing all left premisses in the above ®L's, as well as the proof strings leading to them; the result is then the same as above, with the cut being eliminated. The rest of the proof follows just as in Chapter 3; there is, however, one other point to which we shall draw attention, for future reference. A point at which one might be concerned with the proof of the normal form theorem failing is at the induction step in the induction on rank, when we are examining the subcase in which the left rank is ³ 2. Here one might worry that if the rule generating the left premiss of the mix in question is ®L, it might not be able to be inverted with that mix as required for the induction, for the right premiss of the mix might introduce formulas not permitted as parameters for ®L. The solution here is the same as that for the case of the intuitionist system LIC for this subcase; the singulary nature of the succedent of the conclusion of ®L, like that of ®N and weakening in succedent for LIC, forbids that that rule be the rule generating the left premiss of the mix in this subcase, else the left rank of the mix would be 1, contrary to hypothesis. We mention this, for we shall have occasion to examine modal sequent-logics in which the conclusion of the ®L rule is not singulary, and we shall see that this fact will prevent the proof of the normal form theorem in these systems precisely at this subcase of the proof. We shall then assert:

 *13.1 The normal form theorem holds for LS3° and LS4°.

The equivalence of the systems

Before the extension of the normal form theorem to LS3° and LS4° we gave some examples of applications of LS3°'s ®L. In one of these applications, we considered the situation in which G is empty; the rule in that case becomes the ®L of LS2°, which system is then contained in LS3°. This containment establishes that all but one of the rules of inference of S2° have analogues in LS3°; this is the rule RLE, which permits us to infer a thesis a when La is provable. The reason that the analogue of this rule is not established to be in LS3° by that system's containment of LS2° is that its proof in LS2° depends on the fact that the normal form theorem holds in that system. But now we have shown that the normal form theorem holds for LS3°, and so the proof of the analogue of RLE extends as well to this system, and in just the same manner to LS4°.

As another one of our examples in the first part of this chapter, we showed that the sequent ® CLCpCqrLCLpCLqLr is provable in LS3°. But this sequent corresponds to axiom L4, the proper axiom of S3° and S4° in the systems of the last chapter. Since S2° plus L4 will give us S3°, we may assert:

 *13.2 If a is a thesis of S3°, ® a is provable in LS3°.

Let us look back now at the system we earlier called LS4°. The ®L of this system is an unrestricted version of that for LS3°; among other things, it will enable us to move from a theorem ® a to one ® La, just as the ®L of LT° does. LS4° will then contain an analogue of the unrestricted rule RL of S4°; since it is clear that whatever is provable in LS3° is provable in LS4° as well, this means that:

 *13.3 If a is a thesis of S4°, ® a is provable in LS4°.

We wish to prove the converses of *13.2 and *13.3. We may do so by showing that analogues of the LS3° and LS4° ®L rules hold in S3° and S4° respectively. Let us suppose that a formula i(D, LG ® a) holds in S4°; this formula is the interpretation of the sequent D, LG ® a, as defined in Chapters 3 and 8. It should be clear that by methods holding in the system we can move from the provability of this formula to that of i(LD, LLG ® La). But LpLLp is a thesis of S4°: Since each of the formulas of LLG is in an A-pos in i(LD, LLG ® La), SSS and LpLLp permit us to delete the initial L of each member of LLG, giving us i(LD, LG ® La) as provable. But this last formula is the interpretation of the conclusion of ®L for this case, giving us an analogue of this rule in S4°. We then have, with the above and *13.3:

 *13.4 a is a thesis of S4° iff ® a is provable in LS4°.

Let us now suppose that D, LG ® a is a sequent such that Li(D, LG ® a) is provable in S3°, and that Li(D, LG ® LQ, a), LQ as in LS3°'s rule ®L, is also there provable. Note that -- as applies in Chapter 8 to LS2° -- the provability of the necessity of the interpretation is analogous to the provability of the sequent in LS3° without the use of an ®L with premises having empty antecedent. First of all, we recall that if G is empty, this rule becomes equivalent to ®L for LS2°, which has an analogue in S3°, since S2° is a subsystem thereof. We then consider the cases in which G is not empty. Of these, look first at the situation in which D also is not empty. Here the interpretation of the right premiss is equivalent to a formula

 13.1 dCLga

and that of the left premiss to

 13.2 dCgALq1 . . . ALqna

where the q1, . . ., qn. are the n formulas of Q; but this formula implies in S3° the formula

 13.3 LALAq1 . . . qnCdCga,

while 13.1 implies

 13.4 CLgCdCga

These last two formulas meet the requirements set by metatheorem *10.7. Such being the case, *10.7 will then allow us to assert that

 13.5 Lg dCga

is an S3° thesis; this in turn gives

 13.6 LgCLdCLgLa

which even in S1° becomes

 13.7 LdCLgLa

which is equivalent to the necessity of the interpretation of the conclusion of ®L for this case. If  D happens to be empty, we shall have, instead of 13.1 and 13.2,

 13.8 Lga

and that of the left premiss to

 13.9 gALq1 . . . ALqna

respectively. It is clear that by steps paralleling those above, we can come to

 13.1 LgLa

as an S3° thesis; again, this is the necessity of the interpretation of the conclusion of ®L for this case. But then an analogue of LS3°'s ®L is a derived rule of inference in S3°, and so with the aid of *13.2 we assert

 *13.5 a is a thesis of S3° iff ® a is provable in LS3°.

Since the normal form theorem is provable in these sequent-logics, we also have:

 *13.6 LS3° (LS4°) provides a decision procedure for S3° (S4°).

Sequent-logics for S3 and S4

The systems of the preceding sections were introduced, with minor differences, in Zeman 1969. Sequent-logics for S3 and S4 were developed prior to those for S3° and S4°; for examples in the literature, see Ohnishi and Matsumoto 1957, Ohnishi 1961, Kanger 1957, Curry 1963, among others. As might be expected, LS3° and LS4° are extended to LS3 and LS4 respectively by adding to each of the former systems the rule L® as discussed in Chapter 8. It should be evident from the work of that chapter that the sequent ®. Lpp will be provable in both of these systems, and furthermore that -- by *5.6 -- an analogue of L® will hold in S3 and S4, making the interpretation of every LS3 (LS4) theorem provable in S3 (S4). Thus we have:

 *13.7 a is a thesis of S3 (S4) iff ® a is provable in LS3 (LS4).

We note that in the literature on sequent-logics for S3 and S4, a somewhat different version of rule ®L than we have employed is used. The rule ordinarily used is like ours except that it lacks the sequence D in its premises. It is clear that rule L® may be applied a sufficient number of times to D, LG ® a to get LD, LG ® a as a premiss for the mentioned modification of ®L (which, of course, requires that all formulas in the antecedent of the premiss begin with L); the mentioned modification is clearly a subcase of our rule.

The normal form theorem for LS3 and LS4

The normal form theorem for these systems may be proved as an extension of the normal form theorem for LS3° and LS4°. Again, the relevant case is the induction step in the induction on grade at the base step in the induction on rank. For LS3° and LS4° the mix formula beginning with L was inserted at this step into both premises of the mix by applications of ®L. This is also a possibility for LS3 and LS4, but the treatment of this situation is just as for the nought versions of these systems. The other possibility for these systems is that the mix formula be introduced into the left premiss by ®L and into the right by L®. For LS3, such a proof with mix of grade k + 1 and rank 2 will conclude

 D, G ® LL, a D, LG ® a

®L

LD, LG  ® La

 a, X ® Q L® La, X ® Q

MIX

LD, LG, X  ® Q

This may be replaced by

 D, LG ® a a, X ® Q

MIX

 D, LG, X ® Q L® LD, LG, X ® Q

Apply the final L® as often as needed to prefix L to each member of D.

The new mix falls within the scope of the induction hypothesis and so may be eliminated. The procedure for LS4 will be the same, the only difference being that the original proof ending will not need a left premiss for the ®L; the replacing proof ending will be identical to that shown above. In all other details the proof for the normal form theorem is the same as that for LS3° and LS4°. We then have

 *13.8 The normal form theorem holds for LS3 and LS4.

Metatheorems *13.7 and *13.8 then bring us to

 *13.9 LS3 (LS4) provides a decision procedure for S3 (S4).

A relationship between intuitionist logic and S4

We may use the sequent-logic LS4 to establish a relationship between the system IC of Chapter 2 and the modal system S4; this relationship was first established by McKinsey and Tarski 1948; the methods used there were algebraic. Let us suppose that a is a formula of IC; we shall define a translation function r as follows;

 (a) If a is a propositional variable, r(a) = La (b) r(Cab) = LCr(a)r(b) (c) r(Kab) = Kr(a)r(b) (d) r(Aab) = Ar(a)r(b) (e) r(Na) = LNr(a)

This function gives a means of translating any IC wff into a formula of S4; as examples we present the translations of the axioms of IC:

 r(C1) =  Lp LqLr  LpLq LpLr r(C2) = Lp LqLp r(K1) = KLpLqLp r(K2) = KLpLqLq r(K3) = Lp LqKLpLq r(A1) = LpALpLq r(A2) = LqALpLq r(A3) =  LpLr  LqLr ALpLqLr r(N1) =  LpLNLpLNLp r(N2) = LNLp LpLq

We shall note that the following applies

 *13.10 Where a is an axiom of IC, r(a) is a theorem of S4.

Proof of the above is simply a matter of carrying out the messy details of the individual proofs; for example, for r(C1):

 13.11 CLpCLqLrCCLpLqCLpLr PC, RL

By S3°'s  pq LpLq and S1° we go from the above to

 13.12  LpCLqLr  LpLq LpLr

and by means of Lpp and SSS, we replace CLqLr (which is in an A-pos) in 13.12 by LqLr to obtain r(C1). The proof in S4 of the remainder of the axiom translations presents no difficulty and is left as an exercise for the reader.

We now shall assume that r(Cab) and r(a) are both provable in S4. Since the first of these formulas is r(a)r(b) and strict detachment holds in S4, r(b) is also provable in S4. Thus there is an analogue under the translation we are discussing in S4 for the IC rule of detachment. We now look at the IC rule of substitution. Suppose that j(a) is the IC formula which results from the substitution p / a in j(p). Consider the S4 wff r(j(p)) and suppose that it is an S4 thesis. Let us further suppose that the substitution indicated above is such that a is a prepositional variable. Then make the substitution  p / a in r(j(p)); the L required before every occurrence of a is there as a result of having been before every occurrence of p, and the result of the substitution is r(j(a)). Suppose now that in the IC substitution a = Cbg or a = Nb. Then in the S4 formula make the substitution p / Cr(b)r(g) or p / Nr(b) respectively. Once again the resulting formula will be r(j(a)). The L required before the C or N in each case is in place already as a result of having been in place before each occurrence of p in r(j(p)). Now suppose that a in the IC substitution was Kbg or Abg. Do the substitution p / Kr(b)r(g) or p / Ar(b)r(g) respectively. Here there is still an L left over before every place where p originally stood, and so before each initial K or A in the substituted formula. These L's must be eliminated, as the connective combinations LK and LA do not occur in the range of r. Therefore note first the LK or LA combinations that stand in C-pos in the formula; by means of Lpp and SSS replace each of these by K or A respectively. Next note the formulas beginning with LK or LA that stand in A-pos. By means of KLpLqLKpq and ALpLqLApq, both of which hold in S2°, distribute the L in each case getting the formula KLr(b)Lr(g) or ALr(b)Lr(g) where before the formulas beginning with LK or LA stood. If b or g is a propositional variable or begins with a C or an N, r(b) or r(g) begins with an L, and so by S4's LpLLp strictly implies Lr(b) or Lr(g) respectively, and so by SSS the extra L may be eliminated. If b or g begins with K or A, we have it standing in A-pos and so we again distribute the L; again the new L's will precede either another L, in which case they may be eliminated, or a K or A, in which case they are distributed again. The distribution eventually must bring each distributed L 'in contact with' an L preceding a propositional variable, a C or an N; each L originally preceding a K or an A in A-pos then may be eliminated, and we have r(j(a)) provable provided r(j(p)) is: we then have in S4 an analogue under the translation of the rule of substitution for IC; since we have also an analogue of detachment and *13.10 holds, we may then assert:

 *13.11 If a is an IC thesis, r(a) is provable in S4.

Now we shall wish to prove the converse of *13.11; to this end we shall employ the sequent-logics LS4 and LIC. Let G be a sequence of IC wffs; then r(G) shall be the sequence of S4 formulas resulting from the application of r to each member of G. We shall then work to establish:

 *13.12 If  r(G) ® r(Q) is provable in LS4, then one or more of the sequents G ® q1, . . ., G ® qn, n ³ 0, is provable in LIC, where Q = q1, . . ., qn.

We shall proceed by induction on the length of the longest proof string in the proof of r(G) ® r(Q); let the number of rule applications in that proof string be n; consider first the situation in which n = 0. Here the sequent in question is an axiom, r(a) ® r(a). G ® q1 is then a ® a, which is an axiom of LIC; this establishes the base case.

Suppose now that *13.12 holds whenever n £ k. Consider the case when n = k + 1. The (k + 1)th step may be a structural rule weakening or contraction, but not cut, by *13.8. If by weakening in the antecedent, then r(a) is inserted into a sequent r(D) ® r(Q); by the induction hypothesis, one or more of the D ® qi, i between 1 and n, will be LIC provable; since G = a, D, one or more of the G ® qi is also LIC provable, by weakening in LIC. If the (k + 1)th rule is weakening in the succedent, we note first that if Q has just one member q, then G ® holds in LIC by the induction hypothesis and by weakening G ® q holds. If Q has m, m £ 1, members, the LS4 sequent in question came about by inserting r(qm) into the succedent of a sequent with n = k; by the induction hypothesis, then, one of the sequents G ® qi, i from 1 to m - 1 holds in LIC; then one or more of the set formed by adding G ® qm to this set also holds.

If the (k + 1)th step is contraction in the antecedent, then the premiss to that step is r(a), r(G) ® r(Q) where r(a) is the contracted formula and a is in G. By the induction hypothesis, one of the a, G ® qi is provable in LIC, and so by contraction there, so too will be one of the G ® qi. If this step is contraction in the succedent, then the premiss to that step is r(G) ® r(Q), r(qm) where qm. is contracted wff and is also in Q; by the induction hypothesis, one of G ® q1, . . ., G ® qm, G ® qm holds in LIC; but this is the same as saying that one of the G ® qi, i from 1 to m, holds, as required.

The (k + 1)th step may also be by a logical rule. Given the nature of the function r, it may be one of the rules for A or K, or one of the rules for L. If this step is by rule K®, then r(G) = r(Kab), r(D), which is ti say. r(G) = Kr(a)r(b), r(D); the premiss to this step is then r(a), r(b), r(D) ® r(Q). This sequent falls into the scope of the induction hypothesis, making one of the sequents a, b, D ® qi provable. By K® in LIC, then one of the sequents Kab, D ® qi (= G ® qi) is so provable. If the rule is ®K, then r(Q) = r(L), Kr(a)r(b); the premises for this rule are then r(G) ® r(L), r(a) and r(G) ® r(L), r(b); with q1, . . ., qm - 1 the members of L, this means that, by the induction hypothesis, either one of G ® qi, i from 1 to m - 1, or both of G ® a, G ® b are LIC provable; in the first case weakening and in the second ®K in LIC make one or more of G ® L, Kab provable in LIC.

If the (k + 1)th step is by A®, then G = Aab, D, and the premises of this step are r(a), r(D) ® r(Q) and r(a), r(D) ® r(Q). In LIC, then, it will be the case that one or more of the sequents a, G ® qi as well as one of the sequents b, G ® qi is provable. Let, then, a, G ® qx, and b, G ® qy, be so provable. If x = y, get Aab, G ® qx by A®; if x or y but not both = 0, insert qx or qy as appropriate by weakening in the empty succedent, and apply A® as above. If x ¹ y and neither is 0, use ®A to get a, G ® Aqxqy and b, G ® Aqxqy as provable in LIC; an application of A® now gives us Aab, G ® Aqxqy. as provable. Now, it is the case that in LIC a sequent of form :X ® Agd is provable iff one or both of X ® g and X ® d is provable. Thus one or both of Aab, G ® qx and Aab, G ® qy are provable, and since x and y are £ m, one or more of the Aab, G ® qi are provable, as required. If the (k + l)th step is by ®A, then Q = L, Aab and the premiss of the rule application is r(G) ® r(L), r(a), r(b), with L = q1, . . ., qm - 1,. By the induction hypothesis then one of the sequents G ® qi, i from 1 to (m - 1), or G ® a, or G ® b is provable. But as we have noted, this is equivalent to saying that one of the sequents G ® qi, i from 1 to (m - 1), or G ® Aab is provable, as required for *13.12.

The (k + 1)th step may also be by one of the L rules. First let us consider the possibility that the rule, L® or ®L, involves a side formula which is a propositional variable. This side formula was introduced into the proof originally either as part of an axiom or in a weakening step. If p was introduced by a weakening step, introduce instead Lp at that point; the L-introduction rule earlier assumed to introduce Lp is then unnecessary unless that step was ®L with premiss D, LG ® p and conclusion LD, LG ® Lp. In this case the new proof would not be reduced to k steps unless D were empty, for L® would have to be applied as often as necessary to prefix L to each member of D. To handle this situation we note that LS4 could have been formulated with a version of ®L in which D is always empty. All other details of the current proof will follow through in that version, and the present difficulty does not arrive. Thus, whenever a variable introduced by a weakening step is later prefixed by an L, the proof in question may be shortened as required by the induction hypothesis. If a variable later prefixed by an L is originally introduced as part of an axiom, we note the following. In LS4, every proof may be replaced by one with the same conclusion, but beginning only with axioms ai ® ai where ai is a propositional variable. Suppose otherwise; then there is a proof with an axiom b ® b at the top of one of its branches which sequent cannot be the conclusion of one of the LS4 rules and having b beginning with a connective; but examination of LS4's rules shows that every provable sequent which contains a connective can be the conclusion of a rule application, contrary to the hypothesis. Every proof of LS4, then, can begin only with axioms containing no connectives. But the special subclass of LS4 provable sequents we are now considering contains only formulas in the range of the function r; in such formulas every variable is prefixed by an L. Considering the L and its variable as a unit, we may apply the above argument to show that every sequent of this subclass is provable in a proof beginning only with axioms of form Lai ® Lai, where ai is a variable. So we begin the proof in question with Lai ® Lai instead of ai ® ai and omit the (k + 1)th (L-introducing) rule. Again, there is a problem in our formulation if that rule happens to be ®L with premiss D, LG ® p, where p = ai; again, we handle this problem by noting that we could have used the equivalent formulation in which D in this rule is always empty. We note, then, that whenever the (k + 1)th step is an L rule and the side formula is a propositional variable, the proof may be shortened to bring it under the induction hypothesis.

The other possibilities when the (k + l)th step is an L rule are that the L is prefixed by that rule to a formula beginning with a C or with an N. Suppose, first of all, the former, and suppose that the L rule in question is L®. The antecedent G of the LIC sequent for which the value of r is the (k + 1)th step of our LS4 proof is then Cab, D. The premiss of the L-introduction in question then is Cr(a)r(b), r(D) ® r(Q). This sequent, because of the initial C, contains a formula not in the range of p. But it itself is derivable by a C® whose premisses are r(D) ® r(Q), r(a) and r(b), r(D) ® r(Q), both of which are in the range of r and for which n is less than k. By the induction hypothesis, then, one or more of the sequents D ® a and D ® qi, i from 1 to m, as well as one or more of the sequents b, D ® qi, i from 1 to m, is LIC provable. Suppose that one of the D ® qi holds. Then, simply by weakening, one of the Cab, D ® qi holds as well, as required. Suppose, on the other hand, that D ® a holds. Since one of the b, D ® qi holds, we may use it and D ® a as premises for C® to obtain the required sequent as provable.

Suppose again that the L rule involved is L®, and that the side formula for that step begins this time with N. G (in LIC) is then Na, D, and the premiss of the L-introduction is Nr(a), r(D) ® r(Q). Again, it does not fall into the range of the function r, but the proof is again invertible so that the premiss leading-to the premiss of the L-introduction is the sequent r(D) ® r(Q), r(a); this is in the scope of the induction hypothesis and in the range of the function r, so one of the sequents D ® qi, i from 1 to m, and D ® a is LIC provable. If one of the former, insert Na by weakening to obtain one of the sequents Na, D ® qi as provable. If the latter, then apply N® first to get Na, D ®; this sequent qualifies, although any of the qi; may now be inserted right by weakening.

We have been considering the cases in which the L in question is introduced by L®, and so is on the left; it is possible that L be introduced on the left by ®L in our formulation; we shall here appeal as before to the fact that the system can be formulated with a postulated ®L which introduces no L's on the left to argue that we need not consider this situation.

Now suppose that the L in question is introduced on the right, by ®L. Since this rule demands a singulary succedent, Q is precisely Cab or Na. If Cab, then the premiss of the ®L is r(G) ® Cr(a)r(b) (note that we have D empty here by the same argument given in the last paragraph); this last sequent can have, by appropriate inversions, r(a), r(G) ® r(b) as its premiss. This sequent is in the range of p and is provable in fewer than k applications; a, G ® b is then LIC provable (note that if a, G ® is provable, we add b by weakening), and so we get G ® Cab in LIC by ®C. If Q is Na, we have r(G) ® Nr(a) and so r(a), r(G) ® provable in k or fewer steps. Thus a, G ® holds in LIC, and by ®N we then have the required G ® Na. If, then, r(G) ® r(Q) is provable in LS4, we shall always have one or more of the sequents G ® bi, i from 1 to m, provable in LIC; so * 13.12 holds, and we have, by this and *13.11:

 *13.13 a is a thesis of IC iff r(a) is provable in S4.

We note that McKinsey and Tarski established that the same relationship holds between PC and S5; it also holds for a number of systems intermediate between IC and PC to respective systems intermediate between S4 and S5.

Sequent-logic for S5

We shall now develop a sequent-logic for the system S5; this formulation was originally due to Ohnishi and Matsumoto 1957. As we shall see, it differs in an important respect from the systems we have been studying till now. The system LS5 will be based upon LPC and will have the rule L® as we have been employing it for the 'non-nought' sequent logics. In addition it will have the following version of ®L:

 D, LG ® LQ, a ®L LD, LG ® LQ, La

It will be noted that this rule permits a multiple succedent, one with more formulas than one, provided the formulas in that succedent which are parametric begin with L. If  Q is empty, the rule becomes ®L of LS4°; LS5 then contains LS4; further, note the proof:

 Lp ® Lp ®N ® Lp, NLp

®L
® Lp, LNLp

N®
NLNLp ® Lp

®C, Df. M
® CMLpLp

®L
® MLpLp

It is evident then that:

 *13.14 If a is an S5 thesis, then ® a is provable in LS5.

Let us now consider this version of ®L from the point of view of S5. If d is the conjunction of the formulas of D, g the conjunction of the formulas of G, and qL the disjunction of the formulas of LQ, the interpretation (in the sense in which we have been using that term to relate the sequents of a Gentzen system with ordinary formulas) of the premiss of ®L is equivalent in S5 to the formula CdCLgAqLa. This in turn is equivalent (by PC methods) to CKLgNqLCda. In *11.1 it has been shown that *10.5 applies to S5 as follows: if Cab is an S5 thesis and if each of a's variables is in the scope of a modal operator belonging to a, then CaLb is an S5 thesis. But every variable of KLgNqL is in the scope of such a modal operator, and so we are able to infer to CKLgNqL da., which in S1° yields CKLgNqLCLdLa.; by PC this last gives CKLgLdAqLLa.. This formula is, of course, equivalent to the interpretation of the conclusion of LS5's ®L rule. We then conclude that if a given sequent is provable in LS5, its interpretation is a thesis of S5, and with *13.14 this gives us

 *13.15 a is an S5 thesis iff ® a is provable in LS5.

We have remarked that LS5 differs from the other sequent-logics we have been studying in an important respect. The most obvious respect so far in which it differs from them is that its ®L has parametric formulas in its premiss's (and its conclusion's) succedent. This leads to a significant thing -- the normal form theorem is not provable in LS5. Specifically, we shall refer to the induction step in the induction on rank in that proof (see Chapter 3), and in that step to the subcase in which the left premiss of the mix to be eliminated is generated by a rule application with the mix formula parametric in its succedent, and the left rank of this mix is, of course, ³ 2. As we noted in our discussion of the normal form theorem for LS3° and LS4°, the case in which this rule -- the one generating the left premiss for the mix of this subcase -- is ®L is excluded for this subcase, for otherwise the left rank would have to be 1, which is contrary to the hypothesis. But for LS5 we must consider ®L as a possibility for the generator of the left mix premiss. Suppose we had a proof (at this subcase) ending thus (with mix formula La):

 LG  ® LQ, b ®L LG  ® LQ, Lb
D ® L

MIX

LG, DLa  ® LQLa, L, Lb

If we attempt to bring the mix into the scope of the induction hypothesis by doing it before the ®L, we mix the premiss of the ®L with the right premiss of the mix, getting LG, DLa  ® LQLa, L, b. To this must be applied ®L to prefix the necessary L to b -- but there is no guarantee that the formulas of DLa and L begin with L as required for the application of this rule. A specific example of such a proof is

 Lp ® Lp ®N ® NLp, Lp

®L

® LNLp, Lp

 p  ® p ®L Lp® p

MIX

® LNLp, p

Mixing before the ®L would require us to apply ®L to ® NLp, p, which is not permitted. Note also that the left rank of the mix cannot be lowered here by inverting the introduction of the mix formula Lp with the rule following it, as its introduction here is as part of an axiom. So the proof of ® LNLp, p requires the use of mix or cut.

This is a drawback if we think of sequent-logics themselves as providing decision procedures for our logics. But in spite of the fact that the normal form theorem is not here provable, the system LS5 is quite useful to us. We shall see in the next chapter that LS5 will provide a bridge for us between the proof theory and the semantics of S5, just as our sequent-logics for the absolutely strict systems did for them. Indeed, we shall eventually investigate a number of systems which like S5 have sequent-logic versions for which the normal form theorem is not provable, but which provide us with a very natural bridge between semantics and syntax.