Introduction

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 S1-S5 are mentioned there, but are not discussed in much detail.) One of the earlier attempts to extend this list of Lewis-modal 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

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 non-equivalent 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 non-equivalence 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

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 system S4.3

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 two-premiss rules in the sequent-logics). 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,

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:

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

We see then that 15.10 holds for S4.3 and so the interpretation of 15.9 will hold there, and so

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 A-r, 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 L-r 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:

ALpqLqp               Lqp               Lpq

( t1)   ( t2)                   CLqp                               CLpq

( t2)   ( t1)                   CLpq                               CLqp

We may now perform C-r in each of the new alternative tableaux; our L-l 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:

( t1)   ( t2)         CLqp Lq       p           CLpq Lp       q

( t2)   ( t1)         CLpq Lp       q Lq         q                   CLqp Lq       p Lp         p

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

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 L-r(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 L-r 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 L-r for each of the n above-mentioned sets will have a different one of the a₁, . . ., 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₁, . . ., 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 L-r(4.3) as stated here, *15.2 holds.

We now move on to another metatheorem:

The above figure establishes that there is m LS4.3 a principle corresponding to the inverse of L-r(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 sequent-logic 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

represent the sequence whose n members are:

is a theorem of LS4.3. This sequent may also be represented as

Let us first of all take p_k in the above as the formula ALp_kp_{k + 1}.

Then let us take p_k in 15.20 as the formula Ap_kLp_{k + 1}

We note that the sequent LAp_kLp_{k + 1}, LALp_kp_{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

We note that the sequents ALp_kLp_{k + 1} ® LAp_kLp_{k + 1} and ALp_kLp_{k + 1} ® LALp_kp_{k + 1} hold in LS4. The formulas forming the succedents of these two sequents are in C-pos in formulas in the antecedent of 15.23; by a sequent-logic analogue of SSS we shall be able to replace both these formulas in 15.23, then, by ALp_kLp_{k + 1}. Contracting the resulting duplicated sequence, then, we get:

But this sequent may be represented as

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

which corresponds to the state of the tableau in which the L-r(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 L-r. This means that *15.3 is established. By this last metatheorem, *15.1, *15.2, and *9.1, then, we have

By *9.2, then

The system S4.2

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

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):

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 L-r as appropriate:

CNLNLpLNLNp NLNLp       LNLNp         LNLp

LNLp LNp                 NLNp

NLp Lp         Np                 p p

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 L-r 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 'cut-like' rule such as that employed in MS5. With the help of *15.6, then, we may state

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 L-r, giving two auxiliary tableaux:

Lpq         Lqp

CLpq Lp       q           CLqp Lq       p

After the indicated C-r'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.

The Diodorean system D

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 curious-looking

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 L-l within the main tableau and then apply C-l to the resulting tableau:

pLpp		p
		LNLp
CpLpp
		pLp p		(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

NLp         pLp Lp		LNLp         CpLp p       Lp

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 L-r:

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:

pLpp       p         LNLp

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 false-that 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;

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

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

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 branching-but-not-converging model even with discrete instants. The infinitely alternating truth and falsity of p is compatible with MLp in a non-converging 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 branching-but-not-converging 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

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ⁿ values for some finite n. We noted that such values may be represented by the binary numbers from 0 to 2^n-1, 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 time-sequences, 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 here-in 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:

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 low-order bit position), and so Lp is false in each world, or over-all, 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 over-all, 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:

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).

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 C-pos

15.70

pLppCMLpp

The last is, of course, M13; S4.4, then, contains D. Let us now note the formula

M17. ALpqCMLqp

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.

LG LQ
	CONV
Q, LG LQ

We shall give an example of a proof in LS4.4:

Lp ® Lp ®N ® Lp, NLp Lp Lp .N Lp, NLp L Lp, LNLp CONV p, NLp ® Lp, LNLp

CUT

p ® Lp, Lp, LNLp CONTR p ® Lp, LNLp N® NLNLp, p ® Lp Df.M MLp, p ® Lp ®C(x2) ® CpCMLpLp ®L ® pCMLpLp

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

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

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

MLCLgALq1 . . . Lqn

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

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

This corresponds to the L-r rule for MS5. Suppose now that we have formulas La₁, . . ., 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:

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 L-r(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 C-r and one N-l 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 L-r here discussed):

			p				Lp
							LNLp
			NLp NLp
Lp

We have performed the N-r in the left of these tableaux-note that that tableau closes. We now note that in the other tableau we have both p and NLp left, and so clause (2) of L-r(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
		Lp

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 L-r(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 L-r. The construction is then a recipe for a proof of that formula in MPC + L-l, and the formula is then provable in LS4.4. Next, suppose that in such a construction L-r was used ('use' of (1) only does not count). There are then alternative sets in that construction in which clause (2) of L-r(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 L-r(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 'cut-like' 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 L-r(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:

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

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

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 K-N-L-primitive 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

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.

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°

The rule of L-r in the main tableau shall be MS4.4's L-r(4.4m) with its three clauses. We may interpret MK4 in our binary notation; with the high-order bit representing the main world and the low-order 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:

This is the table for Group II; indeed, it should be clear that

We then also have, by M22's validity in Group II:

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

G Q, a G Q, La

L

This rule corresponds to the revised L-r(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 ; L-r(K4a) does for the right side of an auxiliary tableau precisely what L-l 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 L-r(K4a) in the same way that the L in the succedent rules of the other systems we have studied correspond to their respective L-r 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: