15.

THE SYSTEMS OF COMPLETE MODALIZATION -- THE S4-S5 SPECTRUM AND RELATED SYSTEMS

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

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.

which is equivalent given S4 to the earlier-mentioned 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 set-theoretical (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 sequent-logic 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 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

*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 L-r 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₁, . . ., 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 L-r. Do it as follows:

We shall indicate how to show that there is a principle in LS4.3 corresponding to rule L-r(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 L-r 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 L-r(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

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

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₁, . . ., a_n excluding a_i. As induction hypothesis for our generalization, we then assume that the sequent

When we have a situation in the application of L-r(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 L-r(4.3) are then sequents

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

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 sequent-logic for S4.3; let LS4.2 be the sequent-logic resulting from the replacement of LS4's ®L by

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

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

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

where q is the conjunction of the members of Q. Applying RL to 15.40 and then distributing the L we get

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

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

which is PC equivalent to the interpretation of the conclusion of ®L for LS4.2. We shall then be able to say:

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 L-r 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 L-l 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 L-r steps required gives us:

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 L-r (and leave the rest of the structure as in MS4):

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

*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 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

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