5.

THE ABSOLUTELY STRICT SYSTEMS -- S1° AND S1

Introduction

WE have till now been labouring at the groundwork of our study of modal systems -- propositional calculi, in both their 'pure' and their sequent-logic versions. We now turn to modal logic itself; in many ways our treatment will parallel that of the propositional calculi, especially in that we shall set down sequent-logic versions of many of the modal systems we shall study.

When logicians have gathered together over the years, they have always found things about which to argue: One of the most venerable of these disputes began long ago when a Megarian logician named Ρhilο disagreed with his mentor Diodorus; the point on which they were at odds has generated argument-at least intermittently-ever since. This disagreement centred around the nature of the conditional, with Ρhilο defending a truth-functional 'if-then' -- the material implication of the modem classical propositional calculus -- and Diodorus in favour of a modalίzed conditional. Diodorus claimed, in effect, that there is an element of necessity expressed by an implication, that a conditional ought not to be considered true merely because its antecedent happened to avoid being true at the same time its consequent was false.

In our times, the debate over the nature of the conditional has helped to inspire the bringing forth of whole families of logical systems. One of the most interesting and formally fruitful of these families is that fathered by C. Ι. Lewis. Lewis felt, like Diodorus, that the connective we write as C does not reflect the true nature of the conditional, of implication. He set down systems including an operator which he called 'strict implication'; strict implication was to express more accurately than material implication the nature of the 'if-then'. But it is not our intention here to investigate the philosophical merits of Lewis's efforts. Our prime purpose is the study of modal systems in their formal aspects, and here there is

no question that Lewis has succeeded; his systems form the basis of what has been an extremely active area of research in today's world of logic.

The basic source for much of our present investigation is Lewis and Langford's Symbol Logic (1932), which we shall refer to as 'SL'; we shall also make some use of Lewis's Survey of Symbolic Logic (1918), in which he published his early work on the 'system of strict implication'.

The systems of SL are systems with conjunction and negation primitive, but since they are modal systems, we need some way of 'getting modality into' their formulas. Thus, these systems also have possibility as a primitive operator; the symbol we shall use as the sign of possibility is Μ. Μ is a unary operator forming wffs just as Ν does. As we shall see later on, other modal operators than Μ may be taken as primitive.

Lewis in SL defines material implication, equivalence, and alternation in terms of Κ and Ν just as we did at the end of the second chapter. In addition, he defines the modal connectives 'strict implication' and 'strict equivalence' in terms of Κ, Ν, and Μ. His notation is infixive, with the 'gaffing hook' ' being to strict implication what the horseshoe 'É' is to material implication, and with '=' as the sign of strict equivalence (for possibility he uses the sign 'à', with àa being read 'possibly a'). We shall use ( as the sign of strict implication, and for strict equivalence. These connectives are defined as follows

ab is defined as ΝΜΚaΝb

ab is defined as Kabba

Τo assert that a strictly implies b, then, is to assert the impossibility of the conjunction of a and Nb, and strict equivalence is formed from strict implication just as the ordinary material equivalence of the system PC is formed from material implication. Another key symbol of modal systems may be defined in terms of Μ and Ν; this is the sign of necessity, L:

La is defined as ΝΜΝa

Lewis himself does not define a sign of necessity; others who have employed the infixive notation of Lewis in their work, however, have used a to mean 'necessarily a' (this is defined, of course, as ~à~a).

Lewis shows some confusion in his references to the sign of strict equivalence; at one point he refers to it as if it were a primitive sign of his systems -- and then he goes on to define it. This seemingly inconsistent approach might be rationalized by holding that Lewis's sign '=' is indeed primitive, and all the definitions of SL are really to be considered axioms. But this is probably not Lewis's intent; what he has done, it seems, is to confuse two 'equivalence notions' and apply the same symbol -- = -- to both of them. When used as a defined symbol, '=' in SL is a sign of the object language -- of the system of strict implication itself. When used in the 'undefined' sense (Lewis uses it in this sense as a connective between definίens and definiendum in definitions), this symbol is in the metalanguage, and properly speaking, the notions of 'defined' and 'primitive' apply to it no more than they do to any term in mathematical English.

