Chapter 6: The Absolutely Strict Systems

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.

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

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.

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

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)

ΝqΝρ, and we have easily provable in S2° -- by *5.1 and *6.2 -- the formulas

KprKqr and

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

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

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

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

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.

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.33
6.34	aLa	D(6.32)(6.27)
6.35	aLa	J(6.34)(6.30)

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)

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.

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

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.

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.

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 Mⁿ recursively (the definition of Lⁿ is analogous):

It can readily be seen that Mⁿp and M^mp will take the same value for all assignments in t4 iff m = n. Thus no formula of form

M^mtpMⁿp 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 > À₀; 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.

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

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

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

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

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

6.

THE ABSOLUTELY STRICT SYSTEMS -- S2°, S2, T°, AND T