Ma is defined as NLNa
ab is defined as
LCab;
WE have been investigating the systems S1° through T in what is essentially the form in which Lewis presented them (with the exception, of course, of T° and T). But this is not the only way to formulate these systems, nor is it the simplest. Other systems of primitive connectives than K-N-M might be used; most simply, K and N might be replaced by any functionally complete system of connectives for PC, and M might be replaced by L. And yet other connectives might be employed. Instead of L or M, a sign of impossibility or of lack of necessity might be used; in the original formulation of strict implication of Lewis 1918, impossibility was the primitive modal operator. As we shall see, in fact, impossibility along with just material implication provides a complete set of connectives for some of the Lewis-modal systems.
The common base for the systems as we have till now studied them is the system S1°. But S1° itself contains the PC. Is it not possible that the PC itself rather than S1° might be taken as the base for these calculi? It is indeed possible, and as it turns out, perhaps even preferable to do so. As we shall see, formulations of these systems based upon the classical PC are more elegant and economical than those we have seen up to now, and they also permit these logics to be treated as 'tiered' systems, with all the theorems not containing modal symbols provable from the non-modal axioms. Simplifications in the postulated rules of inference for these systems are also made possible.
We shall assume for our present purposes that our primitive operators are implication, negation, and necessity, C, N, and L. The other operators of PC will be defined as usual, and we shall have in addition the following:
Ma is defined as NLNa
the definition of 
will be as
before. Formulations of S1°-T° as based upon the PC are found in
Zeman 1968b and
Thomas 1964. We shall present S1° as given in the former and
T° as in both of
these; the present formulation of S2° differs somewhat from that given in these
papers. Some complete system of axioms for PC in C and N is assumed as base for
all these systems; in addition, each of them will contain the following
postulated rule of inference (beyond the rules proper to PC):
| RLE: | If
 La,