We are now ready to enter into detailed study of the various systems belonging to Lewis's family of modal logics. We begin our study with a subfamily called the 'absolutely strict' systems, and specifically, with a pair of systems -- called S1° and S1-- which form a basis for all the systems of SL.

It is possible to classify the Lewis modal systems in a number of ways; certain of these systems contain, for example, a rule of inference which permits the assertion to the theoremhood of the formula La whenever a itself is a theorem, while in others of these systems, this rule exists only in a restricted form, and La will often not be a theorem although a is. The form that this rule takes thus might be used as a criterion of classification for these modal systems. The basic system of classification we shall use, however, will be somewhat different. The instrument of classification here employed will be something called the modality. Basically, a modality is any formula of our systems; each such formula, qua modality, will be considered to be of form Χa, where Χ is considered to represent a string, possibly empty, of the operators L, Μ, and Ν, and a begins with none of those operators. The term modality will also be applied to the string Χ itself. If Χ contains an odd number of N's, the modality will be called 'negative'; otherwise, it is a 'positive' modality. We shall say that a modality Χ is equivalent to a modality Υ (in a given system) iff the formula ΧpΥp is a thesis (of that system). If this equivalence does not hold, we shall say that Χ and Υ are nonequivalent modalities. The most obvious and trivial example of equivalent modalities occurs when Χ and Υ are identical; our definition of L on the previous page provides us with another simple example of equivalent modalities: with that definition, LpNMNp will be a thesis of our systems, and so L and ΝΜΝ will be equivalent modalities.

Now, if a modality Υ is equivalent to a shorter (in number of N's, M's, and L's) modality Χ, then Υ is said to reduce to Χ; if there is no shorter (than Χ) modality Ζ to which Χ is reducible, then we say that Χ is irreducible. It is possible to have equivalent irreducible modalities. For example, it will turn out that the modalities NM and LN are equivalent, but are both irreducible in our systems. But the prime question here is that of the non-equivalent irreducible modalities in a system. If we think of the classical PC as a modal system, it is easy to see that there are in that system (since L and Μ do not occur there) precisely two non-equivalent irreducible modalities, which may be represented by the formulas a and Νa. It is also easy to see that IC, under the same consideration, has three nonequivalent irreducible modalities, represented by a, Νa, and ΝΝa. So these systems have a finite number of non-equivalent irreducible modalities (we shall refer to non-equivalent irreducible modalities simply as non-equivalent modalities when there is no danger of confusion).

What is the case with the modal systems we are beginning to study? Do they, like PC and IC, have only a finite number of non-equivalent modalities? As might be expected, the answer is that some do and some do not, and the possession or non-possession by a system of an infinite number of non-equivalent modalities will be a criterion for the classification of that system. In brief, the systems which have an infinite number of non-equivalent irreducible modalities will generally be called 'absolutely strict systems, while systems containing only a finite number of non-equivalent modalities will, in general, be called 'systems of complete modalization' (we note here, however, that there are a few systems which have infinitely many non-equivalent modalities, but which we shall study along with the systems of complete modalization rather than with the absolutely strict systems; this is because the systems in question are structurally related much more closely to certain systems with finite numbers of non-equivalent modalities than to any of the systems we are calling absolutely strict). The notion of complete modalization is, roughly, that a formula is completely modalized if the prefixing of modal operators to it does not change its 'modal quality', provided the preying does not change it from a positive to a negative modality, or vice versa. Thus, if a is completely modalized, and Χ is a string of L, Μ, and Ν with an even number of N's or no N's, then Χa will be equivalent to a (and if Χ contains an odd number of N's, Χa is equivalent to Νa).

The systems we shall be studying in the next few chapters are calculi in which the notion of complete modalization is lacking, the absolutely strict systems. As has been mentioned, Lewis in SL puts forth the bases of a number of modal systems; the one he suggests is the best to serve as a formalization of the concept of strict implication is the one commonly referred to as S2. If a certain one of Lewis's axioms for this system is omitted, the result is a system called S1, which is a proper subsystem of S2. Various proper extensions of S2 may be set up by subjoining to the axiom set for S2 appropriate new axioms; among the more important of these systems are those called S3, S4, and S5. These three, unlike S1 and S2, are systems of complete modalization and will be studied later in this book. Besides S1 and S2 there are a number of other absolutely strict systems we shall study. One of these is a proper extension of S2 called Τ; the others are proper subsystems of each of S1, S2, and Τ, and will be called S1°, S2°, and Τ° respectively (Feys 1950, Sobocinski 1962, Thomas 1964). We begin our detailed study with an examination of the system S1°.

The system S1°

As has been indicated, the system S1 is the basic system of SL; other systems are formed there by subjoining further axioms to S1. One of the commonly used axioms for S1 is the formula pΜp, which asserts that any statement strictly implies its own possibility. As will be seen, this formula is independent of the other axioms of S1, which means that the system formed by its omission from this set is a proper subsystem of S1. This proper subsystem is S1° (this may be read 'S1-nought') and was first studied in Feys 1950. S1° will serve as our basic system; most of the other calculi we study will be formed by the subjunction to S1° of one or more additional axioms. As first we study it, S1° will be considered to employ the primitive operators of SL, which are K, Ν, and Μ. The definition of C, Α, and Ε will be just as in a conjunction-negation primitive prepositional calculus, and the modal operators L, , and are defined as in the previous section. We postulate for S1° four rules of inference:

M1. KpqKqp

Μ2. Kpqp

Μ3. KKpqrKpKqr

Μ4. pΚpp

Μ5. Kpqqrpr.

Lewis includes in his axiom set the formula pΝΝp; as we shall see, this is derivable from the five listed above (McKinsey 1934). Since Lewis works with the system S1 rather than S1°, his axiom set includes another formula (deductively equivalent to pMp); actually, he offers a choice of two axioms; either his

which is originally from the axiom set in Lewis 1918, or his

Β7. Kppqq

will do the same job as will pMp. None of these last-discussed axioms, of course, is part of S1°. Lewis 1918 offers another slight variation on the set of axioms from which we have drawn Μ1-Μ5; in place of our Μ3, this formulation has

Μ3'. KpKqrKqKpr

We now begin deductions in the system S1°; first we note that Μ1, Μ3, and Μ4 may be made into strict equivalences:

5.1	pKpp	J(Μ4)(Μ2) q / p, Df.
5.2	KpqKqp	D(2.1)(C2)
5.3	KrKqpKKrqp	Μ3, 5.2, SSE
5.4	KKpqrKpKqr	J(Μ3)(5.3 p / r, r / p) Df.

Next, the 'law of identity'

5.5	pp	S(Μ5)(J(Μ4)(Μ2))
5.6	pp	J(5.5)(5.5), Df.

Now, some deductions involving negation:

5.7	NpqNMKNpNq	5.5 p / NMKNpNq,  Df.
5.8	NpqNqp	5.7, 5.2, SSE, Df.
5.9	NNpp	S(5.8)(5.5)
5.10	NNNNpp	S(Μ5)(J(5.9)(5.9))
5.11	NpNNNp	S(5.8)(5. 10)
5.12	ΝΜΚρΝρ	5.5, Df.
5.13	NpNNNp	S(5.11)(5.9 p / Νp), Df.
5.14	pNNp (i.e. ΝΜΚpΝΝΝp)	5.12, 5.13, SSE, Df.
5.15	pNNp	J(5.14)(5.9), Df.

As we promised earlier, with 5.14 we have shown' the redundancy of Lewis's axiom pΝΝp.

5.16	NNpqΝqΝρ	5.8, p / Νp
5.17	pqΝqΝρ	5.16, 5.15, SSE

In S1° we cannot show that the formula pqr is equivalent to Kpqr; we can, however, prove a weaker version of 'importation-exportation':

