The System S2

AS we remarked earlier, the calculus S1 was to serve as our basic modal logic; the other systems we treat will, in general, be presented as extensions of S1. The system S1 is itself such an extension. We now retrace our steps somewhat in that we shall be discussing a system which is not an extension of the most recently discussed system, S1, but an extension of S1 and actually independent of S1. This is the system S2, which contains theses not in S1, but which is lacking certain theses belonging to S1 -- specifically, the formula pMp and its consequences.

S2 is formulated by adding to S1 the additional axiom:

M7. MKpqMp.

It will be recalled that a material implication version of M7 is an S1 thesis; it is easily derivable from formula 5.82. That M7 itself is not a thesis of S1 may be shown by a matrix. For ease of reference, let us assign names to the matrices we employ: the matrix we are about to set down will be called t2, while the one previously used to distinguish S1 from S1 will be t1. t2 consists of the previously discussed standard four-valued tables for K and N and the following tables for M and L:

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

This matrix validates all the axioms of S1 -- indeed of S1. The property of always taking a designated value (1 or 2, as indicated by asterisk) is preserved by our rules of inference, as the reader may verify, so all S1 theses are validated by this matrix. But if we consider M7 with p = 2 and q = 3: MK23M2 = M4M2 = 32 = L2 = 4. But 4 is not a designated value, so M7 cannot be an S1 thesis (t2 is presented in SL as 'Group V').

But M7 always takes a designated value in matrix t1; all S2 theses are, then, validated by that matrix, and pMp and its consequences are independent of S2 just as they are of S1.

S2, then, is a proper extension of S1, and it neither contains nor is contained in S1-- it is independent of S1. Our first work with S2 will involve the proof of some derived rules of inference which are characteristic of the system:

*6.1 If ab, then MaMb.
*6.2 If ab, then LaLb.

We begin by setting up the premiss common to these two rules as a hypothesis:

6.1 ab Hyp.
6.2 CpqCpKqp *5.1
6.3 CpqpKqp S(5.61)(6.2), 5.43, SSE
6.4 aKba D(6.3)(6.1)
6.5 Kbaa 5.35, r / b, p / a
6.6 aKba J(6.4)(6.5)

Note that to this point the entire deduction beginning with the hypothesis 6.1 has been in S1. We now make our first use of the S2 proper axiom:

6.7 MKbaMb M7, p / b, q / a
6.8 MaMb 6.7, 6.6, SSE

Rule *6.1 has thus been proved. To get *6.2, we start again with formula 6.1:

6.9 NbNa S(5.17)(6.1)
6.10 MNbMNa *5.1
6.11 LaLb S(5.61)(6.2), 5.43, SSE

Thus *6.2 is also proved. It should be clear that on the basis of the above proofs a number of other such rules may be proved:

  If ab, then:
*6.3 MNbMNa
*6.2 NLbNLa
*6.3 NMbNMa
*6.4 LNbLNa

Rules such as *6.1-*6.6 are commonly referred to as 'Becker's rules'; they are, as we have remarked, a characteristic feature of S2. It is easy to see that the appending of one of these rules to S1 would make axiom M7 provable.

Semisubstitutivity of strict implication in S2

Closely related to Becker's rules and also a characteristic feature of S2 is the version of semisubstitutivity of strict implication (SSS) holding in this system. We recall that if the weakest version of SSS is assumed to hold in S1, it makes derivable our axiom M7, the proper axiom of S2. We shall now show that a version of SSS does hold in S2.

*6.7 Let the wff j be like the wff y except for having an accurrence of the wf subformula b where j has a, and let ab. Then:
  if a is in C-pos in j, then jy;
  if a is in A-pos in j, then yj.

Definition of A- and C-pos for modal contexts is as in Chapter 5. The reader may satisfy himself that *6.7 is actually equivalent to the 'weak' SSS discussed with relation to S1 in Chapter 5.

