The system S4°

WE now turn to other systems based on S1°. As before, we add to S1° an axiom, in this case:

M9. MMpMp

This formula plus S1° yields S4° (Sobocinski 1962). As a theorem of S4° we clearly have

11.1

LpLLp

M9, duality

Since it containsS1°, S4° has as a thesis formula 5.64, pqCMpMq. Containing S2°, it also has Becker's rules, and so

11.2	LpqMpMq	5.64, BKR
11.3	pqMpMq	S(M5)(J(11.1)(11.2))

This last formula is axiom M8; S4°, then, contains S3°.

It is clear that S4° is a system of complete modalization in the sense discussed in Chapter 10, and that metatheorems *10.4 and *10.5 hold in S4° when complete modalization is as it was defined for S4 in the statement of *10.6.

S4°, S4, and the previously discussed systems

The full system S4

Since S4 contains S3, it has as theorems all the reduction theses of S3, and so can have no more non-equivalent irreducible modalities than does S3. And in addition, it is clear that as theorems of S4 we have

11.4	LpLLp
11.5	MpMMp

These are more powerful reduction theses than those of S3, permitting a string of L's of any length to be reduced to one, and the same for any string of M's. An examination of the diagram showing the relationships between the S3 modalities will then tell us that the proper positive modalities of S3 reduce to no more than the following six modalities for S4 with the addition of 11.4 and 11.5 to S3: L, LML, ML, LM, MLM, and M. The formulas relating these modalities (which are, of course, S4 theses as well as S3) are 10.31, 10.32, 10.58, 10.59, 10.60, and 10.61. The reader may verify for himself that the proofs of these formulas (in particular of the first two) are far more straightforward and natural in S4 than they are in S3. A diagram follows of the relations between the S4 modalities as expressed by the cited theorems.

As was the case with the S3 modalities, this diagram may be turned into a diagram of the relations between the negative modalities by negating each of the six modalities and reversing the arrows. To aid in showing that the indicated implications are the only ones holding in S4 we set down the following matrix due again to Parry 1939:

The only relationships remaining to be investigated are those between modalities which in S3 were members of group 'A' -- L and LML (and the dual relationships between M and MLM, group `D').

We see then that the relationships shown in our diagram are all and only the implications holding between the positive proper irreducible modalities, and S4 then contains just six such modalities or twelve proper modalities in all. The pattern of implications involving the improper positive modality will, of course be

Lp ® p ® Mp

The system S5

We have mentioned that there is a definite relationship between the intuitionistic IC and the system S4, which relationship we shall study later. One might ask if there is a modal system bearing an analogous relationship to the classical PC. The answer is affirmative, and the modal system in question is that of the present section, S5. But, one might ask, what became of the `nought system' which corresponds to S5 as S1°, etc. correspond to S1, etc? Why not study that system before treating of S5 itself? The answer is that S5° does not exist. The proper axiom for S5 is -

M10. MpLMp

or its dual

11.6

MLpLp

which is obviously deductively equivalent to M10 in the presence of S1°. The reason that there is no S5° is that the addition of M10 to S1° makes axiom M6 immediately derivable, giving the system S5; this was first mentioned by Sobocinski 1962. Recall that S1° contains as a theorem formula 5.86, CCMpLqpq, which makes possible the proof of *5.4; this rule permits us to go from axiom M10 to

11.7

pMp

M10, *5.4

The original formulation of S5 was S1 + M10; by 11.7, S1° + M10 contains S1 and so is equivalent to the original S5. We continue with work in S5:

11.8	MLMpLMp	11.6, p / Mp
11.9	MMpMLMp	S(5.64)(M10)
11.10	MMpLMp	S(M5)(J(11.9)(11.8))
11.11	MMpMp	S(M5)(J(11.10)(5.91))

M2LM2 = 2L2 = 24 = L3 = 3, which is not a designated value. One might suspect that the modalities of S5 will be even fewer than those of S4; this is indeed the case. By M10 and 11.6 the following are theorems of S5:

11.12	MpLMp
11.13	LpMLp

An examination of the diagram of irreducible positive modalities in S4 will show that in the presence of 11.12 and 11.13 the modalities in S5 reduce to two (proper), L and M. The whole diagram of S5's irreducible modalities, then, is

Lp ® p ® Mp

The diagram for the negative modalities may be constructed as usual; there are, then, a total of six irreducible modalities in S5, four of them proper. A little consideration will convince the reader that any string of M's and L's in S5 will always be equivalent to its rightmost member, be it an M or an L.

Complete modalization in S5

As is the case with S3 and S4, the system S5 has its own peculiar notion of complete modalization. The following metatheorem will introduce us to that notion. (See Lemmon 1956.)

*11.1

Suppose that every propositional variable of a wff a is in the scope of one of a's modal operators. Then both aLa and aMa will be S5 theses.

The proof is by induction on the number of operators (K's, N's, M's) belonging to a. The shortest possible formula a meeting the requirements of *11.1 is of form Mp; by 11.5 and 11.12, then, we have both MpMMp and MpLMp; here *11.1 is proved for the base case of the induction.