5.18	pCqrNMKpNNKqNr	5.6 p / pCqr, Df. , C
5.19	pCqrNMKpKqNr	5.18, 5.15, SSE
5.20	pCqrNMKKpqNr	5.19, 5.4, SSE
5.21	pCqrKpqr	5.20, Df.

5.21 is, of course, the promised importation-exportation formula. Let us now prove a thesis which is an analogue of comm in IC and PC.

5.22	pCqrKpqr	S(Μ2)(5.21)
5.23	pCqrKqpr	5.22, 5.21, SSE
5.24	pCqrqCpr	5.23, 5.21, SSE

Note that not all the implications within 5.24 are strict. We may now show that material detachment is a derived rule of inference in Sl°:

5.25	pCCpqq	S(5.24)(5.5)
5.26	ab	Hyp
5.27	a	Hyp
5.28	KpCpqq	S(5.22)(5.25)
5.29	b	S(5.28)(J(5.27)(5.26))

The provability of 5.29 from the hypotheses 5.26 and 5.27 establishes material detachment as a derived rule here. If we employ material detachment, we shall make use of the D-notation just as in Chapter 2.

5.30	rCqKqr	Μ1, 5.21, SSE
5.31	KrpCqKqr	S(Μ5)(J(Μ2)(5.30))
5.32	qCKrpKqr	S(5.24)(5.31)
5.33	CKpCpqCKrpKqr	S(Μ5)(J(5.28)(5.32))
5.34	pCCpqCKrpKqr	S(Μ5)(J(5.22)(5.33))
5.35	Krpp	S(Μ5)(J(Μ1)(Μ2))
5.36	KrpCCpqCKrpKqr	S(Μ5)(J(5.35)(5.34))
5.37	CpqCKrpCKrpKqr	S(5.24)(5.36)
5.38	CpqCKKrpKrpKqr	S(Μ5)(J(5.37)(5.22))
5.39	CpqCKrpKqr	5.38, 5.1, SSE
5.40	CpqCNKqrNKrp	S(Μ5)(J(5.39)(5.17))

Formula 5.40 will be recognized as a 'strict implication version' of axiom ΚΝ3 of Chapter 2, that is, it is the same as the third axiom of Rosser 1953 for the propositional calculus in Κ-Ν primitive; its first character, however, is a strict rather than a material implication.

Also observe that axiom Μ4 of S1° is a strict implication version of Rosser's axiom ΚΝ1, and Μ2 is a strict implication version of his ΚΝ2. Strict implication versions of all of Rosser's axioms for PC in Κ-Ν primitive, then, are S1° theses.

We shall now enter into some deductions involving L, the defined sign of necessity.

5.41	pqNMKpNq	5.6 p / pq, Df.
5.42	pqNMNNKpNq	5.41, 5.15, SSE
5.43	pqLCpq	5.42, Df. L, C

Α strict implication, then, is equivalent to a necessary material implication.

5.44	pNpp	Μ2, 5.21, SSE, q / Νp
5.45	NKppNp	S(5.17)(Μ4)
5.46	CNppp	S(Μ5)(J(5.45)(5.9)), Df. C
5.47	pCNpp	J(5.44)(5.46), Df.
5.48	LpLp	5.6 p / Lp
5.49	LpLCNpp	5.48, 5.47, SSE
5.50	LpNpp	5.49, 5.43, SSE

This last thesis relates the necessity of a simple statement of Sl° to a strict implication.

5.51	MpNNMNNp	5.6 p / Mp 5.15, SSE
5.52	MpNLNp	5.51, Df. L

Formula 5.51 gives Μ in terms of L.

5.53	prCrsps	Μ5, 2.21, SSE
5.54	KpqqrCrsps	S(Μ5)(J(Μ5)(5.53))
5.55	KNqNpNppCpqNqq	5.54 p / Nq, q / Νp. r / p, s / q
5.56	NqNpCNppCpqNqq	5.55, 5.21, SSE
5.57	pqCNppCpqNqq	S(Μ5)(J(5.17)(5.56))
5.58	pqCLpCpqLq	5.57, 5.50, SSE
5.59	LpCKpqpqLq	S(Μ5)(J(S(5.24)(5.58))(5.22))
5.60	LpCpqLq	5.59, 5.1, SSE
5.61	pqCLpLq	S(5.24)(5.60)
5.62	LCpqCLpLq	5.61, 5.43, SSE