then
a. |
Other rules of inference for the various systems will be drawn from the following stock:
| RL: | If
a,
then
La. |
| RL1: | If
a,
then
La,
provided either |
| (a) a is a PC thesis, or | |
| (b) a is
of form CKLbLgd
where LAbg, or |
|
| (c) a is of form CLbb; this clause applies to S1 only. | |
| RL2: | If a is a PC
theorem or a theorem of form CLbg, then
La. |
| BKW: | If both
LCab
and LCba,
then LCLaLb. |
It will be noted that BKW is a weakened version of one of Becker's rules. Each of the systems will include the PC, rule RLE, and one or more of the other rules listed above. In addition, each system will have one axiom besides those of the PC. The following table summarizes the way modal axioms and rules (other than RLE) are employed in these systems; axioms are listed down the left, and rules across the top of the table. A system listed on this table will contain the axiom of the row in which it is listed, and each of the rules in whose column it is listed.
| Rules Employed | |||||
| Axioms | BKW | RL1 | RL2 | RL | |
| L1. | CKLCpqLCqrLCpr | S1° | S1° | ||
| L2. | CLCpqCLpLq | S2° | T° | ||
S2° as formulated in Zeman 1968b and
Thomas 1964 consists of the PC, RLE, axiom
L2, and rule RL1 above, and, in addition, one of Becker's rules,
'If LCab,
then LCLaLb.'
(We shall sometimes refer to this rule as 'BKR'.) The present
formulation of S2° has the advantage of having only one postulated modal rule of inference aside
from RLE.
That the systems as above formulated are included in their respective Lewis-modal systems as defined in Chapters 5 and 6 may be immediately established. S1° as studied in the previous chapters contains the PC by *5.3, as do all the systems founded upon S1°. All these systems also contain RLE, by *5.2. That rule RL2 holds in S2° and that RL1 holds in S1° and S1 are points that we shall not establish at this time. Their proof will be delayed until the next chapter, in which we shall discuss sequent-logics corresponding to the absolutely strict Lewis modal systems; the sequent-logics for S2° and S1° make the proof of these rules extremely simple. The rule BKW holds in the original S1° by *5.5. The formulations of S1° and S2° here proposed, then, are included in the respective versions of those systems of Chapters 5 and 6.
Since T° as originally discussed is founded on S1°, it contains the basis of the present chapter's T° with the exception of rule RL; this rule, however, is contained in Chapter 6's T° by *6.12. This chapter's T°, then, is contained in that of Chapter 6.
We now assume the present chapter's version of S1°. By PC and RLR, axioms
M1-M4
of Chapter 5 are theorems in this chapter; clearly too, the rule of adjunction
is here derivable by PC methods alone. The rule of strict detachment follows
here too; RLE permits us to move from any thesis
ab to the simple
Cab, at
which point material detachment may be employed, giving strict detachment as a
derived rule. By axiom L1 and RLR, we have axiom M5 of Chapter 5 as a thesis of
the present chapter. Since substitution for variables is common to both systems,
we need only show now that substitutivity of strict equivalence holds in the
present S1°. By PC and RLR we have:
| 7.1 |
CNppNp |
Applying BKW to 7.1 (since this rule is, equivalently, 'If
ab,
then
LaLb'):
| 7.2 |
NppLp |
|
| 7.3 |
ENppLp |
7.2, PC, RLE |
| 7.4 |
CpqCqrCrsps |
L1, PC |
| 7.5 |
CNqNpCNppCpqNqq |
7.4, p / Nq, q / Np, r / p, s / q |
| 7.6 |
CpqCLpLq |
7.5, 7.3, PC |
| 7.7 |
CpqCqrCpr |
PC, RL1, 7.6 |
| 7.8 |
CqrCpqCpr |
PC, RL1, 7.6 |
We now set up as a hypothesis
| 7.9 |
ab |
Hyp. |
| 7.10 |
ab |
7.9, PC |
| 7.11 |
ba |
7.9, PC |
| 7.12 |
CagCbg |
D(7.7)(7.11), r / g |
| 7.13 |
CbgCag |
D(7.7)(7.10), r / g |
| 7.14 |
CgaCgb |
D(7.8)(7.10), p / g |
| 7.15 |
CgbCga |
D(7.8)(7.11), p / g |
| 7.16 |
CagCbg |
7.12, 7.13, PC |
| 7.17 |
CgaCgb |
7.14, 7.15, PC |
We now turn our attention to the negation sign:
| 7.18 |
CpqNqNp |
PC, RL1, BKW, RLE |
| 7.10 |
NaNb |
D(7.18)(7.11) |
| 7.20 |
NbNa |
D(7.18)(7.10) |
| 7.21 |
NaNb |
7.19, 7.20, PC |
Thus we may, in the present version of S1°, move from the hypothesis 7.9 to
formulas 7.16, 7.17, and 7.21; by BKW, we may move from 7.9
to LaLb. But these
are the operations necessary to complete the induction step of the proof of SSE
in a C-N-L primitive system. We leave details to the reader, and shall now
assert that SSE is a derived rule in this chapter's S1°. Thus is the
S1° of
Chapter 5 contained in the present version, and we have:
| *7.1 | The PC based formulation of S1° of Chapter 7 is equivalent to the original S1°. |
Let us now assume the system S2° as given in this chapter.
| 7.22 |
CpqCCqrCpr |
PC, RLR |
| 7.23 |
CpqCqrCpr |
7.22, L2, PC |
| 7.24 |
CpqCqrpr |
7.23, L2, PC |
| 7.25 |
pqCqrpr |
7.24, RL2 |
| 7.26 |
pCqrCKpqr |
PC, RL2, L2 |
| 7.27 |
Kpqqrpr |
D(7.26)(7.25) |
This last formula is the strict implication version of axiom L1, which axiom is also a thesis of this S2° by RLE; RLR in its S1° version (as applying to L1) is thus seen to hold in S2°. Now note that Becker's rules hold in the present S2°; for instance:
| 7.28 |
ab |
Hyp. |
| 7.29 |
CLaLb |
D(L2)(7.28) |
| 7.30 |
LaLb |
7.29, RL2 |
It is clear that the rule BKW will also hold in this system, then, and so we
have Sl° contained in this chapter's S2°. And since Becker's rules hold in this
system, the proper axiom of S2° as presented in Chapter 6,
MKpqMp, will
clearly be provable. The present system then contains the original S2°, and we
may say:
| *7.2 | The present S2° is equivalent to the original. |
System T° in this formulation presents no problem whatsoever; BKR is easily derived in it by axiom L2 and the unrestricted rule RL and so S2° and therefore S1° are contained therein. RL permits the derivation of a thesis beginning with two L's, meaning that the system contains T° as originally formulated:
| *7.3 | The present T° is equivalent to T° as originally presented. |
We now turn to
the question of the full systems S1-T. As might be expected, these systems
result when the rule RLE is replaced by an axiom corresponding to the
pMp of
the previous chapters; the formula we shall employ is
L3. CLpp
Implicit in the use of this axiom to form S1, of course, is the extension of
rule RLR to include application to it, making
Lpp a thesis of this system. It
should be evident that:
| *7.4 | The systems formulated by replacing RLE in the S1°, S2°, and T° of this chapter by axiom L3 are equivalent, respectively, to S1, S2, and T. |
The formulation of S1 referred to is essentially that of Lemmon 1957; the system T is as originally formulated in Feys 1950 (we note that the base here given for T is included in the formulations of the systems S4 and S5 of Gödel 1933). Our formulation of S1 differs from that .of Lemmon in having rule BKW where Lemmon has substitutivity of strict equivalence (see Zeman 1968b, Thomas 1968). If rule RL2 in our S2 is replaced by rule RLl and the rule to infer LCLaLb from LCab, we have the S2 of Lemmon 1957.
We shall note a couple of other formulations of the system T, leaving it to the reader to establish their equivalence to T. In von Wright 1951 a number of modal systems based on PC are set down; one of them is the system there called M, which is equivalent to T. In addition to PC, this system has our rule RL, and another rule resembling our BKW
| BKX: | If
Eab,
then
ELaLb. |
Axioms employed for M are:
vW1. CpMp
vW2. EMApqAMpMq
This system has M as its primitive modal operator, with L defined as NMN.
We commented earlier that Lewis 1918 used impossibility as a primitive operator. As the final formulation of this chapter, we shall set down a version of T which uses impossibility as primitive; the only other primitive connective employed is the ordinary material implication sign, C (Zeman 1968a). The symbol R will be the sign of impossibility and will form wffs as does N. Definitions in the system are
Na is defined as CaRa
La is defined as RCaRa
Ma is defined as CRaa
Note that the necessity of a statement comes out as a kind of modalized conjunction of that formula with itself, and possibility as a modalized disjunction. One rule in addition to those of PC will be employed:
| RR: | If
CaRa,
then
Ra. |
The propositional calculus base for the system will be not the full PC, but rather the classical implicational calculus, for which the axioms might be formula 2.11 (syl) and axioms C2 and C3. The axioms to be subjoined to classical implication are:
R1. CRpCpq
R2. CRCCpqqRp
R3. CLpCRqRCpq