Proof, as with SSI, is by induction on the number of primitive operators (total of K's, N's, and M's) belonging to j and into whose scope a falls. The base step is trivial, with ab the same formula as jy. At the induction step, j will be of one of the forms Kgd, Kdg, Ng, or Mg, with a a subformula of g. Suppose now that h is like g except for containing an occurrence of b where g has a; then, by the induction hypothesis, if a is in C-pos in g, gh, and if a is in A-pos in g, hg. Now, we have as an S1 thesis (5.17) pqΝqΝρ, and we have easily provable in S2 -- by *5.1 and *6.2 -- the formulas pqKprKqr and pqKrpKrq. With these three theses we easily complete the proof for the cases where j at the induction step begins with a PC connective. Where that 0 begins with an M, we make use of *6.1, Becker's rule for M. SSS as expressed in *6.7, then, is an S2 metatheorem; we shall see that a stronger SSS than *6.7 is provable for the system S3 (Zeman 1968c).

Some theorems of S2

In our discussion of S1 we noted that a certain number of formulas (located about 5.79 ff.) were provable in S1 as material -- but not strict -- implications or equivalences. In S2 these formulas become provable in strict form. We shall simply list a number of such theses; method of proof should be obvious, using, basically, *5.1 and *6.1 or *6.2.

6.12 LKpqLp  
6.13 LKpqLq
6.14 LKpqKLpLq
6.15 MApqAMpMq
6.16 MKpqKMpMq
6.17 ALpLqLApq
6.18 CMpLqpq

As a variant of 6.15 we have:

6.19 MCpqCLpMq  

And finally, 6.14 gives us the strict equivalence of a strict and a necessary material equivalence:

6.20 pqLEpq  

The system S2

S2 is the system which Lewis in SL feels to be probably the best of his systems to serve as a formalization of 'strict implication'. S2 is formed, of course, by adding axiom M6, pMp, to S2. We have previously noted that, like the theses of S1, M7 -- the proper axiom of S2 -- is verified by matrix t1, which -- falsifies M6. S2 thus contains S2 properly. t2, on the other hand, is a matrix which verifies the theses of S1., but falsifies M7; S2 is then also a proper extension of S1.

The important theses and rules of S2 are, essentially, those of S1 plus those of S2; not too many theses of note are provable in S2 which are not provable in one or the other of those subsystems of S2. We shall set out the proof of just one of these:

6.21 CppqCpp *5.1
6.22 ppqpp 6.21, *6.2, 5.43, SSE
6.23 KCppqppq *5.1

We note that the right occurrence of pp in the above is in an A-pos:

6.24 KCppqppqq 6.23, 6.22, SSS

Again, Cppq in 6.24 is in an A-pos

6.25 Kppqppqq 6.24, 5.91, SSS, 5.43, SSE
6.26 ppqq S(M5)(J(M4)(6.25))

We shall leave it to the reader to determine that 6.26 is verified neither by t1 nor by t2.

The systems T and T

It could be argued that the systems of the present section have no place here, since they were not presented in SL, or even by Lewis at all, and at least T was not originally presented as founded upon the original S1 or S1. Later on we shall study the original presentation of T, but we shall set these systems down here as based upon S1, for this discussion would not really be complete without them. We begin with some deductions in S1:

6.27 LLa Hyp
6.28 La 6.27, *5.2
6.29 qa (q not in a) D(5.69)(6.28)
6.30 Laa 6.29, q / La
6.31 LpCpLp *5.1
6.32 CLLppLp S(5.61)(6.31), 5.43, SSE
6.34 aLa D(6.32)(6.27)
6.35 aLa J(6.34)(6.30)

We thus have as a rule:

*6.8 In an extension of S1 (with the rules of inference of S1):
  if LLa, then aLa.

By *5.1, the material version of 5.61, and PC, we have

6.36 CLpCLqpq  
6.37 Lb Hyp.
6.38 ab 6.36, 6.28, 6.37
6.39 bLb 6.34, 6.38, SSE
6.40 LLb S(6.39)(6.37)

Another rule then, is

*6.9 In an extension of S1 (with the rules of inference of S1):
  if both LLa and Lb, then LLb.

We now prove the following:

*6.10 In the system S1 plus any axiom of form LLa, :
  if b, then either Lb, or b is of form Lg, or is a strict implication.

We note first of all that all the axioms of the system in question are, essentially, of form Lg or gd. Thus, for any proof in the system consisting of exactly one step, *6.10 holds. Assuming that it holds for all proofs of length k or fewer steps, we note that the (k + 1)th step of a proof may be the result of the application of

(a) substitution for variables or SSE,
  (b) adjunction,  
  (c) strict detachment.  

If case (a), the substitution or application of SSE was in a previous step j of the proof. By the induction hypothesis, either Lj is a thesis or j is of form Ly or is a strict implication. In either case, the same substitution or SSE may be made into j, resulting in a thesis beginning with L as required; if j is of form Lj or is a strict implication, the requirement of *6.10 is already met; otherwise, as we have noted, the induction hypothesis enables us to meet it.

If case (b), suppose that j is either one of the premisses of the adjunction; if j is not of form Ly or a strict implication, then by the induction hypothesis, Lj; if it is of form Ly or a strict implication, then by *6.9, LLy, which is Lj. With j and c as the two premises of the original adjunction, then, under any circumstances and by the above considerations and the S1 thesis CLpCLqLKpq, we may move to LKjc, which is what we need.

If case (c), the premises for b, the (k + 1)th step, are jb and j. By the induction hypothesis, either j is of form Ly or is a strict implication, or Lj is provable. In the latter case, apply pqCLpLq to jb and then to Lj to get the desired result, Lb as a thesis. If the former case, then by *6.9, LLy, which is Lj is also provable, so the same pair of applications again yields the desired result. But then *6.10 stands proved.

By *6.9 and *6.10 we may now move immediately to:

*6.11 In an extension of S1 (with the rules of S1), if LLa, then if b, then Lb.

For if b already begins with an L, then *6.11 is a special case of *6.9. If not, then by *6.10 Lb is provable.

It is thus the case that if any thesis beginning with two L's is added as an axiom to S1, a rule to infer La from any thesis a becomes provable. And this will be, essentially, the way that we shall form the system T (sometimes called K) from S1 -- simply by adding to S1 as an axiom some formula beginning with two L's. We cannot, of course, be completely arbitrary in our choice of a formula to use as this axiom; adding the wrong formula might give us a system which is more comprehensive than we desire. So let us specify that the axiom for T be of form LLa, where a is any thesis at all of S2. We then assert about the system T:

*6.12 In the system T, if a, then La.

Proof is immediate by *6.11. The following proof-step goes through in S1:

6.41 CMKpqMp S(5.64)(M2)
6.42 MKpqMp 6.41, *6.12, 5.43, SSE

Formula 6.42 is, of course, the proper axiom of S2, which system is then contained in T. That the containment is proper is shown by matrix t3, which is 'Group I' of SL; to form t3, add to the standard four-valued tables for K and N the following:

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

The reader may verify for himself that t3 validates all S2 theses; as is quite evident, however, no formula beginning with two L's can take a designated value in this matrix. The system T will be formed by adding axiom M6, pMp, to T. That T is a proper extension of  T is shown by matrix t1, which fails to validate axiom M6, but which will give designated values to all of T's theses.

Modalities in T and its included systems

It was asserted in chapter 5 that the systems we have been studying all have an infinite number of irreducible modalities which are nonequivalent. Now we shall offer a proof of this.

*6.13 T and all systems included in T have an infinite number of non-equivalent irreducible modalities.

Suppose first of all that a system included in T had only a finite number of such modalities; that system must then contain 'reduction theses' asserting the equivalences necessary to establish that finite number of non-equivalent modalities. But then T too must contain these theses, and so could possess no fewer such modalities than did its included system. Thus, if T has an infinite number of such modalities, so too must each of its subsystems, and the proof of *6.13 reduces to a proof for T (which proof is an adaptation of McKinsey 1940).

For the proof we present at this point, we make use of a matrix; let us call it t4. t4 differs from the other matrices we have been employing in being infinite and in having as its elements not integers, but sets of integers. To be precise, the elements of t4 are the sets of signed integers (all such sets), and the designated value is the universal set. Evaluation in the matrix goes as follows: if the wff a is assigned the set A as its value, and b is assigned the set B, then Kab is assigned A B as value. If a is assigned the set A as value, Na is assigned A, the complement of A, as value. Now, let pA be a set such that the signed integer x belongs to pA iff the immediate predecessor of x belongs to A. Then if a is assigned the set A as value, Ma is assigned the set A pA. We might then represent the possible assignments to, say axiom M2 (Kpqp, or NMKKpqNp) by the notation (A B A p(A B A)); this is easily recognized as the universal set, regardless of the identity of A and B. We leave it to the reader to determine that all axioms of T (including LLa) take the designated value in this matrix, and that the property of taking the designated value is inherent through the rules of inference. Thus every thesis of T will be validated by this matrix.

Let us now define the notation Mn recursively (the definition of Ln is analogous):

M0a = a

Mn+la = MMna.

It can readily be seen that Mnp and Mmp will take the same value for all assignments in t4 iff m = n. Thus no formula of form MmtpMnp can be a T thesis unless m = n. Each string of M's, then, is a modality non-equivalent to each string of M's of length different from it, and T (and so all T's subsystems) has an infinite number of non-equivalent modalities.

Now note that the number of 'truth values' in this matrix is > 0; thus, if we think of evaluation in t4 as an actual procedure of computing the value of the formula for each possible assignment of values to the formula's variables, there must always be value-assignments for which -- in principle -- the computation will never occur. Evaluation in this matrix must then be considered 'non-constructive', and so too, I fear, must we consider this proof of *6.13. But when we later develop a sequent-logic version of T, we shall provide an alternative proof of *6.13 which is indeed constructive.