Formulas 5.61 and 5.62 are two versions of the very important law of distribution of L over material implication.

5.63	pqCNLqNLp	S(Μ5)(J(5.62)(5.17))
5.64	pqCMpMq	S(Μ5)(J(5.17)(5.63))
5.65	pqCNMqNMp	S(Μ5)(J(5.64)(5.17))
5.66	pqCMNqMNp	5.63 p / NNp q / NNq, 5.15, 5.52, SSE

Formulas 5.63-5.66 are various modal distribution-tranposition formulas related to 5.61 and 5.62.

The classical PC in S1°

We are now prepared to prove a number of important metatheorems of the system S1°. First among these is the following:

We assume for the PC Rosser's Κ-Ν primitive basis; each PC theorem a is then provable from this base in a certain number of proof steps, say n such steps. If n = 1, a can only be one of the axioms CpKpp, CKpqp, or CCpqCNKqrNKrp. But formulas Μ4, Μ2, and 5.40 are exactly like these axioms respectively except for having rather than C as main connective. By the equivalence of and LC, then, when a is an axiom of Rosser's formulation of PC --and so when n = 1 -- La is a thesis of S1°.

Suppose now that whenever n £ k and a (provable in n steps) is a thesis of Rosser's formulation of PC, then also La is a thesis of S1°. Consider the case in which n = k + 1; there are here two possibilities:

(1)

a resulted from a substitution in a formula b, b being a previous step in the proof of a. Since b then is provable in k or fewer steps, by the induction hypothesis Lb is a thesis of S1°. But then La is also an S1° theorem, by the same substitution in Lb as that which transformed b to a in PC.

(2)

a resulted from a detachment involving two previous proof steps, b and Cba. Since both these formulas are provable in k or fewer steps, Lb and LCba are both theses of S1° by the induction hypothesis. But then applying formula 5.62 (LCpqCLpLq) to the latter of these formulas (using strict detachment) gives CLbLa as an S1° thesis, and applying this formula to Lb (with the derived rule of material detachment) gives us La as an S1° thesis.

The metatheorem therefore holds.

We begin our proof by setting up the hypothesis:

5.67	La	Hyp.
5.68	pCqp	5.21, Μ2, SSE
5.69	CLpqp	S(5.61)(5.68), 5.43, SSE
5.70	qa	D(5.69)(5.67)
5.71	a	S(5.70)(Μ1)

Of course, the variable q in 5.68-5.70 must be chosen in such a fashion as to be distinct from all the variables of a. Thus, beginning with the assumption of La as a theorem, we are able to derive a, and *5.2 holds.

We now move easily to yet another metatheorem:

From this point on, we shall justify the inclusion of a PC theorem or the use of a PC operation in a proof simply by the notation 'PC'; the use of a thesis La where a is a PC thesis will be justified by reference to *5.1.

Further theses and rules of S1°

Formulas 5.61-5.66 gave us some modal distributional and transpositional theses related to pqCLpLq; we now engage in the proof of more such theorems

5.72	CLKpqLp	S(5.61)(Μ2)
5.73	CLKpqLq	S(5.61)(5.35)
5.74	CLKpqKLpLq	5.72, 5.73, PC
5.75	pCqKpq	*5.1
5.76	CLpqKpq	S(5.61)(5.75), 5.43, SSE
5.77	CpqCLpLq	5.61, *5.2
5.78	CLpCLqLKpq	5.76, 5.77, PC
5.79	CKLpLqLKpq	5.78, PC
5.80	ELKpqKLpLq	5.74, 5.79, PC

It will be noted that 5.80 is a material equivalence and 5.74 and 5.79 are material implications. The corresponding strict formulas are not provable in S1°; this is, in fact, a feature which distinguishes S1° from its proper extension S2°; many theses which are strict implications in the latter system are only material in the former. Easily provable from 5.80, now, is

Details are left to the reader, as they are for the proof of

and

That modality behaves somewhat as does quantification is quite evident, by the way, from the last four theses, with necessity analogous to universal and possibility analogous to existential quantification. The proof of another thesis emphasizing the resemblance follows:

5.84	CNKMpMNqNMKpNq
5.85	CNKMpNNMNqpq
5.86	CCMpLqpq

In conjunction with *5.2 and 5.43, 5.86 yields the following rule:

*5.4	If MaLb, then ab.

This last metatheorem will figure later in the extension of S1° to S5. As a final distributional item of S1°, we prove the rule:

*5.5	If both ab and ba, then LaLb.

Start with

5.87

ab.

Hyp.

In the field of Sl°, this last is equivalent to the premiss of *5.5.

5.88	LaLa	5.6, p / La
5.89	LaLb	5.88, 5.87, SSE
5.90	LaLb	5.89, PC

The semisubstitutivity of strict implication and S1°

In Chapter 2 we stated and proved the principle of semisubstitutivity of implication (SSI) for the systems IC and PC. SSI is, in effect, an analysed version of substitutivity of the biconditional (SBC). One of the rules of inference of S1° is substitutivity of strict equivalence (SSE), which is a modal kind of SBC; this raises the question of whether there is a modal SSI which will stand to SSE as SSI itself stands to SBC; we might call the proposed rule the 'semisubstitutivity of strict implication', or SSS.

Before we can determine whether or not Sl° has an SSS rule, we must extend the notions of Α-pos and C-pos to include modal as well as non-modal contexts; this can be done for the present systems simply by adding to our previously stated rules the following (we continue the numbering begun in Chapter 2)

We shall consider as a possible S1° metatheorem the following weak version of SSS:

If a is a subformula of an S1° thesis b, then if a is in C-pos in b, it may be replaced without loss of theoremhood by any formula which it strictly implies, while if a is in A-pos in b, it may be replaced by any formula strictly implying it.

This proposed rule is an analysed version of the principle of SSE which is a rule of inference for S1°, and so it seems reasonable that it be an S1° metatheorem. However, by p / Μp in 5.5 we have MpMp and as axiom Μ2 we have Kpqp. The first p in ΜpΜp is in Α-pos, and so if SSE held here, by axiom Μ2 we should be able to replace that p with Kpq, yielding MKpqMp. But this formula is not an S1° thesis; as we shall see, it is, in fact, the proper axiom of S2°, a proper extension of S1°. Thus S1°, although it contains SSE, cannot contain SSS. We shall see, however, that S2° does contain a version of SSS, and that S3° contains an even stronger one.

The system S1; truth-value systems

Although many of the important theorems of S1 are provable in S1°, a number of theses relating modal statements to other modal statements and to non-modal statements are not provable therein. We earlier noted that pMp -- a formula which we should probably expect to hold in a modal logic -- does not hold in S1°. That it is indeed independent of S1° may be shown in a variety of ways; one method that immediately comes to mind would be to develop a sequent-logic equivalent to S1° and providing a decision procedure for S1° as LPC and LIC do for PC and IC, and use the sequent-logic to 'decide' ρΜρ for S1°. We shall indeed develop such a sequent-logic later on, but for now we shall discuss and employ a different method, one quite standardly used in establishing the independence of axiom systems. What we refer to may be called the matrix method. For some η, we find an n-valued 'truth-value system' which verifies all the theses of S1°, in this case, but which fails to verify, say, ρΜρ  Such a truth-value system, or matrix, may be thought of as a set of tables, one for each of the primitive operators of the system, which may be used in computing a 'truth table' for any wff of the system. Matrices for independence proofs for axiomatizations of, say, the ordinary propositional calculus are often wildly strange in appearance; we shall find that on the contrary, the matrices commonly employed with the Lewis-modal systems fall into a very nice pattern.

First of all, the number m of values employed will almost always be such that m = 2n for some natural number n. Secondly, the tables for the PC will always be the same, regardless of the modal system in which we are working; differences between systems will be reflected only in differences between tables for modal operators. Also, tables for the PC connectives are so designed as to be direct extensions of the standard two-valued PC truth tables. As it turns out, the PC is complete with respect to each of the matrices for non-modal operators which we shall use, whether the number of values in that matrix is 2, 4, 8, 16, 32,. ...

Let us go on to describe the general method of setting up the PC connective matrix tables for the Lewis-modal systems. The simplest way of doing so is to think of our truth values -- initially, anyway -- as being expressed in binary notation. When the truth values are thus expressed, we consider the lowest numbered value as the 'falsest', and the highest as the 'truest.' Since the number of truth values will be 2ⁿ for some integral n, we shall always be able to express all and only the m truth values by using exactly n binary digits (bits). Thus if n = 1, we have the ordinary two-valued system, with 0 and 1 as binary notation truth values. If n = 2, we have all the truth values we can express in two bits per number, or four; these are 00, 0 l, 10, and 11. If n = 3, our system is eight-valued (eight being the total number of three-bit binary numbers) with values 000, 001, 010, 011, 100, 101, 110, and 111. In general, our truth-values for any such m-valued system will be the binary numbers from 0 to m - 1.

We may now easily determine the table for the operator N for any such m: for any truth value in binary, no matter how many bits it has, if a has that truth value, then determine the truth value of Na by changing each 1 in a's truth value to a 0 and each 0 to a l. We give the binary truth table for N in four values as an example:

It should be clear that for any number of truth values m, we can always form a table for N simply by counting backwards from m - 1 -- if our table for a begins with the lowest value, that for Na will begin with the highest, and then continue like an upside-down table for a.

Since the systems with which we are now working have K as well as N primitive, we shall describe a means of constructing a table for K; tables for all other PC connectives may then be defined in terms of those for N and K. In the repertoire of almost every digital computer is an instruction variously named by the computer manufacturers; the most descriptive name for it, for our purposes, is 'logical and'. The 'logical and' takes two binary numbers with an equal number of bits and uses them to construct a third, again with the same number of bits as each of the first two. It constructs the third number as follows: it compares the leftmost bit of the first number with that of the second; if both bits are 1's, it writes 1 as the leftmost bit of the third number. Otherwise, it writes a 0 (taking 1 as true and 0 as false, the reason for the name 'logical and' is obvious). It then does the same thing with the second bit of each of the first two numbers, using them to determine what the second bit of the third number will be. In general, the ith bit of the third number will be 1 only when the ith bits of both the first and the second are 1; otherwise it will be 0. We shall think of a 'logical and' instruction as computing our tables for K; for the two-valued system, of course, this gives us the standard two-valued table for K. The following table will show what it does for an eight-valued system. The values for the first argument of K -- p in Kpq -- are read down the leftmost column, and those for the second argument -- q -- are read across the topmost row. The value of Kpq when p takes the value x and q the value y is found at the intersection of row x and column y

Now, there is no question that a table all in binary is rather difficult to read, so we shall translate it into a different numbering system. Our method of computing the value of K takes the truest value to be the highest, whatever the number of truth values may be. In the literature, it is most common to do just the opposite and allow the truest value to be the number 1, and then number in the decimal notation up towards the falsest value, which will then be m in an m-valued system. If we so correlate the numbers in our table for K with the decimal numbers from 1 to 8, we shall get the following table (note that we have listed the binary equivalent of each decimal number next to that number in the leftmost column)

This table naturally divides itself into quadrants, one of which is marked off. This upper left quadrant is, in fact, the K table for four values (its upper left quadrant is, in turn, the table for two values). The table for N in eight values is, of course,

while that for N in four values is

Given the tables for K and N, we may construct tables for C, A, and E by means of the standard definitions of these connectives in terms of K and N in PC; the table for C is:

We shall leave it to the reader to construct tables for A and E. Again we have sectioned off the upper left quadrant of the C table; once again, this quadrant is the table for C in four values.

We are now ready to make a first use of the family of matrices we have been describing; this will be to show the independence of the formula pMp from S1°. We shall use a four-valued matrix; the tables for K and N are as above indicated, and the table for M is: 

 Since L is NMN, we may construct a table for L as well: 

The 'designated values' we shall take for this application are 1 and 2; a designated value is one which we think of as being 'true enough' for our immediate purposes. The reader may satisfy himself that all the axioms of S1° take only designated values in our matrix, and that the property of taking designated values only is hereditary through our rules of inference (this is much like the standard way of proving consistency for PC, except for the greater number of values). All theorems of S1°, then, take only designated values in our matrix. But let p in the formula LCpMp (clearly equivalent in this matrix to pMpp) take the value 1 (3 will also do); the formula then is LC1M1 = LC12 = L2 = 3; 3 is not a designated value, so pMp is not a theorem of S1°. Other formulas given in this section as specifically S1 theses may also be shown to take non-designated values in this matrix; checking this is left to the reader.

The matrix employed above is taken from SL [p. 494], where it is called 'Group IV'.

Some work within the system S1

As we have remarked, we formulate the system S 1 by adding to S1° the axiom

Μ6. pMp

We earlier noted that Lewis gives two ways of formulating this system; to whatever is the basis of the system S1° he adds either his axiom A7 -- NMpNp -- or axiom B7 -- Kppqq. It would immediately be clear that Sl° + M6 and S1° + A7 are equivalent systems. Let us then proceed as follows:

5.91	Lpp	S(M5)(J(A7)(5.9))
5.92	pqCpq	5.91 p / Cpq, 5.43, SSE
5.93	Kpqpq	S(5.21)(5.92)
5.94	Kppqq = B7	S(M5)(J(M1)(5.93))

Let us now assume the system S1° + B7; taking p / Np and q / p in B7 and employing axiom M1 we get:

5.95	KNppNpp
5.96	NppCNpp	5.95, 5.21, SSE
5.97	Lpp	5.96, 5.47, SSE, 5.50
5.98	NNpNLNp	S(5.17)(5.97)
5.99	pMp = M6	5.98, 5.15, 5.52, SSE

We thus have it that S1° plus A7, B7, or M6 are equivalent systems. Another typical S1 thesis is

5.100

LpMp

S(M5)(J (5.91)(M6))

Of course, all the above formulas as material rather than strict implications are also S1 theorems. We shall note that the following are derived rules in S1:

*5.6	If ab, then Lab.
*5.7	If ab, then aMb.

Proof is immediate by M5 and 5.91 or M6. Material versions of these rules also hold:

*5.8	If Cab, then CLab.
*5.9	If Cab, then CaMb.

Earlier we showed that 5.86, CCMpLqpq is an S1° thesis; variations of this theorem are provable in S1 (see Sobocinski 1963):

5.101	LCLpp	5.91, 5.43, SSE
5.102	CLpp	5.101, *5.2
5.103	CMpLqpq	5.86, *5.8, 5.43, 55E
5.104	CCMpLqCpq	5.86, 5.102, 5.43, PC
5.105	CMpLqCpq	5.104, *5.8, 5.43, SSE

Observe that the last three formulas may be proved in S1° + 5.102, a weaker system than S1.

5.106	C*5.1, 5.61, 5,43, SSEpqCqrCpr	*5.1, 5.61, 5,43, SSE
5.107	CqrCpqCpr	*5.1, 5.61, 5,43, SSE
5.108	CMpqCpq	D(5.106)(M6)
5.109	CpLqCpq	D(5.107)(5.91)
5.110	CMpLqCpq	S(M5)(J(5.108)(5.109))
5.111	MpLqCpq	5.110, *5.6, 5.43, SSE

The last two formulas are versions of 5.86 provable in S1 proper. It should be clear that S1° plus either of 5.108 or 5.109 gives S1; but even the system S1° + 5.110 = S1. Assume for the moment this last mentioned system:

5.112	LqCMpLq	*5.1
5.113	LqCpq	S(M5)(J(5.112)(5.110))
5.114	LqCNqq	5.113, p / Nq
5.115	Lqq	5.114, 5.47, SSE