IN appendix II to SL, Lewis and Langford assign the names S1 through S5 to the systems which we have been calling thus. (Several modal formulas which, as it turns out, extend various of these systems to systems not among the systems S1S5 are mentioned there, but are not discussed in much detail.) One of the earlier attempts to extend this list of Lewismodal systems was made in Parry 1939. As an aside to the main thrust of that paper, Parry suggests that we might formulate a system presumably properly between S4 and S5 (by 'properly between' we understand 'contained in the one and containing the other, but identical to neither') by adding to S4 the additional axiom
M10¢. LMLpLp
This should have the effect of identifying the modalities L and LML (and so by duality M and MLM) and the resulting system then should have as nonequivalent irreducible proper modalities L, ML, LM, M, and their negations. Parry proposed the name 'S4.5' for this system. We note that M10¢ is clearly in S5 and not in S4 (by the nonequivalence of L and LML in the latter system. S4.5 then contains S4 properly (i.e. without being equivalent to it)  but is it contained properly in S5? The answer is negative  see for example Dummett and Lemmon 1959. We show this as follows; do p / CMLpLp in M10¢, with = LC:
15.1  LMMLpLpMLpLp 
As a typical S4 thesis we have
15.2  CMLpLpMLpLp 
In S1 we have
15.3  CLMLpMLp 
In S1° we have (derivable, say from 5.74)
15.4  CCLpMqMCpq  
15.5  MCMLpLp  D(15.4)(15.3) 
15.6  MMLpLp  15.5, 15.2, SSS 
15.7  LMMLpLp  15.6, RL 
15.8  MLpLp  D(15.1)(15.7) 
We see then that if we assume M10¢ as an axiom in addition to S4, we are able to derive M10, the proper axioms of S5. Parry's S4.5, then, is not properly contained in S5, but is equivalent to it.
The question of a system properly between S4 and S5 did not seem to receive too much attention for a number of years following Parry 1939. In the mid 1950s, Arthur Prior began investigating a system he called the 'Diodorean modal system'. In this system, necessity and possibility are defined semantically in terms of time; a statement is taken to be necessary iff it is true now and at every future instant, and a statement is taken as possible iff it is true either now or at some future instant (we shall have more to say about this approach to modality). Regardless of what we think of this notion of possibility and necessity, we can see that certain formulas expressible in the notation we have been using may be considered valid, or universally true, in the semantics thus defined. All PC theses would, first of all, be valid in this framework; the PC would be taken as the logic of any given instant, without reference to future instants. CLpp, given the above definition of necessity, would say that 'If p is true now and ever after, then p is true (now)'; CLCpqCLpLq would say that 'If p implies q now and forever, and p itself holds now and forever, then so does q'. Both interpretations of formulas here given are easily seen to be true. And if a formula is provable as a matter of logic, one would be justified in saying that it too is true now and forever; thus, if a is a thesis, La would be said to be valid. We thus have as valid within Prior's Diodorean system formulas and rules which form a basis sufficient for at least the system T. But we can go further; suppose that a statement p is true now and forever after. What then of the statement Lp? Well, clearly, Lp is true now  this is its very definition; but it also will be true at the moment following this one, at the moment following that, etc.; indeed, Lp will also be true now and forever; the formula CLpLLp will then be valid in this semantic system, and Prior's Diodorean semantics now validates systems sufficient to serve as a base for the system S4. Prior 1955 notes this fact, but (as Prior 1958 notes) Prior 1957 goes a step further and makes the claim that the Diodorean semantics is characteristic of the system S4, that is, that all and only the formulas valid in the Diodorean semantics (taken with an infinite number of instants) are the theses of S4. As it turns out, this is not the case; counterexamples to Prior's claim were quick to come. Dummett 1959 sets down a propositional calculus called LC which is properly between our IC and our PC. As we have shown in Chapter 13, there is a translation which can be established between formulas of the propositional calculi and modal formulas such that if a is a propositional calculus formula and r(a) is its modal translation, then a is provable in IC iff r(a) is provable in S4; also, a is provable in PC iff r(a) is provable in S5. Dummett's LC contains formulas which are theses of PC but not of IC (one example is ACpqCqp which, indeed, added to IC yields LC) which when added to IC do not extend it to PC but to a system properly between IC and PC. And, as it turns out, if a is such a formula, the addition of r(a) to S4 will produce a system properly between S4 and S5. As it turns out, r(ACpqCqp) is the formula ALpLqLqLp. This last formula is one that turns out to be valid in Prior's Diodorean semantics. But it plus S4 will, by the above, produce a system properly containing S4. Other such formulas were noted in Dummett and Lemmon 1959 and the systems formed by adding them to S4 were studied there.
If we examine a typical model formed by the rules of the model structure MS4, we shall see that the reflexive, transitive accessibility relation of that system has partially ordered the worlds of that model. This means that the model may be viewed as a geometrical tree in which branchings may occur. The model considered as a tree here differs from the tree produced by the branching of 'split' rules (analogous to the branching of twopremiss rules in the sequentlogics). The branching here is a branching of 'strings' of possible worlds. A world w may be accessible to me before I choose to go down one path rather than another at a branching, but after I make that choice in MS4, w may no longer be accessible. If, as we have suggested above, we view possible worlds as instants in time and the accessibility relation as the relation of 'being no earlier than', MS4 gives us a universe of branching time. There are possible worlds, or states of affairs or future instants which are accessible to me now, but which may, because of intermediate events, become inaccessible to me some time in the future. But it is possible to think of other kinds of ordering than the simple partial ordering in the S4 models. The ordering suggested by Prior for the worlds or instants in the models for the Diodorean system is more than a partial ordering; indeed, it is a total ordering. For any possible worlds w1 and w2 in such a model, either w1 has access to w2 or w2 has access to w1 or both (in which case w1 = w2). We call attention now to the formula
M11. ALpqLqp,
which is equivalent given S4 to the earliermentioned formula ALpLqLqLp. This formula corresponds by the translation earlier mentioned to ACpqCqp, the proper axiom of the system LC of Dummett 1959; this last formula is an 'axiom of connexity', corresponding to the settheoretical (a Í b) Ú (b Í a). Might there be a connection between M11 and the linear, connected nature of Diodorean models? Indeed there is such a connection. We now define a system called S4.3, which was first studied in Dummett and Lemmon 1959; S4.3 = S4 + M11. As an intermediary to the study of S4.3 models, let us also define a sequentlogic which will correspond to S4.3. This system, LS4.3, will differ from the systems we have been studying in that it will have a special axiom schema in addition to that of LPC; as with LS5, we shall be unable to prove the normal form theorem here. We add the following to LS4 to get LS4.3:
15.9  LALab, LAaLb ® La, Lb 
We wish to show that the interpretation of the above sequent is a thesis of S4.3. Let us do this by showing that there is a deduction in S4.3 corresponding to
15.10  LALpq, LApLq ALpLq 
We shall first write the hypotheses of the above:
15.11  LALpq  Hyp. 
15.12  LApLq  Hyp. 
Even in S1° these become respectively
15.13  NqLp  
15.14  NpLq 
Axiom M11 plus these last two formulas and SSS gives
15.15  ANqqNpp 
which in S1° is equivalent to
15.16  ALpLq 
We see then that 15.10 holds for S4.3 and so the interpretation of 15.9 will hold there, and so
*15.1  If ® a is provable in LS4.3, a is a thesis of S4.3. 
We shall now set down. a model structure to correspond to S4.3. This will be called MS4.3, and its accessibility relation will be like that of MS4 in being reflexive and transitive; in addition, as we have indicated, it will also be connected. For any two worlds w1 and w2, either w1 has access to w2 or vice versa. The statement of rules for this system will be basically as for MS4, with exceptions to be noted. Let us now examine the tableau construction in this structure for the tableau beginning with ALpqLqp on the right. The first operation is an Ar, giving
ALpqLqp  
Lqp  
Lpq 
Because of the nature of this model structure, we shall require here a different strategy from that used in MS4. We have here two formulas on the right beginning with L; in MS4 we should develop each of these on its own, that is, we should apply Lr independently to each in our search for a countermodel, and it would turn out that each resulting tableau would fail to close, giving us a 'branching' countermodel, one branch arising from Lqp and the other from Lpq. In MS4.3 too we may think of each of the formulas on the right and beginning with L as giving rise to an auxiliary tableau  say Lqp gives t1 and Lpq gives t2. But given the nature of the accessibility relation in MS4.3, either t1 must be accessible to t2 or t2 to t1. We can handle this situation by thinking of our tableau construction as splitting alternatively; one of the alternative sets will have t2 auxiliary to t1 with all that implies and the other will have t1 auxiliary to t2. Each of these sets offers a possibility for finding a countermodel:





We may now perform Cr in each of the new alternative tableaux; our Ll rule will then have us transfer Lq and q in the one alternative set from t1 to t2 and Lp and p from t2 to t1 in the other:




Both alternative sets close, and so ALpqLqp is valid in MS4.3 by the above and *9.1. By this structure's containment of MS4, then, we have
*15.2  If a formula is provable in S4.3, then it is valid in MS4.3. 
We shall now investigate in greater detail the rule Lr as it functions in MS4.3. If there are n different formulas beginning with L on the right of an MS4.3 tableau, this rule would have us investigate situations involving n specific auxiliary tableaux. Where La_{1}, . . ., La_{n} are the n formulas involved, the n tableaux would be those respectively specified as having a_{i}, i from 1 to n, on the right. But since our models must be connected, with i and j between or equal to 1 and n, the ith tableau must be auxiliary to the jth or vice versa. Since there are n! permutations of these n tableaux, there will be n! possible situations of mutual auxiliarity to be considered. The tableau with n L's on its right will split, then, into n! tableaux, each of which will have auxiliary to it one of the n! possible arrangements of auxiliary tableaux (each of which is an attempt to construct a countermodel). There is an orderly way in which we can handle this situation in the general case of application of rule Lr. Do it as follows:
Lr(4.3):  Where La_{1}, . . ., La_{n} occur on the right of an MS4.3 tableau, split that tableau into n tableaux, each one having auxiliary to it a tableau with a different one of the a_{1}, . . ., a_{n} on its right; the auxiliary tableau with a_{i} on its right, 1 £ i £ n, will also have the set of formulas La_{1}, . . ., La_{n} less La_{i} on its right. 
If this rule is applied to a tableau having n formulas beginning with L on the right, the alternative set to which that tableau belongs will split into n alternative sets, each ending with a tableau having (n  1) formulas beginning with L on the right. If Lr(4.3) is applied in turn to the final tableau of each of these n sets, the result will be a total of n(n  1) alternative sets. If the procedure is carried out with each of these sets, and with each resulting set, etc., the final result is a construction with n! alternative sets, each ending with a tableau having no L's (from the original tableau) right. It will be noted that these n! sets are precisely those required by the connexity of models in this system. The first phase of application of our Lr will put into each of the n tableaux which respectively conclude each of the n alternative sets a different one of the a_{i} (from La_{i} of the original tableau); the n  1 alternative sets resulting at the second phase of application of Lr for each of the n abovementioned sets will have a different one of the a_{1}, . . ., a_{n} (less a_{i}) in their latest tableaux; each such tableau will then contain n  2 formulas beginning with L. The procedure is repeated through n phases, at which point there will be n! alternative sets beginning with the original tableau and having n auxiliary tableaux each. Each alternative set corresponds to one of the permutations of a_{1}, . . ., a_{n} and all such permutations are included. The construction then covers all possibilities of mutual accessibility of the auxiliary tableaux which can arise from the formulas beginning with L on the right of the main tableau. It is clear that with Lr(4.3) as stated here, *15.2 holds.
We now move on to another metatheorem:
*15.3  If a formula a is valid in MS4.3, then ® a is a theorem of LS4.3 
We shall indicate how to show that there is a principle in LS4.3 corresponding to rule Lr(4.3) as stated above, and so that *15.3 holds. Where n (the number of L formulas on the right) = 1, the rule is the Lr of MS4. When n = 2, the special axiom schema for LS4.3 gives us our result as follows. In this case there are two alternative sets resulting from the application of Lr(4.3). The final sequents of the segments of proof corresponding to the first tableaux in these respective sets are of form G, LG ® La, b and G, LG ® a, Lb. We then do




LG ® La, Lb 
The above figure establishes that there is m LS4.3 a principle corresponding to the inverse of Lr(4.3) when that rule is applied with two formulas on the right beginning with L. We wish to show that there is such a principle in that sequentlogic in the general case, when there are any number of formulas beginning with L on the right. We do so by establishing a generalized version of the special axiom schema for LS4.3. First of all, let the notation
15.17  Ú (a_{i}, 1/n) 
represent the sequence whose n members are:
1st  the disjunction of the formulas a_{2}, . . ., a_{n }(a_{1} is excluded) 
2nd  the disjunction of the formulas a_{1}, . . ., a_{n }(a_{2} is excluded) 
...  
ith  the disjunction of the formulas a_{1}, . . ., a_{n }(a_{i} is excluded) 
We may assume that n ³ 3, for the case in which n = 2 is our special axiom. Developing our notation further, let j(b) be an S4.3 wff having b as a subformula; then
15.18  j(Ú (a_{i}, 1/n)) 
is the sequence whose ith member, 1 £ i £ n, is formed by replacing b in j(b) by the disjunction of the n  1 formulas a_{1}, . . ., a_{n} excluding a_{i}. As induction hypothesis for our generalization, we then assume that the sequent
15.19  LAp_{i} Ú (Lp_{i}, 1/k) ® Lp_{1}, . . ., Lp_{k} 
is a theorem of LS4.3. This sequent may also be represented as
15.20  LAp_{i}ALp_{k} Ú (Lp_{i}, 1/k  1), ALp_{1} . . . ALp_{k}_{  1}p_{k} ® Lp_{1}, . . ., Lp_{k} 
Let us first of all take p_{k} in the above as the formula ALp_{k}p_{k}_{ + 1}.
15.21  LAp_{i}ALALp_{k}p_{k + }_{1} Ú (Lp_{i}, 1/k  1), ALp_{1} . . . ALp_{k}_{  1}ALp_{k}p_{k}_{ + 1} ® Lp_{1}, . . ., LALp_{k}p_{k}_{ + 1} 
Then let us take p_{k} in 15.20 as the formula Ap_{k}Lp_{k}_{ + 1}
15.22  LAp_{i}ALAp_{k}Lp_{k}_{ + 1} Ú (Lp_{i}, 1/k  1), ALp_{1} . . . ALp_{k}_{  1}Ap_{k}Lp_{k}_{ + 1} ® Lp_{1}, . . ., LAp_{k}Lp_{k}_{ + 1} 
We note that the sequent LAp_{k}Lp_{k}_{ + 1}, LALp_{k}p_{k}_{ + 1} ® Lp_{k}, Lp_{k}_{ + 1} is in the axiom schema proper to LS4.3. With this axiom schema, cut, and 15.21 and 15.22, then, we may prove the sequent
15.23 

We note that the sequents ALp_{k}Lp_{k}_{ + 1} ® LAp_{k}Lp_{k}_{ + 1} and ALp_{k}Lp_{k}_{ + 1} ® LALp_{k}p_{k}_{ + 1} hold in LS4. The formulas forming the succedents of these two sequents are in Cpos in formulas in the antecedent of 15.23; by a sequentlogic analogue of SSS we shall be able to replace both these formulas in 15.23, then, by ALp_{k}Lp_{k}_{ + 1}. Contracting the resulting duplicated sequence, then, we get:
15.24 

But this sequent may be represented as
15.25  LAp_{i} Ú (Lp_{i}, 1/k  1) ® Lp_{1}, . . ., Lp_{k}_{ + 1} 
which is the generalized version of our special axiom. As an example of this sequent, with, say, the number of formulas in the succedent = 4, we should have the sequent
15.26  LApALqALrLs, LALpAqALrLs, LALpALqArLs, LALpALqALrs ® Lp, Lq, Lr, Ls 
When we have a situation in the application of Lr(4.3) in which there are n formulas beginning with the operator L on the right of the tableau in question, the final sequents in the segments of LS4.3 proof corresponding to the first tableaux in the n alternative sets resulting from the Lr(4.3) are then sequents
G, LG ® a_{1}, La_{2}, . . ., La_{n}  
. . .  
LG ® La_{1}, . . ., La_{n  1}, La_{n} 
We may use ®A, ®L, cut, contraction and the generalized version of our axiom just as we used those rules and the original version of the axiom to prove the correspondence in the case above in which n = 2. The result would be a sequent
15.27  LG ® La_{1}, . . ., La_{n} 
which corresponds to the state of the tableau in which the Lr(4.3) was applied at the time that it was applied. We then conclude that in the general case we have an analogue in LS4.3 of MS4.3's rule Lr. This means that *15.3 is established. By this last metatheorem, *15.1, *15.2, and *9.1, then, we have
*15.4  A formula a is valid in MS4.3 iff ® a is provable in LS4.3, and so also iff a is a thesis of S4.3. 
By *9.2, then
*15.5  MS4.3 provides a decision procedure for S4.3.MS4.3 provides a decision procedure for S4.3. 
We now turn to a system intermediate between S4 and S4.3; this is S4.2, which was also discussed in Dummett and Lemmon 1959. S4 models may branch while S4.3 models are linear  but S4.2 models are something of a compromise between the two. Branching is permitted, but each S4.2 model has a property which is most simply expressed in terms of the accessibility relation U as follows
15.28  (x)(y)(z)(Uxy . Uxz . É ($w)(Uyw . Uzw)) 
If two worlds are accessible to a common world, they have a common world accessible to them. Models for S4.2, then, are convergent, though not necessarily connected (convexity is a limiting case of convergence). If the formula MLa holds, it means that a will, in some world now accessible to us, become necessary. In an S4 model, MLa can hold in the real world without holding in every world; « may become necessary along one branch of the model, but fail to do so along another. If we wish to assert in an S4 framework that a will become necessary eventually, no matter what happens, we should have to assert LMLa. In the convergent models for S4.2 this is not necessary, for if two worlds are accessible to the real world, then they have a common world to which they have access, which by the transitivity of the accessibility relation is accessible to the real world. If MLa holds in the real world, then, no branch can be found along which a fails to become necessary. Involved in S4.2, then, is a collapsing of part of the modal structure of S4 by the identification of LML and ML with each other and of their duals MLM and LM with each other. We could use
15.29  MLpLMLp 
as an axiom for S4.2; we shall instead use the shorter
M12. MLpLMp
which with p / Lp by LpLLp and SSS in S4 gives us 15.29. We note, by the way that if we apply *5.4 to M12 we get
15.30  LpMp 
which is then provable in S1° + M12 even without Lpp..
As we have informally indicated, S4.2 is contained in S4.3:
15.31  LALpqLqp  M11, RL 
15.32  MKLpNqLqp  15.31, S1° 
15.33  MKLpNMNpLMNpp  15.32, q / MNp 
15.34  MLpNpMLp  15.33, S1° 
15.35  MLpNLpMLp  15.34, S4 
15.36  NLpMLpMLp  S2° 
15.37  MLpLMLp  15.35, 15.36, SSS 
We thus have formula 15.29, which in S1 gives us M11, and S4.2 is in S4.3.
We shall establish a sequentlogic for S4.3; let LS4.2 be the sequentlogic resulting from the replacement of LS4's ®L by
D, LG ® LNLQ, a 


®L 
LD, LG ® LNLQ, La 
LNLQ, of course, is formed by prefixing LNL to each member of the sequence Q. The resemblance of this rule to the ®L for LS5 will be noted. We note that the interpretation of the premiss of this rule will be equivalent to
15.38  CKdLgA(LNLQ)_{A}a, 
where d and g are the conjunctions of the formulas of D and G respectively, and (LNLQ)_{A} is the disjunction of the formulas of LNLQ. 15.38 is PC equivalent to
15.39  CdCLgCN(LNLQ)_{A}a. 
By PC, N(LNLQ)_{A} is equivalent to (MLQ)_{K}, which is the conjunction of the members of LNLQ each prefixed by an N. By this fact and CMLKpqKMLpMLq, which holds in S1°, 15.39 yields
15.40  CdCLgCMLqa. 
where q is the conjunction of the members of Q. Applying RL to 15.40 and then distributing the L we get
15.41  CLdCLLgCLMLqLa. 
The LL in the above may be replaced by L in S4; since CMLpLMLp holds in S4.2, we may replace LMLq by MLq to get
15.42  CLdCLgCMLqLa. 
We now note the following deduction in S4.2:
15.43  LpCLqLKpq  S2° 
15.44  MLpMCLqLKpq  15.43, S3° 
15.45  MLpCLLqMLKpq  15.44, S2° 
15.46  LMLpLLqMLKpq  15.45, S3° 
15.47  LMLpCMLLqMMLKpq  15.46, S2° 
15.48  LMLpCMLqMLKpq  15.47, S4 
15.49  MLpCMLqMLKpq  15.48, 15.18, S1° 
15.50  KMLpMLqMLKpq  15.49, S1° 
Therefore we see that the distribution of ML over conjunction in S4.2 will be an equivalence. This, along with PC methods, converts 15.42 to
15.51  CLdCLgA(LNLQ)_{A}La, 
which is PC equivalent to the interpretation of the conclusion of ®L for LS4.2. We shall then be able to say:
*15.6  If ® a is a theorem of LS4.2, a is provable in S4.2. 
We might remark, by the way, that the above deductions indicate that a formula beginning with ML is completely modalized in S4.2 in the same sense that one beginning with L is completely modalized in S4. This indicates that S4.2 is a 'step' in the family of complete modalized systems.
We shall now discuss two versions of a semantics for S4.2. One of these shall be called MS4.2, and was proposed in essence by Lemmon. Here the rules all operate as with MS4, with one exception. When there are more formulas than one beginning with L on the right of a tableau, the rule Lr will prescribe the creation of an auxiliary tableau for each of them, giving us in effect a 'branching' or 'divergence' of tableaux in the same alternative set. Formula 15.28 specifies that when this occurs we must have available a tableau auxiliary to all such divergent tableaux resulting from a common tableau; this is a tableau of 'convergence'. We then specify that the rule Ll be altered so that when we have a divergence and no other steps can be taken in any branch of that divergence, a new tableau (that of convergence) be constructed auxiliary to all the tableaux in the branches of the divergence, and where La is any formula beginning with L and occurring left in one of these tableaux, a be written left in the tableau of convergence. As an example, consider the tableau construction beginning with CMLpLMp on its right. Execution of the PC steps and the Lr steps required gives us:



If we were constructing an MS4 model, our work would now be complete; we should have a countermodel to CMLpLMp. The requirement for convergence in MS4.2, however, requires the construction of a tableau auxiliary in common to each of the two lower tableaux above:




The Np, of course, comes from the left of the divergent tableaux, and the p (on the left of the last tableau) from the right divergent tableau. Given the convergence, then, this tableau construction closes. Since all the theorems of S4 will be valid in MS4.2 and since S4 + CMLpLMp gives S4.2, we may then assert (given *9.1):
*15.7  Every theorem of S4.2 is valid in MS4.2. 
The reader may take as an exercise the demonstration that ALpqLqp, the axiom for S4.3, is not valid in this model structure. We shall now examine a slightly different version of the semantics for S4.2. It will be called MS4.2¢, but it will be based upon the accessibility relation as employed above. Suppose we follow down the left branch of the divergence in the above construction. LNLNp causes NLNp to be carried into the auxiliary tableau on that branch  but what is the status of the formula LNLp (which causes construction of the right branch) in the world corresponding to that auxiliary tableau? If LNLp is to be falsified in the main world, then there must eventually be a world accessible to the main world and to the world corresponding to the auxiliary tableau beginning with NLp right in which p becomes necessary, in which Lp holds. By the requirement of convergence, then, there must be a world accessible to the world represented by the auxiliary tableau of the left branch in which Lp holds; NLp must then be falsified in a world accessible to that world, and so LNLp must fail there as well as in the main world. We should then be justified in writing LNLp on the right of the auxiliary tableau in the left branch in addition to the formula NLNp. We shall use this fact as the basis for the structure MS4.2¢; as an alternative to constructions involving branching and converging explicitly in MS4.2, we might employ the following version of the rule Lr (and leave the rest of the structure as in MS4):
Lr(4.2¢):  When the formulas LNLQ, La are all the formulas beginning with L on the right of an MS4.2¢ tableau, construct a tableau auxiliary to that tableau and having LNLQ and a on its right. 
We may use the formula CMLpLMp as an example to illustrate how evaluation in MS4.2¢ proceeds; begin a construction with a tableau having CMLpLMp (CNLNLpLNLNp) on its right, and use the above Lr as appropriate:





The Np left in the above closing construction comes from the LNp in the middle tableau; the p left in the last tableau comes from the Lp left in that tableau. It will be seen that CMLpLMp is then valid in MS4.2¢. It may be seen further that the version of Lr given above parallels exactly the rule ®L for LS4.2. We comment at this point that the rule cut is not redundant in LS4.2 (try, for example, to prove ® LLNLp, LLNLNp); therefore, we must explicitly assume in MS4.2¢ a 'cutlike' rule such as that employed in MS5. With the help of *15.6, then, we may state
*15.8  A formula a is valid in MS4.2' iff ® a is provable in LS4.2 and so also iff a is a thesis of S4.2. 
At this point we run into a problem, not  we trust  in theory, but in execution. The next stage of our study of S4.2 would be to show that if a formula is valid in MS4.2, then it is valid in MS4.2¢. This problem has proved to be rather difficult to crack; that validity in MS4.2 implies validity in MS4.2¢, then, we leave for the present a conjecture (given the methods we have been here employing). And this also then will be the status of the assertion of the absolute equivalence of MS4.2, LS4.2, S4.2, and MS4.2¢.
As a final note on S4.2 at this time, we may show that that system does not contain S4.3 by showing that ALpqLqp is not valid in MS4.2. A tableau beginning with this formula right will close iff one with Lpq and Lqp as its right formulas closes. To such a tableau, we apply MS4.2's rule Lr, giving two auxiliary tableaux:



After the indicated Cr's have been performed, we have formulas Lp and Lq left in the respective auxiliary tableaux; although convergence requires that there be a tableau in which, then, p and q are both true, this is a consistent assignment and a countermodel has been found.
We noted earlier that other formulas than those of S4.2 and S4.3 are verified by Prior's Diodorean semantics. One of these is the rather curiouslooking
M13. pLppCMLpp
Another closely related formula is
M14. pLpLpCMLpLp
Let us examine the status of M13 in our model structure MS4.3; a countermodel for M13 will exist there iff the tableau construction beginning with a tableau having pLpp left and the formulas p and LNLp right closes. We first execute Ll within the main tableau and then apply Cl to the resulting tableau:
pLpp  p  
LNLp  
CpLpp  

(closes) 
We note that the tableau resulting from the placement of p left closes. We now have an unclosed tableau with LNLp and pLp right. Following MS4.3's procedure, this means that we split this tableau and construct tableaux auxiliary to each of the resulting tableaux as follows





The leftmost of these auxiliary tableaux will have an auxiliary tableau in turn which will look like this:




This tableau closes; the Lp on the left is written there as a result of the Lp left in the above tableau. This leaves the tableau shown on the right above; in this case again we get a split of tableaux each of which takes an auxiliary tableau by MS4.3's Lr:





We note that the rightmost tableau closes. So far as the other one is concerned, we have an interesting situation. The main tableau started out with pLpp left. Since this is a formula beginning with L and is on the left, and since the accessibility relation is transitive, pLpp must be able to be written on the left of every tableau in the construction, including the one on the left just above:




But this is where we came in. It would seem that the verification of M13 cannot be accomplished, that a countermodel involving the indefinitely long recycling of the main tableau will result. But this infinite countermodel differs somewhat from that constructed earlier in this book for CLMpMLp. For the present countermodel to exist, there must be an infinite number of worlds accessible to the main world in which infinite number the conditions indicated in the above tableau prevail. But among these conditions is the requirement that LNLp be falsethat is, that Lp eventually hold. And this would appear to be at odds with another requirement dictated by the required recursion of the above conditions; that is, that p be false in an infinite number of worlds accessible to the main world. These requirements are not at odds, however, if there is indeed a world in which p becomes necessary, but between this world and the main world there are as many worlds (accessible to the main world and having access to the world in which Lp holds) as we wish. The world in which p becomes necessary then has no world which is its immediate predecessor, and so stands in a position of 'limit ordinality' to the main world. In effect, for M13 to be falsified in an S4.3 model structure, models must be there constructible which are 'dense' so far as the worlds making them up are concerned. If we look at our worlds as instants of time as Prior does, then, the `time sequence' which verifies S4.3 but not M13 will be a sequence having two instants between which there are an infinite number of instants. On the other hand, if we take M13 as an axiom in addition to S4.3, we obtain a system corresponding to a time sequence with discrete instants. This system will be called D (Sobocinski 1964 refers to it as S4.3.1). That S4.3 is the Diodorean system when time is considered to be dense and that D is the Diodorean system when the instants of time are thought of as being discrete (when a statement becomes false, for example, there is always a last instant at which it is true) was established algebraically by Bull 1965.
Now in S3° we have:
15.52  pLppLpLpLp 
which in S4° becomes
15.53  pLpppLpLp 
Given S1°, the above plus M14 give us
15.54  pLppCMLpLp 
By S1° and Lpp this last gives
15.55  pLppCMLpp 
which is M13; M14 then transforms to M13 in the field of S4. Whether or not S4 + M13 gives M14 is a problem that has stubbornly resisted solution; see, for example, Sobocinski 1964a. K. Fine has, however, provided an answer, and in the affirmative. The technique employed in this solution is somewhat different from those we have been using. We note first of all that the formula CpLpLpCMLpLp added to S4 gives M14, provided the rule RL of S4 can apply to it; the negation of this last formula is equivalent to
KMNpKMNpMKpMNpMLp;
the negation of M13, in turn, is equivalent to MKNpKNpMKpMNpMLp. We then show that a deduction corresponding to the Gentzen notation (given a certain a, to be specified)
15.55.1  MNp, MNpMKpMNp, MLp ® MKNpKNpMKpMNpMLp, MKNaKNaMKaMNaMLa 
holds in S4. By application of rules for N and PC procedures, this would mean that
15.55.2  MKNpMLp, MNp, MNpMKpMNp, MLp ® pLppCMLpLp 
holds in S4; this last deduction would permit the derivation of M14 (assuming RL to apply) from M13 and the substitution instance of M13 with p / a. We begin by showing that the deduction corresponding to
15.55.3  MNp, MNpMKpMNp, MLp ® MKNpKNpMKpMNpMLp 
holds in S4; note the formula in the antecedent of 15.55.3 not contained in that of 15.55.2; this will be eliminated in due time. We begin:
15.55.4  MKNpMLp  Hyp 
15.55.5  MNpMKpMNp  Hyp 
15.55.6  NpMNp  S1 
15.55.7  NpMKpMNp  15.55.5, 15.55.6, S1° 
15.55.8  MKNpKMLpNpMKpMNp  15.55.4, 15.55.5, S4° 
This last formula, of course, is strictly equivalent to the succedent of 15.55.3, which then represents a deduction of S4. We now note that the negation of formula MKNpMLp is strictly equivalent to NpNMLp; we shall now show that
15.55.9  NpNMLp, MNp, MNpMKpMNp, MLp ® KaKNaMKaMNaMLa 
represents an S4 deduction. The formula a is
15.55.10  NAKMNpMLpNp 
Let the formula b be strictly equivalent to the negation of a; what will then be shown is that given the formulas in the antecedent of 15.55.9 as hypotheses, we can derive
KNbKbMKNbMbMLNb,
which is equivalent to the succedent of 15.55.9:
15.55.11  MNp  Hyp, 
15.55.12  MLp  Hyp, 
15.55.13  KMNpMLp  15.55.11, 15.55.12, PC 
15.55.14  b (= AKMNpMLpNp)  15.55.14, PC 
15.55.15  CMLpMLKALpNMLpp  S2 
15.55.16  MLNb (= MLKALpNMLp)  15.55.15, 15.55.12, PC 
We now need only to derive bMKNbMKNbMb.
15.55.17  NpNMLp  Hyp, 
15.55.18  MNpMKpMNp  Hyp, 
15.55.19  NpMKNMLpKNpMNp  15.55.17, 15.55.18, S4 
15.55.20  MKNMLpKNpMNpMKNbMb  S4 
15.55.21  pMKNbMb  15/55.19, 15.55.20, S1° 
15.55.22  MNpMKNbMb  15.55.21, S4° 
But in S1, b implies MNp, and so bMKNbMb is derivable, along with b and MLNb. This makes KNbKbMKNbMbMLNb derivable, and so 15.55.9 holds. We think of ourselves as applying ®N to MKNpMLp in 15.55.3, and then mixing the resulting sequent with 15.55.9, with NpNMLp as the mix formula; the resulting sequent is easily transformed to 15.55.1. We then have it that S4 + M13 = S4 + M14, provided RL applies universally. This system may be called S4.1, following Sobocinski 1964a.
The Diodorean system  whether taken as S4.3 or D  is a system which finds its tense interpretation in a linear time sequence; that which is possible is precisely that which is now or will be at some time. If a statement happens never to become true, it is not, from the Diodorean point of view, in the realm of the possible. Systems like S4.2 and S4 may also be given a tenseoriented interpretation. The models for these systems are not connected as is that for S4.3, and so we may say that if the possible worlds for S4.2 and S4 models are interpreted as instants of time, then the time sequence interpretations for these systems involve 'branching time'; it is possible under these interpretations to have statements which are now possibly true but which are never realized. The difference between S4.2 and S4 is that as we shall recall S4.2 models have the special property of convergence. Thus the time sequence interpretation for S4.2 has the curious property of being branching but also converging. There are variations possible in the immediate future, but whatever path of intermediate possibilities we happen to actualize, the ultimate future is the same. The situation in S4 models permits branching but does not require convergence. Thus to say that a statement a will ultimately become necessary in an S4 model, we must assert LMLa  MLa in S4 models would assert merely that La is actualized along some branch; that branch, however, is one that might not be actualized in our future. In S4.2 models, however, all branches ultimately converge, and so if a becomes necessary along any branch, it becomes necessary along all  thus the typical S4.2 thesis MLpLMLp.
The addition of M13 or M14 to S4.3 gives us D, a system whose time sequence interpretation is such that every statement that is true, say, and becomes false has a last instant of being true, as opposed to the dense time of S4.3. Prior 1967 illustrates this by noting that the falsification of M13 requires the three statements NpMKpMNp (which is strictly equivalent to pLpp), MLp, and Np be true at once. Since Np is to be true, the truth of NpMKpMNp requires that p be true some time in the future and false at some time thereafter. Since NpMKpMNp begins with an L, it applies to all instants, including the instants in the future in which p is false; this means that we shall get an infinite recycling of the truth and falsity of p which  provided p must have a last instant of being false  is at odds with the requirement that p sometime must become necessary (MLp must hold). (It will be noted that this approach of Prior's is an 'ordinary language' version of the tableau construction above executed for this formula.) Since MLp in S4.2 as well as in S4.3 means that p must sometime become necessary, the above arguments will hold there as well as in S4.3, and so the addition of M13 or M14 to S4.2 will result in a system whose time sequence interpretation has 'discrete' instants (this system is called S4.2.1 in Sobocinski 1964a). The situation is a bit more complicated in the case of the addition of M13 or M14 to S4. First of all, S4 + M13 (called S4.1 in Sobocinski 1964a) and S4 + M14 (called S4.1.1) are likely distinct systems. And further, either M13 or M14 can be falsified in a branchingbutnotconverging model even with discrete instants. The infinitely alternating truth and falsity of p is compatible with MLp in a nonconverging system; we simply let p and Np alternate in truth up one branch and MLp be true along another. In order to get a time sequence analogue of D with S4 rather than S4.3 as base, then, we must add to S4 not M13 or M14, but
M15. pLppCLMLpp
It will be noted that although NpMKpMNp, MLp, and Np are compatible in a branchingbutnotconverging time sequence, the same trio with MLp replaced by LMLp is not compatible in such a model. Let us call S4 + M15 S4.1.4.
S4.4 and some associated systems
The systems we have so far discussed in this chapter (except for Parry's abortive S4.5) are all such that all their theses always take the value 1 in matrix t6 of Chapter 10; this is the matrix that is called 'Group II' in Lewis and Langford's SL  its basic use is to show that S4 is properly contained in S5; clearly, it accomplishes this for the various systems of this chapter. Another formula which always comes out with value 1 in this matrix is
M16. pCMLpLp
The relationship of this formula to MLpLp, the proper axiom of S5, is clear, as is the fact that it is a thesis of S5. That its addition to S4 does not yield S5 is established by the fact that, as we have noted, it always takes the value 1 in 'Group II'. Following Sobocinski 1964a, we call S4 + M16 S4.4.
Finite matrices such as Group II are often used in the literature to show that certain formulas are not in given systems. One might wonder if the discovery of such matrices is strictly a matter of hunches, ingenuity, and luck. It might be instructive to show how, for certain systems at least, such matrices may be developed as subcases of semantics such as we have been discussing in detail in this work. Our preliminary discussion of finite matrices (in Chapter 5) focused on truth value systems with 2^{n} values for some finite n. We noted that such values may be represented by the binary numbers from 0 to 2^{n1}, and that the PC operations within these systems operate as do the logical instructions of a digital computer, i.e. the value of the ith binary digit (bit) position of a truth function is determined by and only by the ith bit position of the arguments of that function. In the light of our semantics of possible worlds it may be seen that each bit position of the binary number representation of one of the values of such a system may be considered to be, in effect, a possible world (or, in the language of timesequences, an instant). For the purposes of evaluating under modal functions, then, we shall have to order the bits of a binary number in some way  in effect, this ordering will be the assignment of an accessibility relation. For example, suppose we order the bits from high order (leftmost) to low order. The relation of being 'of no higher order than' would be a natural interpretation of accessibility herein this case, a bit position would be thought of as 'having access to' itself and to all bits of lower order than itself. This relation is reflexive, transitive, and connected, and so is a version of the accessibility relation for MS4.3. Let us set down the eight bit arrangements of three bits each:
111  110  101  100  011  010  001  000 
We assume the bit positions in the above binary numbers to be related as indicated above, with higher order bit positions having access to themselves and to lower order ones. If p takes value 111, then, every world of the three represented has p 'true' in every world accessible to it, and so Lp will also be true in every world, and will take value 111. If p = 110, every world will have accessible to it a world in which p is false (the last one  the loworder bit position), and so Lp is false in each world, or overall, Lp = 000. If p = 101, the first and second worlds have accessible to them a world in which p is false (the second), and so Lp is false in them, but the only world accessible to the third world (itself) has p true, and so Lp will be true there, or overall, Lp = 001. Following this procedure (which is only a version of our tableau evaluation) in each case, we come up with the following list of values of Lp for the respective list of values of p above:
111  000  001  000  011  000  001  000 
Following common practice as we have done before, we assign the number 1 to the 'truest' of the eight value arrangements and 8 to the falsest (000) and the intermediate numbers to the intermediate arrangements. Doing so we come up with the following table for Lp and Mp (= NLNp).
p =  1*  2  3  4  5  6  7  8 
Lp =  1  8  7  8  5  8  7  8 
Mp=  1  2  1  4  1  2  1  8 
We then use this table for L and M in conjunction with the eightvalued tables for the PC connectives developed in Chapter 5. The reader may determine for himself that the matrix thus formed (call it t10) verifies all the theorems of the system D (indeed, this should be obvious from the relationship of this matrix to MS4.3). But take formula M16 and let p = 3 in the above matrix; 3CML3L3 = 3CM77 = 3C17 = 37 = L5 = 5. We see therefore that M16 cannot be proved in the Diodorean system D. Considering the status of D in S4.4, we note that if we do p / CLpq in M16 we get:
15.56  CLpqCMLpqLpq  
15.57  NpCLpq  S1 
15.58  NpCMLpqCLpq  15.56, 15.57, S1° 
15.59  MLqMLpq  S2° 
15.60  NpCMLqLpq  15.58, 15.59, S1° 
15.61  KMLqNpLpq  15.60, S1° 
15.62  LACMLqpLpq  15.61, S1° 
We call attention to 15.62 for future reference. Now do p / Lp in this last formula:
15.63  LACMLqLpLLpq  
15.64  LACMLqLpLpq  15.63, S4° 
15.65  CMLqLpLqp  S2° 
15.66  LALqpULpq  15.64, 15.65, SSS 
Note that 15.66 is derived from 15.62 and S4°; 15.62 in turn comes from M16 + S4; we see then that S4.4 contains S4 + 15.62 which in turn contains S4.3 and so S4.2.
In S1, now, we have as a substitution instance of Lpp
15.67  MLppCMLpp  
15.68  LMLppLp  M16, S2° 
15.69  MLppLp  15.68,S4.2 
Noting that the initial MLp in 15.67 is in a Cpos
15.70  pLppCMLpp 
The last is, of course, M13; S4.4, then, contains D. Let us now note the formula
M17. ALpqCMLqp
This formula is deductively equivalent in the field of S4 to 15.62, and so is provable in S4.4; also, then, S4 + M17 contains S4.3; we call S4 + M17 S4.3.2 (Zeman 1968a). Let us now evaluate M17 in matrix t10 above; try it with p = 5 and q = 3: AL53CML35 = A53CM75 = AL3C15 = A75 = 5. M17 fails in this matrix and so is not contained in D nor in S4.3; we shall later show that its containment in S4.4 is proper and that it is independent of D. We now look back to the S4.3.2 theorem 15.65, which clearly can result by Sl° operations from 15.67 and so is in S4.3.2; do p / CpLp, q / Lp in 15.62:
15.71  NCpLpCMLppLpLp 
Let us now assume formula M13 or M14; since we are already assuming S4.3.2, we have S4.2 and so with either M13 or M14, M14 is provable; with 15.71 and Sl° this gives us
15.72  NCpLpCMLpCMLpLp 
In S1° this transforms to
15.73  NLpCpCMLpLp 
(Note that NCpLp is strictly equivalent to KNLpp.) Provable in S1° is
15.74  LpCpCMLpLp 
Since CpqCNpqLq holds even in S1°, we may move from 15.73 and 15.74 to
15.75  pCMLpLp 
which is, of course, the proper axiom for S4.4. S4.3.2 + M13 (or M14) then is precisely S4.4.
We shall now establish a sequentlogic LS4.4 for the system S4.4. This sequentlogic will be somewhat different from the ones we have already discussed in that it will make use of a new symbol  a special kind of arrow, . This symbol will be used to form sequents from sequences just as is the standard arrow ®. Sequents employing this arrow may appear in proofs, but we shall think of them as being 'second class citizens' so far as theoremhood is concerned; if a sequent G Q occurs in an LS4.4 proof, we may refer to it as a 'subtheorem'. LS4.4 will use the axiom schema for the standard arrow as well as the rules of LS4, including, of course, those of LPC, for that arrow. It will also have an axiom schema a a for the special arrow and a set of rules for sequents employing this arrow. This set of rules will be formed simply by taking the full set of LS5 rules (see Chapter 13) and replacing ® wherever it occurs in these rules by . We shall also have a special rule which will enable us to convert subtheorems into theorems. This may be done when we have a sequent involving which has each of its formulas beginning with L. The rule then is
LG LQ 


CONV 
Q, LG LQ 
We shall give an example of a proof in LS4.4:






We have thus shown that there is a sequent theorem in LS4.4 analogous to formula M16. Since LS4.4 contains all LS4's rules for the ordinary arrow ®, LS4.4 will have as theses analogues of all of the theses of S4.4, and so
*15.9  If a is a theorem of S4.4, ® a is provable in LS4.4. 
We now wish to prove the converse of *15.9. To do so, we shall have to establish in S4.4 a means of interpreting the new arrow . If i(G ® Q) is the interpretation in S4.4 of G ® Q, then we shall let i(G Q), the interpretation of G Q, be the formula MLi(G ® Q). We shall wish to show that the interpretations of all theorems and subtheorems of LS4.4 are theorems of S4.4. To do this we first show that
*15.10  If a is a theorem of S5 then MLa is a theorem of S4. 
First of all, we note that if a is a thesis of S4, then MLa and LMLa are also S4 theses, by CpMp and RL. In S1 we have
15.76  LCLMLpMLp 
By LpMqLMCpq, which holds in S2°, and 15.76 we get
15.77  LMCMLpLp 
And by CMpLqMpLq (which holds in S4) and SSS, 15.77 yields
15.78  LMLCMLpLp 
We shall then have both LMLMLpLp and MLMLpLp holding in S4. In S1° we have
15.79  LCpqCLpLq  
15.80  MLCpqMCLpLq  15.79, S2° 
16.81  MLCpqCLpMLq  15.80, S4° 
15.82  LMLCpqLpMLq  15.81, S2° 
15.83  LMLCpqMLpMLq  15.82, S4° 
15.84  LMLCpqCLMLpLMLq  15.83, Sl° 
This last formula is a principle of distribution of LML over C, which then holds in S4. But then if LMLCab and LMLa are S4 theses, so too will be LMLb. And further, if b results from a by substitution, then LMLb so results from LMLa. Since LMLa holds in S4 whenever a is an S4 thesis or  by 15.78  is MLpLp, this will mean that LMLa will be an S4 thesis whenever a is an S5 thesis, and *15.10 holds. If we were to replace ® by in every subtheorem of LS4.4, the result would be the set of theorems of LS5; since the interpretation of each theorem of LS5 is a thesis of S5, we may move by *15.10 to
*15.11  If G Q is a subtheorem of LS4.4, the interpretation of G ® Q is a thesis of S4, and so also of S4.4. 
It is possible to generate theorems in LS4.4, of course, without at all using the rules for . In this case, the rules employed are those of LS4, and since each theorem of LS4 has its interpretation as a thesis of S4, theorems of LS4.4 generated without use of the rules for will have their interpretations as theses of S4.4. Let us now consider the case in which generation of a theorem of LS4.4 does involve the use of the rules for . There will be locations in the proof involved at which subtheorems LG LQ will be converted to theorems by the rule CONV. The interpretation of such a subformula will be equivalent to the S4.4 formula
15.85  MLCLgALq_{1} . . . Lq_{n} 
where g is the conjunction of the formulas of G and the q_{i} are the formulas in Q. In the special case in which n = 0, the interpretation of the sequent in question is equivalent to
15.86  MLNLg 
the interpretation of the conclusion of CONV in this case then is equivalent to
15.87  NLg 
That 15.87 follows from 15.86 holds by CLpLMLp, which holds in S3. Assuming in the more general case that 15.85 holds in S4.4, we first distribute the initial ML (which distributes in S4.2, and so in S4.4, as we have seen LML to do in S4)
15.88  CMLLgMLALq_{1} . . . Lq_{n} 
By CLpMLLp, which holds in S4, and CMLpMp which holds in S1, we transform this last formula to
15.89  CLgMALq_{1} . . . Lq_{n} 
and thence by CMApqAMpMq to
15.90  CLgAMLq_{1} . . . MLq_{n} 
We now note that by the axiom pCMLpLp of S4.4 we shall have holding for each i from 1 to n the formula
15.91  CMLq_{i}Cq_{i}Lq_{i} 
The MLq_{i} in 15.90 are in Cpos in that formula, and so by 15.91 and SSI may be replaced by Cq_{i}Lq_{i} in each case to get
15.92  CLgACq_{1}Lq_{1} . . . Cq_{n}Lq_{n} 
By PC, principally by the thesis CACpqrCpAqr, the above transforms to
15.93  CKLgKq_{1} . . . q_{n}ALq_{1} . . . Lq_{n} 
Distributing the initial L among the conjuncts of g in the above by CKLpLqLKpq transforms 15.93 into the interpretation of Q, LG ® LQ, the conclusion of CONV when the premiss is LG LQ. We thus have an analogue of CONV in S4.4 (details of the above proof are slightly simpler if n = 1; these are left to the reader). Since the rules which can be applied in a proof string after CONV are all LS4 rules, we may now assert that if a sequent is a theorem of LS4.4, then its interpretation is a thesis of S4.4. By the above and *15.9, then, we have
*15.12  a is a thesis of S4.4 iff ® a is a theorem of LS4.4. 
In the sequentlogic for S4.4 we have two different kinds of arrow and so two different kinds of sequent. Corresponding to these two kinds of sequent will be two kinds of world in the 'possible worlds' model structure we shall propose for S4.4. We shall discuss a model structure MS4.4 in which the accessibility relation will differ depending upon the world for which it holds. The 'real' world, that corresponding to the main tableau, will be accessible only to itself and will have access to all worlds. Each world other than the main world will be denied access to the main world, but will have access to all other worlds (including itself, of course). The worlds other than the main world then will constitute a 'substructure' in which the accessibility relation is transitive, reflexive, and symmetrical as it is for MS5. The difference from MS5 comes in the main tableau's having all other tableaux auxiliary to it, but this relation not being symmetrical. As one might expect, this will mean that the rules for L in the tableaux of MS4.4 will differ between main and auxiliary tableaux. For Ll, the differences are straightforward; we state two rules:
Ll(4.4m):  If La occurs left in a main MS4.4 tableau, write La and a left in all tableaux of that alternative set (except where they already occur). 
Ll(4.4a):  If La occurs left in an auxiliary MS4.4 tableau, write La and a left in all auxiliary tableaux of that alternative set (except where they already occur). 
The situation for Lr is a bit more complex; we shall first state the version of Lr for the auxiliary tableaux:
Lr(4.4a):  If La occurs left in an auxiliary tableau in MS4.4, begin a new auxiliary tableau with a on its right. 
This corresponds to the Lr rule for MS5. Suppose now that we have formulas La_{1}, . . ., La_{n}, n ³ 1, on the right in a main tableau. In order to construct the countermodel we are working on we must have these n formulas false in the world corresponding to that main tableau. For each i from 1 to n, then, one of two situations must obtain: either a_{i} is false in the world corresponding to the main tableau, or it is false in one of the other worlds to which that world has access. In the former case, it is possible that a_{i}, may be true in all the worlds other than the main one, in which case La_{i} would also hold in all those worlds (and MLa_{i} would hold in the main one  without La_{i} holding there, thus falsifying CMLpLp). But if the latter case obtains, that is, if a_{i} is false in any of the auxiliary worlds, by the accessibility relation obtaining between these worlds, La_{i} fails in all of them. If a_{i} is assumed to be true in the main world while La_{i} is false there, then a_{i} must fail in one of the auxiliary worlds; from the above, then, if La_{i} must fail in the main world while a_{i} holds there, then La_{i} must fail in all the worlds of that set. We shall make use of the above by specifying that for each La_{i} occurring on the right of a main tableau the tableau will be split:
La_{i}  


a_{i} is to occur right in one of the tableaux resulting from the split and left in the other; the justification for this may be taken as the law of excluded middle: any formula is either true or false in this world. The tableau with a_{i} right is a new main tableau; note that if a countermodel can be constructed on the basis of ai right, we have shown that La_{i} can indeed be written right in that tableau. On the other hand, the alternative tableau with a_{i} left does not give us a sufficient basis for asserting the falsification of La_{i}, even if a_{i} can consistently be placed left there. Here we must go to auxiliary tableaux for that justification; as we have noted, for the situation required in the main tableau to obtain, La_{i} must fail in all other worlds of that set; for this reason we shall begin a new tableau auxiliary to the main tableau and beginning with La_{i} on its right. Let us now state the rule for n in general; this rule will be stated in a number of clauses:
Lr(4.4m): 

This rule then identifies three separate instances of L on the right. In the first, no auxiliary tableau action need be taken for the L in question, since the formula  if falsifiable under this assumption  is falsified in the main tableau. Under assumption (2) above, each of the a_{i} involved must be false in a world corresponding to an auxiliary tableau, and so all m La_{i};, must be false in all such worlds. In the third instance we use excluded middle as noted to test what happens under the assumption that each of the a_{i} is true or is false in the main world. Note that in each of the n tableaux which under (3) take an a_{i} on the right there will remain n  1 formulas beginning with L to which (3) still applies; this will result in a split into n tableaux, one of which has the n  1 formulas (each stripped of its initial L) all left and each of the others with a different one of these n  1 formulas on its right. The procedure given in (3) is then applied recursively until all possible combinations of the a_{i} left and right are represented in alternative tableaux; clauses (1) and (2) then are used as required. The above rule should be applied only after all LPC steps in the main have been used. Let us try out a formula  M16  in this model structure; we place it right in a main tableau; it begins with L, so by clause (3) of Lr(4.4m) we move to
pCMLpLp  
CpCMLpLp 

CpCMLpLp 
Consider first the tableau taking CpCMLpLp on its left. The instructions here are to create an auxiliary tableau taking pCMLpLp on its right (clause (2)). For that tableau the rules then become different, being essentially those of MS5; since an MS5 tableau construction begun for this formula will close, so too will this one, and so will the alternative set in question. We look now at the other alternative main, that with CpCMLpLp on its right. Clause (1) tells us that so far as the original L is concerned, we are finished  but now we have some MPC operations to perform; involved are two Cr and one Nl arising from PC connectives in the CpCMLpLp on the right. When we have performed these operations that tableau will be
pCMLpLp  
CpCMLpLp  
p  CMLpLp  
MLp  Lp  
LNLp 
Lp occurs right, but p also occurs left, and so we shall be able to apply clause (2) for Lp; LNLp, however, occurs right with NLp neither left nor right. We then apply clause (3) (here we show in the tableau only the formulas relevant for the applications of Lr here discussed):
p  Lp  
LNLp  


Lp 

We have performed the Nr in the left of these tableauxnote that that tableau closes. We now note that in the other tableau we have both p and NLp left, and so clause (2) of Lr(4.4m) is performed, resulting in an auxiliary tableau with Lp and LNLp right. Since this tableau will behave like an MS5 tableau, it will close and so the whole construction closes; pCMLpLp then is valid in MS4.4. The reader may easily establish for himself that the axioms of S4 are valid in this system and that the rules of that system preserve validity. We then have:
*15.13  If a formula is a theorem of S4.4, it is valid in MS4.4. 
Let us contrast the validity of M16 with the situation for, say, CMLpLp:
CMLpLp  
MLp  Lp  
LNLp 
This tableau must by clause (3) be split into three tableaux:
CMLpLp  
MLp  Lp  
LNLp  
p 
p 
NLp  
NLp  Lp 
The leftmost of these falls under clause (2) and generates an auxiliary tableau beginning with Lp and LNLp right; behaving like an MS5 tableau, this closes. The rightmost of these takes NLp right and so Lp left, and so closes. The middle one comes under clause (3) so far as LNLp is concerned (with p right, it falls under (1) for its Lp right), and so splits (we show just the Lp, LNLp, and p right in that tableau initially)
Lp  
LNLp  
p  
NLp 
NLp 


The right tableau of this split ends up with Lp left again, and so closes. The other one, however, must generate an auxiliary tableau which by clause (2) of Lr(4.4m) has just LNLp on its right. Since LNLp is not a valid formula in MS5, this auxiliary tableau will not close, and we have a countermodel to CMLpLp (analysis of the countermodel will reveal that it is the one in which p is false in the 'real' world and true in all others).
We now wish to show that all « valid in MS4.4 will have ® a provable in LS4.4. Suppose that a given formula is valid, and that in the construction which shows it to be so there were no uses of Lr. The construction is then a recipe for a proof of that formula in MPC + Ll, and the formula is then provable in LS4.4. Next, suppose that in such a construction Lr was used ('use' of (1) only does not count). There are then alternative sets in that construction in which clause (2) of Lr(4.4m) was applied. Consider one such. The auxiliary tableaux of this set will have one tableau which was generated directly by the main tableau; it begins with on its right the formulas LQ placed there by the application of clause (2). It will also have on its left the formulas LG which are all the formulas beginning with L on the left of the main tableau. This auxiliary tableau closes, essentially, under the L rules of MS5, which means that the sequent LG ® LQ is a theorem of MS5 and so LG LQ is a subtheorem of LS4.4. By the rule CONV of LS4.4, this last subtheorem is converted to the theorem Q, LG ® LQ. But this sequent corresponds to the 'final state' of the main tableau, before clause (2) of Lr(4.4m) was applied. The rule CONV corresponds to the application of clause (2) in the tableau construction. Preceding that application we shall ordinarily have had an application of clause (3), which involves a splitting of the tableau into a tableau with formulas a_{l}, . . ., a_{n}. left and n tableaux, each with one of the a_{i} right. Each of these tableaux closes, since the assumption is that we have a closing construction. The tableau splitting under clause (3) is quite clearly a 'cutlike' operation; the use of clause (3) in MS4.4, then, will signal the use of the rule cut in LS4.4. Where clause (3) split the original tableau into n + 1 tableaux, there will be n applications of cut, with the ith of these applications having a as its cut formula. There are n + 1 proof strings to be combined here; the final sequent of one of these has all the formulas a_{l}, . . ., a_{n} in its antecedent; each of the n others has a different one of the ai in its succedent. The one of these sequents with ai in its succedent is used as the left premiss of the ith cut application; the sequent with the n formulas in its antecedent is used as the right premiss of the first cut application, and the conclusion of the (i  1)th cut application is used as the premiss (right) of the ith cut application. The elimination of the n formulas by these n applications of cut is the inverse of the insertion of these formulas by clause (3) of Lr(4.4m). An example of such cut application is seen in the LS4.4 proof of pCMLpLp earlier executed; note that this cut application follows the use of the rule CONV. Once we have entered the main tableau, so to speak, the remaining steps up to the initial state of the tableau are a recipe for a proof in LS4  actually, in LPC + L®. The closing MS4.4 construction then provides us with a recipe for an LS4.4 proof for the formula for which the construction began, and so by the above, *15.13 and *15.12 we have:
*15.14  A formula a is valid in MS4.4 iff ® a is a theorem of LS4.4, and so also iff a is a theorem of S4.4. 
us now suppose that we have a formula which we wish to check for validity in MS4.4; each alternative set in the resulting construction will either involve an application of clause (2) of Lr(4.4m) or not. If not, then the set closes on the basis of the MPC + Ll rules, and so is decidable. If it does have an application of clause (2), then its closing or not depends on the closing or not closing of the auxiliary tableau generated directly from the main by clause (2). This auxiliary tableau will close iff the tableau beginning with the same formulas (including on its left any formulas on the left of the main beginning with L) closes in MS5; but this is decidable. Thus:
*15.15  MS4.4 provides a decision procedure for S4.4. 
The models for some of the other systems we have studied in this chapter have been interpreted as time sequences; it is interesting to do this for S4.4 as well. In MS4.4 the main world differs in kind from the other worlds (because of the difference in accessibility relation); in a time sequence interpretation the main world would be the first instant of the time sequence, which would then, of course, have all the other instants of the sequence in its future. But given the peculiarities of the accessibility in MS4.4, each of the instants other than the first would have all the other instants other than the first in its 'future'; the notions of past, present, and future then become intermingled as they do in S5 models interpreted as time sequences. We note that in S4.4 models considered as time sequences, any statement that is possibly necessary will become simply necessary in the instant immediately following the first. In time sequence language, this means that all that is ever to become 'eternally' true becomes eternally true in the very instant following the present one. This makes S4.4 a sort of logic of the end of the world; the first instant in the model is the instant in which the angel blows his golden horn (or however the world ends)  after this instant we are in eternity. This interpretation for S4.4 is first developed (using different methods) in Zeman 1971, where it is called the 'end of the world matrix'.
We now direct attention back to the system S43.2, which is S4 + M17 (ALpqCMLqp). We recall that that system plus M13 or M14 gives S4.4; since M13 and M14 have the effect of changing S4.3 and S4.2 into logics with discrete instant time interpretations, we might wonder if the same might be true with S4.3.2  does S4.4 stand to S4.3.2 as D does to S4.3? The answer is that it does. The time sequence interpretation for S4.3.2 is like that for S4.4 in making a distinction between instants in 'time' (like the first instant in an S4.4 model) and in 'eternity'. The instants in 'eternity' in such an S4.3.2 model are just like those in an S4.4 model, all having access to one another and to none of the instants in 'time'. There are, however, not one, but an infinity of instants in time, each having access to all instants in time and to all instants in eternity as well. It is clear that in such an interpretation pCMLpLp would fail; MLp may be true by virtue of p's being true in all instants of eternity; p at the same time may be true in any one of the instants of 'time' without being true in all of them; in this case both p and MLp are true without Lp being true, and S4.4 fails. Let us examine ALpqCMLqp in this interpretation, though. This formula is deductively equivalent to CMLqCNpLpq in the field of S4. This last formula is falsified iff MLq, Np, and MKLpNq (the negation of Lpq) are true simultaneously. We examine these requirements:
MLq  means that q must be true in at least all the instants of 'eternity'. 
Np  means that p must be false at some instant. But since MKLpNq must also hold, p cannot be false in eternity, else Lp can never hold (since all instants of eternity have access to each other); p then must be false in an instant of time, and so Lp must fail in all instants of time (which have access to each other). 
MKLpNq  means that at some time p must be necessary at some instant at which q is false. But by the above, p becomes necessary precisely at the point at which q  by MLq  must be necessary. Falsification of M17 is then impossible here, and the suggested model verifies M17. 
Proof that this model structure is characteristic for S4.3.2 is due to K. Fine; the methods employed differ somewhat from those we have generally been employing and will not be detailed here.
We shall suggest a finite version of this model structure. This matrix will have three instants; we shall think of one of these as being in 'eternity'the last one. The first two are in time, and have access to each other and to the last, which has access only to itself. Using our binary representation as before, we see that if p = 111, Lp = 111; if p = 110, Lp (with p false in the last instant) = 000; if p = 101, Lp = 001. In general, if p is true in the last instant, the one instant in eternity in this model, Lp is also true there; if p is false there, Lp is false at all instants, and Lp is true in either of the first two instants iff p is true at all three. The binary table for Lp for all eight values, then, is
111  000  001  000  001  000  001  000 
The resulting table in decimal notation for Lp and Mp is
p =  1*  2  3  4  5  6  7  8 
Lp =  1  8  7  8  7  8  7  8 
Mp=  1  2  1  4  1  2  1  8 
Call this t11. The reader may satisfy himself that this table verifies S4 and M17. So far as M16 is concerned, at p = 5, 5CML5L5 = 5C17 = 57 = L3 = 7; the reader may verify for himself that M13 fails at the same value for p. The result of the above, of course, is that S4.3.2 is properly contained in S4.4.
Our model for S4.4 shows that that system is 'almost S5'. It is appropriate to ask, as did Sobocinski 1964a, whether or not there are any systems between S4.4 and S5 but equivalent to neither. Actually, this question has been answered in the affirmative (Schumm 1969) but there are aspects to it that we shall examine here. Suppose we have a formula a which is
1.  A theorem of S5; 
2.  Not a theorem of S4.4; 
3.  Has only one distinct variable. 
We wish to show that the addition of a to S4.4 always yields S5. A variable, say p, may be true in all S4.4 worlds, false in all, or true in some and false in others; each distribution of assignments of 1 and 0 to p in the various worlds may be called an assignment to p in MS4.4. We wish to turn our attention to the set of all possible MS4.4 assignments with the exception of two. The two assignments we wish to exclude are first, the one in which p is true in the one instant of time and false in all those of eternity (we use the time sequence terminology) and secondly, the assignment in which p is false in the one instant in time but true in all those of eternity. Consider now a formula whose only variable is p, and let that variable take values only from the set of assignments specified above, that is, values excluding the two explicitly mentioned assignments. Let a be the set of instants (worlds) in which, for a given assignment, p takes the value true, and b be the set for that given assignment in which p is false. Then we wish to show that so long as the assignment to p is not one of those explicitly excluded above, the formula whose only variable is p will be either
(1)  true in every instant of a and false in every one of b, or 
(2)  false in every instant of a and true in every one of b, or 
(3)  true in every instant, or 
(4)  false in every instant. 
If the formula in question has no connectives, then it is p and the above holds. Suppose that when such a formula has k or fewer connectives, one of (1) through (4) above holds of it. Consider such a formula with k + 1 connectives. Let us assume a KNLprimitive basis. The formula in question is then of form Kbg or Nb or Lb. By the induction hypothesis one of (1) to (4) above is true of b and g. For the case in which the formula is Kbg, if the same of (1) to (4) is true of both conjuncts, then it is also true of the conjunction; if (4) is true of either conjunct, then it is also true of the whole conjunction; if (3) is true of either conjunct, then the one of (1) to (4) true of the other conjunct is true of the conjunction; and finally, if (1) is true of one conjunct and (2) of the other, then (4) is true of the whole. In any case the conjunction comes out with one of (1) to (4) true of it. For the case in which the formula is Nb, if (1) or (2) is true of the negated formula, then (2) or (1) respectively is true of the negation, and if (3) or (4) is true of the negated formula, (4) or (3) respectively is true of the negation, which then also has one of (1) to (4) true of it. For the case in which the formula is Lb, b is forbidden by the restrictions on the assignments to p and (1) to (4) from being false in time and true in all of eternity, else p would have to be one of the two excluded values; since false in time and true in all eternity is the only assignment to b that can give Lb a composite value of true in all worlds or false in all worlds, Lb will have one of (3) or (4) true of it. Thus if a formula with only one variable is to be false in time and true in all eternity, its variable must have assigned to it either the value false in time and true in all eternity or the value true in time and false in all eternity.
We now return to our formula a which is a theorem of S5 but not of S4.4 and which has only one variable. Being excluded from theoremhood in S4.4 it must fail to hold in MS4.4 for some assignment to its variable. Being a theorem of S5, it holds in MS5. This means that it must be true always in every world of MS4.4 except, at certain points, for the main world (since the worlds other than the main or real one in MS4.4 constitute an MS5 model). Its failure in MS4.4, then, must come from its being, for some assignment to its variable, false at the instant in time (the main world) and true at all other instants (worlds). But then, by our work above, the assignment to its variable can only be either true in time and false in all eternity or false in time and true in all eternity when a fails to hold. Examine now the formulas MLpLp and MpLMp, either of which when added to S4.4 gives S5. It will be noted that the second of these fails in MS4.4 only when p is true in the instant of time and false in all eternity, and the second fails only when p is false in time and true in all of eternity. Since a can also fail only for one or the other of these assignments, it is clear that one of
15.94  CaMLpLp 
or
15.95  CaMpLMp 
will be valid in MS4.4, and so provable in S4.4. If a is then added to S4.4, MLpLp or MpLMp may be detached, giving S5. We summarize
*15.16  MS4.4 provides a decision procedure for S4.4. 
This gives a negative answer to Sobocinski's question regarding systems between S4.4 and S5 so far as new axioms containing only one variable are concerned. But in general, are there formulas which are theses of S5 and not of S4.4 but whose addition to S4.4 does not extend that system to S5? As noted, that version of the question was answered affirmatively by Schumm 1969. He proposed a system which may be formulated by adding
M18. ACMLppCLMqMLq
to S4.4; he called the system S4.7, but for reasons soon to be made clear, S4.9 is a more appropriate name, and shall be taken as standard for this system. Sobocinski 1970a gets this system by adding
M19. AMLpLpMLMqCpLq
to S4. By MLqMLMq (in S1) and SSS this becomes
15.96  AMLpLpMLqCqLq 
By S1° and with q / p this gives
15.97  AMLpCpLpMLpCpLp 
which gives M16 and so S4.4 by PC methods. On the other hand, we could use M19 and SSS to distribute L as follows
15.98  AMLpLpLMLMqqLq 
and then M as follows
15.99  AMLpLpLMLMqCMqMLq 
Since both LMqLMLMq and LMqMq hold in S4. we go by SSS to
15.100  AMLpLpLMqCLMqMLq 
from which we easily get M18.
It is clear that S4.9 contains S4.4; that it does so properly is seen by the fact that M18 is easily falsifiable in MS4.4; using the time sequence terminology, we simply let p be true at every instant in eternity but not that in time, falsifying CMLpp, and let q be true in some but not all instants of eternity, making LMq true and MLq false, and so falsifying CMLqLMq at the same time as CMLpp.
Another formula which is a thesis of S5 but not of S4.4 is
M20. LMpCLMqCMKpqLMKpq
Let the conjunction Kpq hold at time but nowhere in eternity in MS4.4, and let p and q hold at (distinct) instants of eternity. LMp, LMq, and MKpq (because of Kpq) then hold, with LMKpq failing, and we have a countermodel to M20. We might call S4.4 + M20 S4.6 (see Zeman 1971). Another formulation of S4.6 is S4 plus
M21. CpLMpCCqLMqCMKpqLMKpq
We shall show later on that M19, 20, and 21 are in S4.9.
K. Fine has shown that M18 is in S4.6; the method is similar to that used in showing S4 + M13 = S4 + M14. We note that the negation of M18 is equivalent to the conjunction of the formulas MLp, Np, LMq, and LMNq: strip M20 of its initial L; the resulting formula is CLMpCLMqCMKpqLMKpq, the negation of which is equivalent to the conjunction of the formulas LMp, LMq, MKpq, and MLNKpq. We should then wish to show that a substitution instance of the conjunction of these last four formulas follows from the conjunction of the first four: let a = ANpq and b = ANpNq; we show that the deduction
MLp, Np, LMq, LMNq KLMaKLMbKMKabMLNKab
holds. This, of course, is the same as saying that M18 follows from M20.
15.100.1  LMq  Hyp. 
15.100.2  LMANpq (= LMa)  15.100.1, S2° 
15.100.3  LMNq  Hyp. 
15.100.4  LMANpNq (= LMb)  15.100.2, S2° 
15.100.5  Np  Hyp. 
15.100.6  CNpKANpqANpNq (= CNpKab)  PC 
15.100.7  MKab  15.100.6, 15.100.5, S1 
15.100.8  CpNKANpqANpNq (= CpNKab)  PC 
15.100.9  CMLpMLNKab  15.100.8, S2° 
15.100.10  MLp  Hyp. 
15.100.11  MLNKab  15.100.9, 15.100.10, PC 
So the four conjuncts of the substitution instance of the negation of M20 are provable, and M18 may be derived from S4.6; since we shall show that S4.6 is in S4.9, we shall have S4.6 = S4.9.
We note at this point that formula M20 will be verified both by matrix t10 and t11, which were presented respectively in our discussions of D and S4.3.2. Since these matrices verify those systems respectively but not S4.4, we see that S4.3.2 or D plus M20 is properly contained in S4.6. Call D + M20 S4.3.3 and S4.3.2 + M20 S4.3.4.
Sobocinski's family K of 'nonLewis modal' systems
We shall briefly leave our study of systems strictly in the Lewis modal family to examine a family of systems which are closely related to the Lewis modal systems but which contain as theses some formulas which belong to none of the systems we have so far discussed. Note the formula
M22. LMpMLp
This is the converse of M12, the proper axiom of S4.2. It is provable in none of the systems already discussed, for then it would be provable in S5; by the reduction theses of S5, M22 would make MpLp provable, which would totally collapse the modal structure of S5 by making a, La, and Ma equivalent, for every formula a. But if we test M22 in matrix t6  Group II  we find that it is valid in that matrix. S4.4  and indeed, S4.6 and S4.9  are all verified by this matrix (which falsifies CMLpLp); the addition of M22 to any system contained in S4.9, then, will fail to give us S5, and will fail to make pMLp provable. Another formula with similar effects is
M23. KLMpLMqLMKpq
Note that in S2° we have
15.101  MpMCqKpq  
15.102  MpCLqMKpq  15.101, S2° 
15.103  LMpLqMKpq  15.102, S2 
15.104  MpMLqMKpq  15.103, S4° 
We now assume M22, LMpMLp (with p / q) and SSS:
15.105  LMpLMqMKpq  
15.106  LMpCLMqLMKpq  15.105, S4° 
This last transforms in S1° to M23; M22 + S4, then, yields M23.
Assume now S4 + M23. In S2, M23 transforms to
15.107  LMpMCMqLMKpq 
In S1° this gives
15.108  LMpMALNqLMKpq  
15.109  LMpMALpLNLCpp  15.108, q / Np, S1° 
In S4, LNLCppr is a thesis (LNLCpp is impossible); with SSS and r / Lp, 15.109 then gives
15.110  LMpMALpLp 
which in S1° gives M22; S4 + M22, then, = S4 + M23. McKinsey 1945 refers to this system as S4.1; because of its nonLewis modal nature, however, it seems more appropriate to follow Sobocinski 1964b in calling it system K1.
We can form other systems related to K1 by adding M22 or M23 to other of the systems we have been studying. For example, S4.2 + M22 = K2, S4.3 + M22 = K3, D + M22 = K3.1, S4.3.2 + M22 = K3.2, S4.4 + M22 = K4. We note that the finite matrices we used to show that the containment relations of S4, S4.2, S4.3, D, S4.3.2, and S4.4 are proper will also show that the containment relations between the respective K systems are proper; that is, each of these matrices verifies M22 and M23 as well. Prior 1964 notes the reason for this. Each of these matrices provides a model that has an 'end point'. In a three 'instant' matrix in which the third instant has access to no instant but itself, that instant is an end point (indeed, this holds for any instant that has access to no world other than itself. Suppose we have a finite model in which every branch ends with such an end point. If LMp is to hold in such a model, the truth of p must be accessible to us no matter where we are in the model, including at those end points. Thus if LMp holds, p must hold at each end point. But these end points then mark places where p becomes true and never again becomes false. It will then turn out that there are in the future of the worlds of this model points at which p is necessary  MLp holds. If a model contains no end point, however, LMp can be true simply by alternating p and Np in successive worlds forever; in this case MLp would not hold. The systems containing M22 and M23, then, are systems in which the models possess end points.
We shall be especially interested in system K4 (= S4.4 + M22). What we shall show is that this system has as a characteristic matrix our t6  the Group II of SL. We shall do this by adapting the model structure MS4.4 so that it duplicates the behaviour of Group II. Group II is a fourvalued matrix; this means that when considered from the point of view of possible worlds, each of its models will have two possible worlds, and each of the corresponding tableau constructions will have at most two tableaux in each alternative set. The world other than the main world in such a model is an end point. We note that if La is to be false in such a world, then a must be false there as well, since an end point has access only to itself. We adapt MS4.4 into a model structure MK4, then, by changing the rule Lr(4.4a) so that when La appears right in an auxiliary tableau, we write a right in that tableau rather than creating a new tableau for it. We formally state
Lr(K4a):  If La appears right in an MK4 auxiliary tableau, write a right in that tableau. 
The rule of Lr in the main tableau shall be MS4.4's Lr(4.4m) with its three clauses. We may interpret MK4 in our binary notation; with the highorder bit representing the main world and the loworder bit the other, we shall have for p = 11 Lp = 11 as well; for p = 10, Lp = 00 (both worlds have a world  the last  accessible to them in which p is false); for p = 01, Lp = 01 as well; for p = 00, Lp = 00. Translating into decimal notation, this gives us:
p =  1  2  3  4 
Lp =  1  4  3  4 
Mp =  1  2  1  4 
This is the table for Group II; indeed, it should be clear that
*15.17  A formula is valid in Group II (matrix t6) iff the construction begun for it in MK4 closes. 
We then also have, by M22's validity in Group II:
*15.18  All theses of K4 are valid in MK4. 
We shall draw the connection between K4 and its semantics as we have done with other systems by using a Gentzen style system as an intermediate. This system will be called LK4, and it will differ from LS4.4 only in its rule L. The revised form of this rule for LK4 will be

L 
This rule corresponds to the revised Lr(K4a) for MK4. A closing MK4 construction will be used as a recipe to write a proof in LK4. All operations in an auxiliary tableau correspond to the rules for LK4 involving ; Lr(K4a) does for the right side of an auxiliary tableau precisely what Ll does for the left; L and L are clearly parallel for the system LK4. Other than for L, the rules of LK4 are the same as for LS4.4. Since LK4's L corresponds to MK4's Lr(K4a) in the same way that the L in the succedent rules of the other systems we have studied correspond to their respective Lr rules, we shall be able to use a closing MK4 construction beginning with « on its right to put together a proof in LK4 for ® a, and it will be the case that:
*15.19  If a is valid in MK4 (equivalently: always takes 1 in Group II) then ® a is a theorem of LK4. 
We must now show that the theorems of LK4 have correlate theorems in K4. The interpretations of LK4 sequents in K4 will be the same as those of LS4.4 sequents in S4.4. The only rule of LK4 which differs from its counterpart in LS4.4 is L; we must then show that this rule has an analogue in K4. This will be the case provided we can move from a theorem i(G Q, a) toi(G Q, La) as a theorem in K4. The first of these formulas, the interpretation of the premiss of this L, is
15.111  MLCgAqa 
where g is the conjunction of the formulas of G or constant true and the formula q the disjunction of the formulas of Q or constant false. For our purposes we may express this interpretation as follows, taking j = KgNq:
15.112  MLCja 
ML distributes over C in S4.2, which is contained in K4:
15.113  CMLjMLa 
By the nonLewis modal axiom M22, LMpMLp this transforms to
15.114  CLMjMLa 
which in S4 yields
15.115  CLMjMLLa 
An application of CCLpMqMCpq which holds in S1° gives
15.116  MCMjLLa 
And then with S2°'s CMpLqLCpq we get, by SSS:
15.117  MLCjLa 
which is equivalent to
15.118  MLCgAqLa 
the interpretation of the conclusion of LK4's L. There then is an analogue of this rule in K4, and we may assert, with the aid of *15.17, *15.18, and *15.19
*15.20  A formula a is valid in Group II (in MK4) iff ® a is a theorem of LK4, and so also iff a is a theorem of K4. 
The finite size of the Group II matrix then gives us:
*15.21  Group II provides a decision procedure for K4. 
We note in passing that the formula
M24. ALpApqpNq
is valid in Group II and so by *15.20 a K4 thesis. Checking in MS5 will show that it is not an S5 thesis; it is not incompatible with S5, however, as M22 and M23 are; this may be verified by checking M24 in the 'twoinstant' version of MS5, which has the following table for L:
p =  1  2  3  4 
Lp =  1  4  4  4 
M24 always takes 1 in this matrix, as do all the theses of S5. Following Sobocinski 1970a, we shall call S4 + M24 V1 and S5 + M24 V2. Since M24 is valid in Group II, it cannot make CMLpLp provable when added to S4, and so V1 is properly contained in V2. We shall show later that V1 contains S4.9.
Semantics for S4.9; the 'last stop' before S5
We earlier remarked that S4.9 was a more appropriate name for the system S4.4 + M18 (or S4 + M19) than was Schumm's suggested S4.7. The reason for this will now become apparent: we shall show that there are no systems properly between S4.9 and S5. We shall do this by showing that the semantics for S4.9 are a combination of those of S5 and K4; the set of theorems of S4.9 is the intersection of the sets of theorems of S5 and K4.
First of all, let us suppose that a formula a is
(1)  A theorem of S5, and 
(2)  Invalid in Group II (and so not a K4 thesis). 
We note first that the rule L of LK4 contains that of LS4.4, which is a direct analogue of LS5's ®L. This means that whenever G ® Q is provable in LS5, G Q will be provable as a subtheorem of LK4; the semantic upshot of this is that the formula i(G ® Q) will always be true in MK4 worlds other than main worlds. This further means that in the binary representation of Group II, S5 theses will always take the value 1 in the second (end point) bit position, and so in the decimal notation for Group II values, S5 theses will always take either the value 1 or the value 3. The formula a noted above fails in Group II and is also an S5 thesis, so somewhere it takes the value 3. The n distinct variables of a are q_{1}, . . ., q_{n}. Take note of an assignment in Group II for which a takes the value 3; the variable q_{i}, for each i from 1 to n, will at that assignment take one of the values 1, 2, 3, or 4. We shall make substitutions into a for each of the n variables q_{i} depending on the value given that variable at this falsifying assignment as follows:
If q_{i} is given the value 1 substitute q_{i} / Cpp  
If q_{i} is given the value 2 substitute q_{i} / Np  
If q_{i} is given the value 3 substitute q_{i} / p  
If q_{i} is given the value 4 substitute q_{i} / KpNp 
The result of these substitutions is a formula a* which has only one variable, p. Furthermore, because of the way substitutions were made for the variables of a, a* will take the value 3 in Group II when p is assigned the value 3. We note that the formula MLpLp, M10, takes in Group II the value 3 at and only at the point where p is given the value 3  for other assignments, it takes 1. It will then follow that with p the variable of a*, the formula
15.119  Ca*MLpLp 
is valid in Group II. If a is added as an axiom, then, to the system whose theorems are those common to S5 and K4, and which thus includes 15.119, a* becomes provable by substitution and by *15.119, then, M10, the proper axiom of S5, becomes provable and extends the system to S5. We then have
*15.22  There is no system properly included in S5 and properly including the system whose theses are all and only those common to S5 and K4. 
We now wish to show that S4.9 is indeed the system referred to in *15.22. We do this by first proving a lemma applicable to axiomatic systems in general.
*15.23  Suppose X is a logic containing PC and having detachment and substitution as its rules of inference; suppose b is a thesis of the system X + a; then, if g has no variables in common with a, Ag*b is a thesis of X + Aga; g* has no variables in common with b and either is g or is formed by substituting variable for distinct variable in g (is congruent to g). 
Suppose b provable in a proof of length 1 in X + a. Then it is either an axiom of X or is a. If of X, then also of X + a, and Ag*b is provable by CpApq and appropriate substitutions; if b = a, then Ag*b = Aga and so is in X + Aga.
Suppose now that whenever b is provable in X + a in a proof of length £ k, Ag*b is also provable in X + Aga. Consider a b provable in a proof of length k + 1. Here b may be derived from a previous proof line d by substitution; d is then provable in k or fewer steps and so by the induction hypothesis, Ag*d is a thesis of X + Aga. Ag*b is then derivable from this last formula by the same substitution that gave b from d; note that g* may first have to be altered by appropriate substitutions for the distinct variable provisions of *15.23. On the other hand, suppose the (k + l)th step in the proof of b is a detachment, involving previous steps Cdb and d. By the induction hypothesis, Ag*Cdb and Ag*d are then theses of X + Aga. Taking the axiom Frege (CCpCqrCCpqCpr) with substitutions p / Ng*, q / d, r / b and the equivalence ECNpqApq, we get
15.120  CAg*CdbCAg*dAg*b 
which with two detachments involving the alternations holding by the induction hypothesis gives us Ag*b as a thesis, and *15.23 holds.
We note that S4 is a system which is axiomatizable using only the rules of detachment and substitution (see Chapter 11); S4.4 then is also so axiomatizable. In S4.2 formula M18 makes provable
15.121  AMLpLpLMqMLq 
The left member of this disjunction if added to S4.4 gives S5; the right member added to S4.4 gives K4. 15.121 is in S4.9. By *15.23, then, if a is a thesis of S5, AaLMqMLq (q not in a) is a thesis of S4.9; if also a is a thesis of K4, then, by *15.23 again, Aaa* (a and a* are congruent) is a thesis of S4.9; by simple substitution, Aaa and so a itself is an S4.9 thesis. This means that every formula provable in both S5 and K4 is provable in S4.9, which then is the intersection of S5 theses and Group II valid formulas. Formally:
*15.24  If a is a thesis of both S5 and K4, a is a thesis of S4.9. 
We then get, from *15.22:
*15.25  There is no system properly contained in S5 and properly containing S4.9. 
We may use the above results quickly to establish a number of things about S4.9. First of all, we earlier proved that S4.9 is included in the system S4 + M19 (AMLpLpMLMqCqLq); by noting that M19 is both an S5 thesis and is valid in Group II, we see that S4 + M19 = S4.9. Next, take note of the formula
M25. MLpALpApNqCpq
As this formula follows from MLpLp, it is a thesis of S5; the reader may verify for himself that it is valid in Group II. It is then a thesis of S4.9. Further, the consequent of M25 is equivalent in PC to formula M24; M25 is then a thesis of the system V1 (S4 + M24). Assume S4.4 + M25:
15.122  MLpCNLpCMKpqpq  M25, S1° 
15.123  MLpCLMqMKpq  S4° 
15.124  MLpCNLpCMLpCLMqpq  15.122, 15.123, S1° 
15.125  pqCMLpMLq  S3° 
15.126  MLpCNLpCMLpCLMqCMLpMLq  15.124, 15.125, S1° 
15.127  MLpCNLpCLMqMLq  15.126, S1° 
15.128  ACMLpLpCLMqMLq 
This last formula clearly yields axiom M18; S4.4 + M25, then, contains and so is equivalent to S4.9, which is then a subsystem of V1 .
If we test the formulas M20 and M21 in Group II, we find that they are valid there; these formulas are also theses of S5, and so too of S4.9. S4.6 (= S4.4 + M20 or S4 + M21) is then S4.9.
The systems discussed in this book are not by any means all of the Lewis modal and closely related systems. One might have discussed in this work the system B, for example, which is T + Lpp, and whose possible world semantics involve an accessibility relation which is reflexive and symmetrical but not transitive. Or the systems containing the unusual thesis MMp might have been investigated  S6 = S2 + MMp; S7 = S3 + MMp; S8 = S3 + LMMp (the reader interested in more detail on these systems might refer, for example, to Hughes and Cresswell 1968). We have chosen to study a line of systems between Sl° and S5, with a few digressions. One gets the uneasy feeling as one discovers and studies more and more of the systems belonging to this family that it is literally a family, and has the power of reproducing and multiplying, proliferating new systems without limit. In the interest of concluding this book, then, we shall choose the present instant as the conclusion of this study. The reader who has stayed with us this far should by now have a good feeling for the literature of modal logic, he should be able to find material on these systems, and also she should have a reasonable ability to work with that literature. We conclude, then, with a table summarizing the axiomatizations of this chapter, and a diagram showing the containment relationships between these systems.
S4.1  = S4 + M13, pLppCMLpp or M14. pLpLpCMLpLp 
S4.1.4  = S4 + M15, pLppCLMLpp 
S4.2  = S4 + M12, MLpLMp 
S4.2.1  = S4.2 + M13 
S4.3  = S4 + M11, ALpqLqp 
D (S4.3.1)  = S4.3 + M13 
S4.3.2  = S4 + M17, ALpqCMLqp 
S4.3.3  = D + M20, CLMpCLMqCMKpqLMKpq 
S4.3.4  = S4.3.2 + M20 
S4.4  = S4 + M16, pCMLpLp 
S4.9  = S4.4 + M20 
= S4 + M21, CpLMpCCqLMqCMKpgLMKpq  
= S4.4 + M18, ACMLppCLMqMLq  
= S4 + M19, AMLpLpMLMqCqLq  
V1  = S4 + M24, ALpApqpNq 
V2  = S5 + M24 
K1  = S4 + M22, LMpMLp 
K2  = S4.2 + M22 
K3  = S4.3 + M22 
K3.1  = D + M22 
K3.2  = S4.3.2 + M22 
K4  = S4.4 + M22 
Arrows go from containing to contained systems
Systems left of solid (red) line are not in S5
Systems left of broken (blue) line are incompatible with S5