10.

THE SYSTEMS OF COMPLETE MODALIZATION -- S3° AND S3

The system S3°

WE now get to the system which must be considered the ancestor of the modern modal systems, S3. As with prior systems, we shall begin the study of S3 with an investigation of a proper subsystem of it S3°, which stands to S3 as the other 'nought' systems stand to their respective full systems. S3 is the system which Lewis formulated in his Survey of Symbolic Logic, 1918; it thus antedates the systems of SL by fourteen years. Actually, the system as presented in 1918 was not quite right; it contained as an axiom the formula pqNMqNMp. This formula is too strong; its presence in this modal system is sufficient to destroy the modal character of the system. This was noted by Post and then corrected in Lewis 1920. This law of transposition for impossibility should hold in just one direction; Lewis has the corrected version of it in SL as his axiom A8; it is pqNMqNMp. We shall employ a slight modification of this formula as our proper axiom for S3°; it is the deductively equivalent

M8. pqMpMq

Axiom M8 when added to Sl° yields S3° (Sobocinski 1962).

The first thing we note about S3° is that it contains S2°:

10.1 MKpqMp S(Μ5)(Μ2)

Formula 10.1 is M7, the proper axiom of S2°. Immediately noticeable about S3° is the fact that M8 is very like formula 5.64 of S1°, except for having the principal connective of its consequent a strict rather than a material implication. As should be evident, M8 and S1° make provable in S3°:

10.2 pqLpLq  
10.3 pqNMqNMp  
10.4 pqNLqNLp  

For later use, we prove a slightly extended version of 10.2:

10.5 pCqrLpLCqr 10.2, q / Cqr

We now make use of the S2° version of semisubstitutivity of strict implication (SSS); note that the subformula LCqr of 10.5 is in a C-pos:

10.6 pCqrLpCLqLr 10.5, 5.61, SSS

The feature of having the principal connective of the consequent a strict rather than a material implication in many theses is typical of S3°:

10.7 CpqCCqrCpr *5.1
10.8 pqCqrCpr 10.7, S2° (BKR)
10.9 pqqrpr  S(M5)(J(10.8)(10.2))

This is a version of syl in which all implications are strict. Beginning with the thesis CqrCCpqCpr rather than 10.7, and performing the same operations on it as on 10.7, we get

10.10 qrpqpr  

which is a 'weak syl' version of 10.9.

10.11 Lpqp S2°
10.12 LpLqLp S(Μ5)(J(10.11)(M8))

This is a strict implication version of simp.

Semisubstitutivity of strict implication in S3°

If we return to the proof of the semisubstitutivity of implication for the positive implicational calculus (Chapter 2), we see that the key formulas used in that proof were syl and weak syl. The theoremhood of 10.9 and 10.10 thus suggests that a version of SSS analogous to the strongest PC version of SSI might be proved in S3°. This is indeed the case; the following version of SSS will hold in S3°:

*10.1
Let the wff y be like j except for having an occurrence of the wf subformula b where j has a. Then in S3°:

if a is in C-pos in j, abjy;

if a is in A-pos in j, abyj.

This metatheorem is, of course, stated just as is SSI for the propositional calculus (*2.2), except for having strict implications where *2.2 has material. The proof of SSS in S2°, *6.7, may easily be altered to prove the S3° version. The induction is on the total number of K's, N's, and M's in whose scope a stands; when that number is zero, a = j and b = y, so even in S1° we have as a thesis abjy as an instance of Cpp. At the induction step, when the leftmost connective of j is a K or an N, we have the S1° thesis pqNqNp and the S2° theses pqKprKqr and pqKrpKrq which are employed in this proof much as their material implication analogues are used in the proof of SSI for the propositional calculus. For the case in which the (k + 1)th, the leftmost, connective of j is M, we obviously shall employ axiom M8 to move from the stronger induction assumption required for S3° to the proof of *10.1 just as one of Becker's rules was used to move from the weaker induction assumption of the S2° version to the proof of SSS for that system.

With *10.1 holding, we shall be able to prove a stronger version of the substitutivity of strict equivalence than is postulated for these systems; details of the proof are left to the reader:

*10.2
Let j, y, a, and b be as in *10.1; then in S3°:

abjy

More theorems of S3°

We move to the proof of other theses of this system:

10.13 LpCLLqLLp S(M5)(J(10.12)(5.61))
10.14 pCqrqCpr S1°
10.15 LLqCLpLLp S(10.14)(10.13)

We recall that the addition of any thesis of form LLa to Sl° made provable a rule to infer LLb from any thesis Lb; 10.15 expresses an even stronger principle. As we shall see, 10.15 itself may be strengthened.

10.16 LLpCLLpLLLp 10.15, p / Lp, q / p
10.17 pCpqpq S1°
10.18 LLpLLLp S(10.17)(10.16)

This is a thesis unlike any we have seen until now; it moves from a shorter to a longer string of L's.

At this point we shall digress slightly to deal with a principle that will prove handy in work to come; this is a notion of 'duality' for modalities. Let F be a positive or negative modality (in the sense of a modal prefix -- a string of N's, M's, and L's). The 'dual' of F will be the modality formed by replacing each of F's M's by an L and each of its L's by an M. We then have:

*10.3
Where F* and G* are the duals respectively of F and G,

If FaGb, then G*NaF*Nb,
and in particular.

If FpGp, then G*pF*p.
This holds for S1°

We note first that we can easily prove that F*pNFNp holds; this is done by induction on the length of F. If F is empty, this formula is a case of pNNp, double negation. If the first (primitive notation) character of F is an N, at the induction step, then F is of form NG, where G is a modality falling within the induction hypothesis, and so making G*pNGNp hold. By the form of F, NNGNpNFNp is a case of the law of identity, and so by SSE and the previous formula, we get NG*pNFNp. But in this case, NG* is precisely F*, and so F*pNFNp holds. If the first (primitive notation) character of F is an M, then F is of form MG, and as above, G*pNGNp holds by the induction hypothesis. NFN is now NMGN, and so by double negation, NMNNGNpNFNp holds. By the previous formula, SSE, and Df. L, this means that LG*pNFNp holds. But here LG* is the dual of MG, which is F; thus F*pNFNp holds. Since this is the case, by transposition and double negation we easily prove the first part of *10.3, and then taking a = b  = p and using p / Np and double negation, we prove the second part of that metatheorem. We shall refer to this principle by its number, *10.3, or simply as 'duality'.

We may now make a first use of *10.3:

10.19 MMMpMMp 10.18, duality

We go on now to prove the promised stronger version of 10.15:

10.20 LLLqLpLLp S(10.2)(10.15)
10.21 LLqLpLLp S(M5)(J(10.18)(10.20))

 Thus, if any thesis beginning with two L's is provable in S3°, LpLLp will be provable. By duality, this is clearly deductively equivalent to MMpMp, which we shall eventually take as the proper axiom of S4°, a system stronger than S3°.

Inclusion, containment, and independence with S3° and S3

We shall soon be discussing the full system S3 which, as might be expected, is formed by the addition of M6, pMp, to S3°. S3° is clearly a subsystem of S3; that it is a proper subsystem is shown by matrix t1, which verifies all S3° theses, but -- of course -- fails to verify M6. As we have noted (see formula 10.1), the system S2° is included in S3°; S2 is then included in S3. That these containments are proper is shown by the matrix t5, due to Parry 1934:

p = 1* 2* 3 4 5 6 7 8
Mp = 1 1 1 1 1 1 3 8
Lp= 1 6 8 8 8 8 8 8

These tables for M and L are to be considered added to the standard eight-valued tables for the PC connectives earlier discussed; the designated values are 1 and 2. All theses of S2 (and so of S2°) are verified by t5, but consider axiom M8 with p = 7 and q = 8: LCLC78LCM7M8 = LCL2LC38 = LC6L6 = LC68 = L3 = 8. Axiom M8 (and, indeed, the version of M8 with the main connective material rather than strict implication) is therefore not an S2 thesis, and S3 contains S2 and S3° contains S2° properly.

We may note that t5 verifies not only S2, but the system T as well, for validity in t5 is inherent through the rule to infer La from any thesis a. Thus S3 is not contained in T, nor S3° in T°. If we now examine matrix t3, we see that it verifies not only the theses of S2, but axiom M8 as well. Since t3 fails to verify any formula of form LLa, we see that S3 is not contained in T. S3 and T, then, are independent systems, as are S3° and T°.

The full system S3

As we have remarked, S3 is formed by the addition of pMp to S3°. S3 is a system that is, in a very important respect, markedly different from T and systems contained in T. As we have shown, these systems contain an infinite number of non-equivalent modalities. As we shall see, S3 has only a finite number of non-equivalent modalities, forty-two to be precise, including the improper modalities p and Np, and forty proper modalities. That this is the case was first shown by Parry 1939.

Twenty of these proper modalities are what we have called positive modalities, and the other twenty are negative, the negations of the twenty proper modalities. Most of our work, then, will be done with the positive modalities; the results for the negative modalities will then follow trivially.

An equivalence which allows us to replace one modality by another (such as MpNLNp) is known as a 'reduction thesis'. We begin our work in S3 by proving several important reduction theses.

10.22 LLLpLLp 5.91, p / LLp
10.23 MMpMMMp M6, p / MMp
10.24 LLpLLLp J(10.18)(10.22)
10.25 MMMpMMp J(10.19)(10.23)

The effect of the reduction theses 10.24 and 10.25 is that any string of L's or M's in S3 of length greater than two is precisely equivalent to one of length two and may always be replaced by one of length two, salva veritate. We now prove some important theorems showing implications between modalities.

10.26 pCNpq *5.1
10.27 LpNpLp 10.26, BKR, q / Lp
10.28 LpMNpMLp S(M5)(J(10.27)(M8))

Noting that MNp is in A-pos in 10.28 and recalling that 5.91 is Lpp:

10.29 LpLMNpMLp 10.28, 5.91, SSS

LMN is a modality clearly equivalent to NML (cf. the proof of *10.3); thus formula 10.29 becomes

10.30 LpNMLpMLp  

As one half of the equivalence 5.50 we have NppLp; thus:

10.31 LpLMLp 5.50, S1°

This is a key theorem among those expressing the relationships of modalities in S3.

10.32 MLMpMp 10.31, duality
10.33 LLpLLMLp 10.31, BKR
10.34 MMLMpMMp 10.33, duality

We now establish what amount to further reduction theses in S3, proving the formulas MMLpMMLLp and LLMpLLMMp.

10.35 LLpLp 5.91, p / Lp
10.36 MMLLpMMLp S(M8)(S(M8)(10.35))

Proof of the converse of 10.36 takes more effort:

10.37 LpNpLLp 10.26, BKR, q / LLp
10.38 LMMNpMMNp 5.91, p / MMNp
10.39 LLMMNpMMNp 10.38, *5.6
10.40 LpMNpMLLp S(M5)(J(10.37)(M8))
10.41 LpMMNpMMLLp S(M5)(J(10.40)(M8))

Note that MMNp is in an A-pos in 10.41:

10.42 LpLMMNpMMLLp 10.41, 10.39, SSS
10.43 LpNMMLLpMMLLp 10.42, duality, SSS
10.44 LpLMMLLp 10.43, 5.50, SSE
10.45 MLMMLLpMMLLp 10.32, p / MLLp

Observe that subformula LMMLLp of the antecedent of 10.45 is in an A-pos in that formula. We then have

10.46 MLpMMLLp 10.45, 10.44, SSS
10.47 MMLpMMMLLp 10.46, BKR
10.48 MMLpMMLLp S(M5)(J(10.47)(10.23))

We thus have the converse of 10.36, and so

10.49 MMLpMMLLp J(10.48)(10.36)
10.50 LLMpLLMMp 10.49, duality

We now employ these reduction theses:

10.51 LLMLpLLMLp S1°
10.52 LLMLpLLMMLp 10.51, 10.50, SSE
10.53 LLMLpLLMMLLp 10.52, 10.49, SSE
10.54 LLMLpLLMLLp 10.53, 10.50, SSE

We use the above equivalence to establish another implication between modalities in S3; with 10.54 holding, it is clear that the following holds:

10.55 LLMLpLMLLp  
10.56 MLMMpMMLMp 10.55, duality

We now state a batch of formulas that result fairly directly from what we already have

10.57 MpMMp 10.35, duality
10.58 LMLpMLp 5.91, p / MLp
10.59 LMpMLMp 10.58, duality
10.60 LMLpLMp S(10.2)(S(M8)(5.91))
10.61 MLpMLMp 10.60, duality
10.62 LMLLMpLMp S(10.2)(10.32), 5.91, SSS
10.63 MLpMLMMLp 10.62, duality
10.64 LMpLMMp S(10.2)(S(M8)(M6))
10.65 MLLpMLp 10.64, duality
10.66 LMLpLMMLp 10.64, p / Lp
10.67 MLLMpMLMp 10.66, duality
10.68 LMLLpLMLp S(10.2)(10.65)
10.69 MLMpMLMMp 10.68, duality
10.70 LMLLpMLLp 10.58, p / Lp
10.71 LMMpMLMMp 10.70, duality
10.72 LLMLpLLMp S(10.2)(10.60)
10.73 MMLpMMLMp 10.72, duality
10.74 LLMpLMLLMp 10.31, p / LMp
10.75 MLMMLpMMLp 10.74, duality
10.76 LMMLpLMMp S(10.2)(S(M8)(S(M8)(5.91)))
10.77 MLLpMLLMp 10.76, duality
10.78 LMLLMpMLLMp 5.91, p / MLLMp
10.79 LMMLpMLMMLp 10.78, duality
10.80 LMLLpLMLLMp S(10.2)(10.77)
10.81 MLMMLpMLMMp 10.80, duality

Involved in formulas 10.31-10.35 and 10.55-10.81 are exactly twenty modalities. These modalities are all and only the irreducible non-equivalent positive proper modalities of S3; analogous formulas for the negative proper modalities may be obtained by applying pqNqNp to each of these formulas. The relationships given above are summarized in the following diagram:

A diagram for the negative modalities may be constructed, of course, by prefixing an N to each of the modalities in this diagram and reversing each of the arrows; an arrow going from one modality to another indicates that the first implies the other. We shall go on to show that the modalities indicated in this diagram are indeed all and only the non-equivalent positive proper modalities of S3. We shall show, indeed, that the above diagram expresses completely the implication relations between these modalities (assuming, of course, the transitivity of this relation). We note that the longest modalities in this diagram consist of five characters, LMLLM and MLMML. We shall therefore first investigate all modalities with five or fewer characters; as a start here, we shall prove another pair of reduction theses for S3:

10.82 MLpMLMLp S(M8)(10.31)
10.83 MLMLpMLp 10.32, p / Lp
10.84 MLpMLMLp  J(10.82)(10.83)
10.85 LMpLMLMp 10.84, duality

We now shall display in a table first of all the possible modalities having four or fewer characters. Eighteen of these are included in the above diagram and are claimed to be irreducible. The others are indicated to be equivalent to one or another of the irreducible modalities.
1 Char 2 Char 3 Char 4 Char
  Equiv   Equiv   Equiv   Equiv
M   MM   MMM  = MM MMMM  = MM
L   ML   MML   MMML  = ML
    LM   MLM   MMLM  
    LL   MLL   MMLL  = MML
        LMM   MLMM  
        LML   MLML  = ML
        LLM   MLLM  
        LLL  = LL MLLL  = MLL
            LMMM  = LMM
            LMML  
            LMLM  = LM
            LMLL  
            LLMM  = LLM
            LLML  
            LLLM  = LLM
            LLLL  = LL

Irreducible Modalities Have This Background Color

Reducible Modalities Have This Background Color

The indicated equivalences are obvious by the reduction theses 10.24, 10.25, 10.49, 10.50, 10.84, and 10.85. We see, then, that there are at most eighteen irreducible positive proper modalities with four or fewer characters in S3.

We now may turn to the modalities having exactly five characters. Again we shall display them in a table; here only two of them are irreducible. We note that the others reduce to modalities having fewer than five characters. We leave to the reader the exercise of carrying out the details of the reductions, using again the reduction theses given above.

MMMMM  = MM
MMMML  = MML
MMMLM  = MMLM
MMMLL  = MLL
MMLMM  = MMLM
MMLML  = MML
MMLLM  = MMLM
MMLLL  = MML
MLMMM  = MLMM
MLMML  
MLMLM  = MLM
MLMLL  = MLL 
MLLMM   = MLLM
MLLML  = MLL
MLLLM  = MLLM
MLLLL  = MLL
 
LMMMM  = LMM
LMMML  = LMML
LMMLM  = LMM
LMMLL  = LMML
LMLMM  = LMM
LMLML  = LML
LMLLM  
LMLLL  = LMLL
LLMMM  = LLM
LLMML  = LLML
LLMLM = LLM
LLMLL = LLML
LLLMM = LLM
LLLML  = LLML
LLLLM  = LLM
LLLLL  = LL

The reader might find it easiest in the case of MLLML and LMMLM to prove specific reduction theses for those modalities.

What now of the possible modalities having more than five characters? Since each of the five character modalities except MLMML and LMLLM reduces to a modality of fewer than five characters, it is clear that the addition of an M or an L to the front or the back of any five-character modality but these two will yield a modality with no more than five characters. Now consider MLMML; prefixing an L to this gives LMLMML, which reduces to LMML. Prefixing an M to it gives MMLMML, which reduces to MMLML, which in turn reduces to MML. Adding an L to the end of MLMML gives MLMMLL, which reduces to MLMML itself. Adding an M to the end of MLMML gives MLMMLM, which reduces to MLLM. The possible extensions of LMLLM to six characters will reduce similarly by duality. Any modality (positive proper) of six characters, then, will reduce to one of five or fewer; this means, of course, that any such modality of n + 1 characters, where n ³ 5, will reduce to one of n or fewer characters. A simple induction then shows that any positive proper modality will reduce to one of five or fewer characters, and so ultimately to one of the twenty we claim to be irreducible.

We have thus shown that there are no more than twenty positive proper modalities in S3, and so no more than forty proper modalities over all. We must now show that there are no fewer than these, and that the implications indicated earlier are all those obtaining between these modalities. To do this, we first divide the positive proper modalities into four groups. Group A consists of those beginning with an L and ending with an L. Group B is those beginning with an M and ending with an L; C contains those beginning with an L and ending with an M, and D has those both beginning with and ending with an M. We now define a matrix t6, formed by adding to the standard tables for the propositional calculus connectives the following:

p = 1* 2* 3 4
Mp = 1 2 1 4
Lp = 1 4 3 4

We shall also use a matrix t7, whose modal table is

p = 1* 2* 3 4
Mp = 1 1 1 4
Lp = 1 4 4 4

And we define the following eight-valued t8:

p = 1* 2* 3 4 5 6 7 8
Mp = 1 1 1 1 1 1 3 7
Lp= 2 6 8 8 8 8 8 8

t6 and t7 are 'Group II' and 'Group III' respectively of SL; t8 is due to Parry 1939. 1 and 2 may be taken as designated values in each of these matrices. t7 enables us to show that, as indicated by our diagram, no member of group D or group C of modalities implies any member of group A or group B. In t7 (which like the other two matrices, of course, verifies S3) any positive modality ending with an L behaves precisely like an L and any ending with an M like an M. Since MpLp fails in this matrix, so too will any implication of a modality ending with an L by any ending with an M.

We can also show that no member of group B or D implies any member of group A or C. The modalities of A and C all begin with an L, while those of B and D begin with M. Matrix t3, which verifies S3, is such that any modality whose first character is L can take only the values 2 or 4, and any whose first character is M can take only the values 1 or 3. If, then, a is from B or D and b is from A or C, Cab can take no value higher than 2, and so ab will always take the value 4, which is not designated. All the above observations, of course, apply in transposed form to the negations of these modalities.

Speaking of negations, we can easily establish that no positive modality implies any negative one and vice versa by using the ordinary two-valued matrix, taking M1= L1=1 and M0 = L0 = 0.

We may now turn our attention to the relationships between the modalities belonging to group A. We shall set up a table, each line of which will account for one or more of these relationships. Some of the lines will be justified by reference to a matrix and a value at which that matrix fails to verify the relevant implication. Some of the lines will be justified by the statement 'to be shown in LS3'; we shall in a later chapter define a sequent-logic equivalent to S3 and shall use that system to show that these implications do not hold. Some of the lines will be justified by reference to another line. For example, if L or any of the modalities which L implies were to imply LLML, say, then -- given the implications indicated in our diagram -- L would have to imply MLLM. If L does not imply MLLM, then, neither L nor any modality it implies can imply LLML. Thus we may justify the statement that L, LML, and LMML do not imply LLML by reference to the fact that L does not imply MLLM. And this statement, although it involves a modality not in group A, will be the first line in our table for A, since we shall use it in a number of places.

(A1)   L fails to imply MLLM, by t3 @ p = 1
(A2)   LL implies all of group A
(A3) LLML fails to imply L, by t6 @ p = 3
(A4)   LLML fails to imply LL, by (A3)
(A5)   LMLL fails to imply LL, L by (A3)
(A6)   LMLL fails to imply LLML, by t8 @ p = 1
(A7)   L fails to imply LL, LLML, LMLL, by (A1)
(A8)   LML fails to imply LL, LLML, LMLL, by (A1)
(A9)   LML fails to imply L, by t6 @ p = 3
(A10)   LMML fails to imply LML, by t3 @ p = 4
(A11)   LMML fails to imply LL, LLML, LMLL, L, by (A10)

This table establishes that the only implications holding between members of group A are those shown in our diagram. Since the members of group D are the duals of A, the table for A establishes this result for D as well. Clearly, it follows also that no member of A is equivalent to any other member of A, and none of D is equivalent to any other of D.

We turn now to the relationships obtaining between members of group C, constructing a table just as we did for A.

(C1)   LLM implies all of group C
(C2)   LMLLM fails to imply LLM, by t8 @ p = 1
(C3) LM fails to imply LLM, LMLLM, by (A1)
(C4)   LMM fails to imply LLM, LMLLM, by (A1)
(C5)   LMM fails to imply LM by t3 @ p = 4

Thus the only implications holding between members of C are those shown in our diagram; the analogous result holds for group B by duality.

The next step is the relationships between members of A and members of B.

(AB1)   LL, LLML, LMLL imply all of group B
(AB2)   L fails to imply MLL, by (A1)
(AB3) LML, LMML fail to imply MLL, by (A1)
(AB4)   LMML fails to imply ML, by t3 @ p = 2

Thus the only relations obtaining between A and B are those shown in the diagram (recall that no member of B can imply one of A). That the relationships shown to hold between groups C and D are the only implications holding there follows by duality. We now turn to the implications between A and C.

(AC1)   LL, LLML imply all of group C
(AC2)   LMLL fails to imply LLM by t8 @ p = 1
(AC3) L fails to imply LLM, LMLLM, by (A1)
(AC4)   LML fails to imply LLM, LMLLM, by (A1)
(AC5)   LMML fails to imply LLM, LMLLM, by (A1)
(AC6)   LMML fails to imply LM, by t3 @ p = 4

So the indicated implications between A and C are the only ones there obtaining. By duality, the same will hold for the indicated implications between B and D. Since we have already established that no member of D or C implies any of A or B, and no member of D or B implies any of A or C, this means that the implication pattern given in the diagram is complete, and we may assert

*10.4 The twenty modalities shown in the diagram are all and only the positive proper irreducible modalities in S3; further, the implications indicated are all and only those holding between these modalities.

The above results apply analogously to the negative proper modalities, giving us forty proper irreducible modalities in all in S3.

We may now consider the improper modality in its relationship to the proper modalities. By 5.91, LLp and Lp both imply p, which in turn, by M6 imply Mp and MMp. We note that these are the only of the twenty proper modalities in our diagram which are not mixtures of L's and M's. Now observe that in matrix t6 any modality (positive) which is a mixture of L's and M's prefixed to a p will take the values 1, 4, 1, 4 as p takes the values 1, 2, 3, 4 respectively. At p = 2, then, p fails to imply any such modality, and at p = 3, any such modality fails to imply p. Also, in any of the matrices we have been using, it is clear that p fails to imply Lp or LLp and Mp and MMp fail to imply p. The following is, then, the only string of positive irreducible modalities involving the improper modality:

LLp ® Lp ® p ® Mp ® MMp

For the negative modalities, of course, prefix each of the above with an N and reverse the arrows.

S3 and complete modalization

We have indicated that S3° and S3 are members of a subfamily of the Lewis modal systems called the systems of complete modalization. We shall now give some attention to the notion of complete modalization. A formula a will be said to be 'completely L-modalized in the system X' if aLa is a theorem of X. a is 'completely M-modalized in the system X' if Maa is a thesis of X. We shall ordinarily refer to complete L-modalization simply as 'complete modalization'. A logic is a system of complete modalization if there are formulas completely modalized in it. It is clear that only systems of complete modalization can contain only a finite number of nonequivalent irreducible modalities. As examples of completely modalized and completely M-modalized formulas in S3, we have LLp and MMp. We can use the notion of complete modalization to prove rules of inference parallel to *5.6-*5.9 which hold in S1 (recall that these rules permit us to insert an L in front of the antecedent or an M in front of the consequent of a theorem which is a material or a strict implication). The parallel rules for the insertion of L before a consequent or M before an antecedent are these

*10.5 If a is completely modalized and Cab (ab), then CaLb (aLb),
*10.6 If b is completely M-modalized and Cab (ab). then CMab (Mab).

It is true that these rules hold for all systems of complete modalization. We shall see that the notion of complete modalization offers us an interesting way of axiomatizing several systems including S4°, which we shall be studying soon. Also, it offers a method of approaching the question of sequent-logics corresponding to some of these systems.

The notion of complete modalization will operate similarly so far as S3 is concerned, but oddly enough, the notion we shall use in connection with axiomatizing and Gentzenizing S3 and S3° is not that proper to S3 itself, but rather the notion appropriate to S4°  and S4. We shall now make use of that notion in order to prove a metatheorem about S3° in preparation for work in future chapters.

First of all, we shall say that a formula is completely modalized in the basic sense of S4 iff it is of form La or is a conjunction only of formulas beginning with L. We then state:

*10.7
If (1) g is completely modalized in the basic sense of S4, and
  (2) for some b, ALba is a PC thesis, and
  (3) Cga is an S3° thesis,
then gLa is an S3° thesis.

We set down our hypotheses and go on with the proof:

10.86 Cga Hyp
10.87 ALba (in PC) Hyp.
10.88 NLba 10.87, S1°

We note now that with the present definition of complete modalization, there will always be a formula d such that gLd holds. Thus:

10.89 CLda 10.86
10.90 Lda 10.89, RL2
10.91 ANLbLda 10.88, 10.90, S1°
10.92 LANLbLdLa 10.91, BKR
10.93 LdLANLbLd 10.12, p / d, q / b, Df. A
10.94 LdLa S(M5)(J(10.93)(10.92))

Relying again on the equivalence gLd, we write

10.95 gLa 10.94

as is required for the proof of *10.6.

The 'unreasonableness' of S3 and its included systems

We conclude our present discussion of S3 with an investigation of an unusual feature of it and its included systems, discovered by Hallden 1951. It is relatively easy to show using our sequent-logic LIC that if a formula Aab is a thesis of the intuitionist calculus IC, then either a or b must be a thesis. The requirement for the classical PC so far as theses of form Aab is concerned is not quite so rigorous; a and b may both be non-theses, but it is easily established that if this is the case, at least they must have a variable in common. We shall see that this is not the case with S3 and some of its included systems. Following McKinsey 1953 we shall call a system of logic 'unreasonable (in the sense of Halden)' if there are formulas a and b such that:

(1) Neither a nor b is a thesis of the system
(2) a and b have no variable in common
(3) Aab is a thesis of the system.

As we have noted, neither of the calculi IC and PC is unreasonable in this sense. However, in S3° we have

10.96 AMMqLpLLp 10.21, q / Nq, S1°

Neither of the disjuncts is an S3 thesis, and so S3 and S3° are unreasonable. This, by the way, is interesting, for the addition of the right disjunct to S3 gives S4, as we have noted, and the addition of MMq as an axiom to S3 gives a consistent system called S7; the reader can easily determine, however, that if both disjuncts of 10.96 were added to S3, the result would be an inconsistent system.

We can go even further in the unreasonableness results; the following is an S1° thesis:

10.97 KpNpKqNq  

As a substitution instance of the PC thesis ApNp we have

10.98 AMKpNpKpNpNMKpNpKpNp  
10.99 AMKqNqKqNqNMKpNpKpNp 10.98, 10.97, SSE

This last is then a thesis of S1°. In matrix t3, however, the formula which is the left disjunct of 10.99 takes the value 4 for any assignment of values to its variables, and in matrix t7 the other disjunct is similarly falsified. Since both of these matrices satisfy S3, neither disjunct is an S3 thesis, and so not a thesis of any system included in S3; all the systems between and including S1° and S3, then, are unreasonable in the sense of Hallden.