IN Chapter 7 we presented PCbased formulations of the systems S1°T; we shall now do the same for S3°S5. Again we shall take C, N, and L as primitive connectives, and the definitions employed will be as in Chapter 7.
The postulated rules of inference will be drawn from those employed in Chapter 7. Among them, of course, will be substitution for variables and material detachment; for reference, we repeat the modal rules that will be used:
RLE: 
If La, then a. 
RL: 
If a, then La. 
RL2 
If a is a PC theorem or a theorem of form CLbg, a, then La. 
S3° and S4° will contain the full PC (an appropriate CN base plus detachment and substitution); both systems will also have rule RLE. In addition, both will employ the following axiom:
L4. CLCpCqrLCLpCLqLr
The distinction between the systems is as follows:
(1)  S3° employs in addition the rule RL2 
(2)  S4° uses RL instead of RL2. 
Axiom L4 is formula 10.6; the rest of the basis of the present S3° is clearly contained in the original S3°. Going the other way:
12.1 
LCCpqCpq 
PC, RL2 
12.2 
CLCpqCLpLq 
D(L3)(12.1), RLE 
Formula 12.2 is axiom L2, which if substituted for L4 in the basis of S3° above would give Chapter 7's basis for S2°. The present S3° therefore contains S2° and so S1°.
12.3 
pqCrpq 
Sl° 
12.3 
pCpqpq 
Sl° 
Recalling that formula 2.10 is syl, CCpqCCqrCpr, we do:
12.5 
CpqLpLq 
D(D(2.10)(12.3))(12.4) 
12.6 
pqLpLq 
12.5, RL2 
Formula 12.6 is the same as formula 10.2, which is deductively equivalent (given S1°) to axiom M8 in our original formulation of S3°. The present formulation of S3°, then, contains and so is equivalent to the original. One might wonder why we use the more complex axiom L4 in place of 12.6 as proper axiom for S3° in this formulation. Indeed, we shall use this latter formula in our formulation of S3 and S4. These systems will contain as an axiom the formula CLpp which will make possible the immediate derivation of axiom L2, so establishing that these systems contain S1 and S2. But the derivation of L2 from PC + RLE + RL2 (or RL) + CLCpqLCLpLq is another question. I have been unable to accomplish this derivation. Also, I have been unable to show that the derivation is impossible, although I conjecture that this is the case. Thus we employ axiom L4 for the nought systems.
We noted in Chapter 10 that if any thesis beginning with two L's were added to S3°, the result would be the system S4°. It is clear that substituting rule RL for rule RL2 in the present S3° makes such formulas provable; the system resulting from such a substitution then contains S4°. Since RL is provable in S4° (original), the present S4° is contained in turn in the original, and so is equivalent to it.
We could form Lemmonstyle bases for S3 and S4 simply by replacing the postulated rule RLE by axiom L3, CLpp respectively in S3° and S4° as above formulated. But as we have indicated, we can come up with a simpler formulation. To formulate S3 and S4, make the replacement of rule RLE by axiom L3 as indicated, and in addition, replace axiom L4 in the nought systems by axiom
L5. CLCpqLCLpLq
Given the work already done, it should be clear that the present S3 and S4 are equivalent respectively to the original S3 and S4. Another way of formulating S4 and S4° would be to add CLpLLp as an extra axiom to any of the other systems of this chapter or of Chapter 7 (adding it to a nought system, of course, gives S4°). Similarly the system S5 may be formulated by adding
L6. CMLpLp
to any of the systems of this chapter or Chapter 7 (assuming that LCMLpLp will be a thesis). Alternatively, one could add either of the deductively equivalent formulas
12.7 
CMpLMp  
12.8 
CNLpLNLp 
to any of these systems. S5 lends itself to a variety of manners of formulation on a PC base. An economical way of setting this system up is simply to replace axiom L5 in, say, S4 above by
L7. CMLCpqCLpLq
Axiom L7 is clearly a thesis of S5. With axiom L3 and PC, we have
12.9 
CLpMLp  
12.10 
CLCpqCLpLq  D(D(2.10)(12.9))(L8) 
The suggested system then contains T.
12.11  CMLqMLCpq  S2° 
12.12  CMLqCLpLq  D(D(2.10)(12.11))(L7) 
12.13  CMLqLq  12.12, S1° 
PC + RL + L3 + L7, then, is equivalent to S5.
Another formula which may be used in formulating S5 is
12.14  CCLpLqLCLpLq 
If this formula is subjoined to S4, for example, the result is S5. The reader might like to verify this for himself and to investigate the effect of subjoining this formula as an axiom to each of the other systems we have been studying. We might suggest the same kind of investigation regarding axiom L7, seeing what happens when L7 replaces the distribution axiom in each of the systems of this chapter and Chapter 7 (axiom L1 for S1° and S1). We shall now state formally:
*12.1  The systems S3°, S4°, S3, S4, and S5 as formulated in this chapter are equivalent to the respective systems as originally studied in this book. 
In Chapter 7 we discussed the system M of von Wright 1951; M is equivalent to our T. Von Wright sets down two other systems as extensions of M; the system M¢ is M plus
vW3. CMMpMp
and M² is M plus
vW4. CMNMpNMp
Clearly, M¢ is equivalent to S4 and M² to S5.
Also in Chapter 7 we presented the basis for T of Zeman 1968a; this system has material implication and impossibility (R) primitive. Noting that M in this system is defined as 'Ma for CRaa', it is easy to determine that T plus
R4. CRpRCRpp
is S4, and T plus
R5. CCRppRRp
is S5.
S5 may be formulated with other modal connectives primitive. This system, for example, is one of a family of systems (others of which will be discussed in a later chapter) which may take 'possible necessity' as primitive (Zeman 1969a). Read Qa as 'a is possibly necessary', and set up the definitions
La is defined as KQaa  
Ma is defined as ANQNaa 
Take rule RL and axioms L2, L3, and L6 and replace each of the L's in the rule and each axiom by Q. Subjoined to the PC, this gives a system equivalent to S5. (The equivalence between the Q and the Lprimitive systems is somewhat trivial here, but becomes more interesting in the rest of this family of systems.)
'Contingency' may also be used as a primitive modal operator for S5 (Lemmon and Gjersten 1959); read Ta as a is contingent' (that is, 'a is neither necessary nor impossible'). Define L as follows
La is defined as KaNTa 
Subjoin to PC the rule
RT: If a, then NTa
and the axioms
Tl. ETpTNp
T2. CNTEpqCTpTq
T3. CTCpqCNTpp
T4. NTCpTp
The result is a system equivalent to S5.
We have studied a number of bases for each of the systems from S1° to S5; all these foundations have in common the property of having postulated rules of inference aside from the PC's rules of detachment and substitution. There may be some interest in knowing whether or not it is possible to axiomatize any of these systems in such a manner as to have material detachment and substitution for variables as the only postulated rules of inference, preserving meanwhile a property which must be considered desirable in logics such as we have been studying: the property of being axiomatizable with only a finite number of axioms. The question is answered affirmatively for S4 and S5 in McKinsey and Tarski 1948; Simmons 1953 contains a similar result for S3. That there are Lewis modal systems which are not so axiomatizable is shown, for example, in Lemmon 1965; among the systems which are not axiomatizable with a finite number of axioms and only detachment and substitution as rules are S2 and T as first shown by Kripke. Systems which may be so formulated are called 'finitely axiomatizable'; Canty 1965 also refers to them as 'classically axiomatizable'.
Simmons's basis for S3 has, of course, the rules of substitution for variables and material detachment and also the axioms:
Fl. pKpp
F2. Kpqp
F3. KKrpNKqrKpNq
F4. CNMpNp
F5. pMp
F6. pqNMqNMp
To form S4, add to the above system axiom M8, which we state again here as
F7. MMpMp
Adding axiom
F8. MpNMNMp
which is the same as axiom M9, to S3 clearly extends it to S5; it might be suspected, however, that axiom F5 would then become nonindependent (just as axiom M6 does when M9 is added to S1); that this is the case is shown in Sobocinski 1962.
One immediate result of the fact that S3, S4, and S5 are able to be formulated as above is that the deduction theorem is provable for them in these formulations exactly as it was for the systems containing the positive implicational calculus in Chapter 2. We shall have more to say about the deduction theorem later in this chapter.
Formulations without axioms beyond those of the PC
Łukasiewicz 1951 presents a method of formulating ordinary classical quantification theory without the use of axioms beyond those of the PC. Taking the universal quantifier as primitive and using Px as the universal quantifier for x, this method calls simply for the addition of the following rules of inference to PC:
P1: If Cab, then CPxab.
P2: If Cab, then CaPxb, provided x is not free in a.
Appropriately modified versions of these rules employing the existential rather than the universal quantifier may also be used, of course. Prior 1962 presents an analogous method of formulating the system S5, which we shall study shortly. Versions of the Lukasiewicz method exist for a number of other systems as well, including S3 and S4.
Each of the systems in question consists of the PC plus a pair of rules. One rule, common to all these calculi, is an analogue of rule P1 above
RLA: If Cab, then CLab.
It should be evident by now that modality behaves in many ways like quantification; rule RLA emphasizes this point. Rule RLA is derivable, of course, even in system S1; see metatheorem *5.8.
S3, S4, and S5 in their present versions will be distinguished by the second modal rule, the one paralleling rule P2. We shall first examine this rule as stated for S3. The version of this rule for S3 is considerably more complicated than are the S4 and S5 versions; we present it not so much as a nice elegant way to axiiomatize S3 but rather as a demonstration of S3's family relationship to S4 and S5. Recall that a formula is completely modalized in the basic sense of S4 if it is of form Lb or is a conjunction of formulas of this form. If a is completely modalized in this sense, then let a* be the formula formed by stripping the 'initial L's' from a; given the above definition of complete modalization, a* is then b or Kb_{1}Kb_{2} . . . b_{n}. as the case may be. We then postulate:
RLC3:  If Cab, then CaLb, provided either:  

First of all, we note that so far as clause 1 of the proviso is concerned, rule RLC3 is provable even in S1°, by CpqCLpLq and CKLpLqLKpq. For cases falling under clause 2a of the proviso, this rule holds in S3° by metatheorem *10.6. For case 2b, observe that if a is contradictory, then CaLb holds by PC. We now consider the cases in which a is not contradictory. If it is a theorem of S3, then so too will b be a theorem. If it is not a theorem, then there will always be substitutions available which will transform it either into a theorem or into a contradiction. This is obvious when a is simply p, that is, when it has no connectives. Assuming it to hold when it has k or fewer connectives, consider the cases in which it has k + 1. Then it will be of form Cgd or Ng (assuming CN primitive). By the induction hypothesis, find substitutions to convert g in each of these cases to a contradiction, and a becomes a thesis. Since a and b do not share any variables, these substitutions may be made into Cab without affecting b, so converting it to C1b; b may then be detached as a theorem in all cases in which a is not contradictory. In these cases, then, CL1b then holds by PC, and metatheorem *10.6 may be applied to give CL1Lb; Lb too, then, is a theorem, and by PC again, so too will be CaLb. These are all the cases covered by the provisos of RLC3, which then holds in S3 (actually, in S3°).
We now shall show that PC + RLA + RLC3 contains, and so is equivalent to, S3:
12.15  CCpqCpq  PC 
12.16  CKLCpqLpq  12.15, RLA 
12.17  CKLCpqLpLq  12.16, RLC3 (clause 1) 
12.18  CLCpqCLpLq  12.17, PC 
12.19  ALpCLpLq  PC 
12.20  CLCpqLCLpLq  12.18, 12.19, RLC3 
This is, of course, axiom L5.
12.21 
Cpp  PC 
12.22 
CLpp  12.21, RLA 
And this is axiom L3. Where l is any PC thesis, and p is not a variable of l, we may write
CCppl  PC  
12.24.1 
CCppLl  12.23, RLC3 
The last step is permitted under clause 2b of RLC3 since p is not in l and ALgl is a PC theorem.
12.24.2  Ll  12.24.1, PC 
Where l is any PC thesis, then, Ll is a theorem of the present system.
12.25  CLgd  Hyp 
12.26  CppCLgd  12.25, PC 
We assume that p in 12.26 is not a variable of g or d.
12.27  ALgCLgd  PC 
12.28  CppLCLgd  12.26, 12.27, RLC3 
12.29  LCLgd  12.28, PC 
We see, then, that any material implication in the current system whose antecedent begins with an L may be converted to a strict implication. Lines 12.2312.29 above, then, establish that rule RL2 is a derived rule of inference in our system. Since we have already established that axioms L3 and L5 are in this system, we see that the present system contains S3 and so is equivalent to it.
We now turn to similar bases for S4 and S5. As we have remarked, the form of the rule analogous to Łukasiewicz's P2 for these systems is simpler than that for S3; it will be essentially the same for both S4 and S5:
RLC:  If Cab, then CaLb, provided either:  

We distinguish between the systems by means of their differing notions of complete modalization; as it turns out, clause 2 above is redundant for S5. As we have mentioned, this formulation of S5 is due to Prior 1962; the version of S4 presented here is essentially that of Zeman 1963; the proviso on the rule here differs slightly from the proviso on the rule in the latter paper, and has the advantage of not tampering with the definition of complete modalization for S4. In Zeman 1963 clause 2 above was omitted and the definition of complete modalization was extended to include certain PC theorems; here we shall, as before in this book, call completely modalized those formulas beginning with L or of form Kab where a and b are completely modalized. The cases of RLC covered by clause 1 of the proviso are seen to hold for both S4 and S5 by *10.4 (recall that a formula is completely modalized in S5 provided each of its propositional variables is in the scope of a modal operator belonging to that formula); *10.4 is proved for S4 and S5 in Chapter 11. The proof of this rule for the cases covered by clause 2 is similar to that for clause 2b of rule RLC3. Again, if a is contradictory, CaLb holds as a PC theorem, and if a itself is a theorem, then b may be detached as a thesis. If a is neither a theorem nor a contradiction, we need only extend the proof that substitutions are always available to make it a theorem from the restricted case employed in the proof of RLC3. There we assumed that a in this situation had no modal operators; all we need do here is extend the induction step of that proof to cover the case when a is of form Lg. By the induction hypothesis, substitutions are available to convert g to a thesis, and by the unrestricted RL which holds in both S4 and S5, Lg too may be converted to a thesis by the same substitutions. Thus again, in each case in which (under clause 2) a is not a contradiction, it may by substitutions be converted to a thesis (without affecting b); b may then be detached as a thesis itself. The unrestricted RL is then applied to b giving Lb. By PC, then, CaLb will be a theorem, as required.
We note that we have above established incidentally another result about S4, and indeed about T° and all the systems including it. Recall that in Chapter 10 we discussed the 'unreasonableness' of S3 and some of its included systems. In the process of proving RLC3 and RLC, we established using methods that hold in T° that if a formula is equivalent neither to the negation of a theorem nor to a theorem, then there are substitutions available to convert it to a theorem or to the negation of one. Consider a theorem Aab of T, S4, or S5 (or the respective nought systems) and suppose that neither is a theorem, and further, that a and b have no variables in common (recall that systems containing such disjunctions as theses are 'unreasonable in the sense of Hallden'). Aab is equivalent to CNab; if a is a contradiction, then b may be detached as a theorem, contrary to the hypothesis. But since a may not be a theorem, we may substitute to make it a contradiction; since substitutions into a do not change b, b may in any case be detached as a thesis. The systems containing rule RL, then, are not 'unreasonable'.
Returning now to RLC, we note that that rule has now been shown to hold in S4 when the S4 notion of complete modalization is used and in S5 when S5's definition is used. We now turn to the other direction of the proof. Assume PC plus RLA and RLC with the S4 version of complete modalization. Then
12.30  CCpqCpq  PC 
12.31  CLCpqCLpq  12.30, RLA, PC 
12.32  CKLCpqLpq  12.31, PC 
12.33  CKLCpqLpLq  12.32, RLC 
Note that the antecedent of 12.32 is completely modalized in the sense of S4; also, the antecedent of the following is so modalized:
12.34  CLCpqCLpLq  12.33, PC 
12.35  CLCpqLCLpLq  12.34, RLC 
This last formula is axiom L5.
12.36  Cpp  PC 
12.37  CLpp  12.36, RLA 
And 12.37 is axiom L3.
12.38  a  Hyp. 
Now, let p be a variable not found in a:
12.39  CCppa  12.38, PC 
12.40  CCppLa  12.39, RLC (clause 2) 
12.41  La  12.40, PC 
The movement from 12.38 to 12.41 establishes RL as a derived rule of the current system. With RL, 12.35, and 12.37, this system contains and so is equivalent to S4.
The S4 definition of complete modalization is contained in the S5 definition. The above proofs then are performable in the system which is PC plus RLA plus RLC with the S5 notion of complete modalization. In addition:
12.42  CMpMp  PC 
12.43  CMpLMp  12.42, RLC (S5) 
12.43 plus S4 gives S5; the present system is then equivalent to S5. We remarked earlier that clause 2 of the proviso on RLC is unnecessary when the S5 definition of complete modalization is used for clause 1. Noting that clause 2 is used only in the proof of RL in S4, we leave it to the reader to satisfy himself that this clause is indeed redundant for S5.
The deduction theorem for the systems of this chapter
We mentioned earlier in this chapter that given the 'finite axiomatizability' of S3, S4, and S5, the deduction theorem will be provable in those systems; the proof, if we use one of the bases of finite axiomatization, is just the same as the proof for the positive implicational calculus, since the rules of inference used are the same: substitution and detachment. The Lemmonstyle bases of this chapter are somewhat more natural than those of Simmons, however, and so there might be some advantage in proving the deduction theorem for them. Here, of course, we have an extra postulated rule of inference (RL or RL2), and so the proof of the deduction theorem must be adjusted to take account of it. We define 'deduction' as in Chapter 2; that is, a step in a deduction may be one of the hypotheses or a variant of an axiom, or derived from previous steps by detachment or substitution (with the appropriate restriction); and we add to the four clauses of Chapter 2's definition a fifth clause to cover rule RL (or RL2 for S3). In addition to the steps permitted by those four clauses, a step in the proof may be
5. 
Inferred from a previous step in the proof by application of rule RL (RL2 for S3), provided each of the hypotheses employed in the deduction of that previous step meets the restrictions of one of the clauses of rule RLC (RLC3 for S3). 
The restricting clauses of RLC and RLC3 have reference to the antecedent and the consequent of an implication; we may apply them to deductions as in 5 above simply by understanding 'hypothesis' for 'antecedent' and 'conclusion' for 'consequent'. We shall first note that the converse of the deduction theorem holds for our extended definition of deduction. Suppose that the following holds:
12.44  a_{1}, . . ., a_{n} Cgb  Hyp. 
If there are no applications of RL or RL2 in this deduction, it is clear that a_{1}, . . ., a_{n}, g b, that is, that the converse of the deduction theorem holds. Supposing it to hold whenever there are k applications of RL (RL2 for S3) in the deduction, consider the case when there are k + 1 such applications. The (k + 1)th application occurs somewhere up in the deduction, and may be considered a movement from
12.45  a_{1}, . . ., a_{n} q 
to
12.46  a_{1}, . . ., a_{n} Lq 
Of course, the restrictions on the application of RL or RL2 will have been observed. By PC methods, we move from 12.45 to
12.47  a_{1}, . . ., a_{n} Cgq 
and thence by the induction hypothesis to
12.48  a_{1}, . . ., a_{n}, g q 
It is clear that g is not a hypothesis that need be employed in the deduction of q in 12.48 (unless it is one of the a_{1}, . . ., a_{n}, in which case it is already accounted for so far as the application of RL or RL2 is concerned). Thus we may apply RL or RL2 to 12.48 to get
12.49  a_{1}, . . ., a_{n}, g Lq 
Now in the original proof of 12.44, the steps from 12.46 to 12.44 were all PC steps; clearly, if we can move from 12.46 to 12.44 by PC methods, we can go from 12.49 to
12.50  a_{1}, . . ., a_{n}, g b 
by PC methods; we may then consider the converse of the deduction theorem to hold given our present definition of deduction.
We turn now to the deduction theorem itself; all we need do here is to extend the proof of the induction step of that theorem in Chapter 2 to the case in which the last ((k + 1)th) step in the deduction of b from a set of hypotheses is by RL or by RL2. Where b_{i} is the previous step to which the rule was applied, the statement of deducibility we are concerned with is
12.51  a_{1}, . . ., a_{n} Lb_{i} 
By the induction hypothesis, we shall have the following
12.52  a_{1}, . . ., a_{n  1} Ca_{n}b_{i} 
Suppose first of all that a_{n} was not employed at all in the deduction of b_{i}; then we shall have
12.53  a_{1}, . . ., a_{n  1} Lb_{i} 
which by PC methods becomes
12.54  a_{1}, . . ., a_{n  1} Ca_{n}Lb_{i} 
So in this case the deduction theorem holds trivially. If a_{n} is employed in the deduction, then by our proviso it must meet the requirements of RLC or RLC3 as appropriate, and so in any of the systems with which we are concerned, we may derive as a thesis
12.55  Ca_{n}La_{n} 
Since we can apply RL to derive 12.51, the hypotheses in 12.52 will be such as to enable us to apply RL (or RL2) to it to get:
12.56  a_{1}, . . ., a_{n  1} LCa_{n}b_{i} 
and then by methods common to all these modal systems, we move to
12.57  a_{1}, . . ., a_{n  1} CLa_{n}Lb_{i} 
Now 12.55 permits us to go from 12.57 to 12.54. We thus have shown that
*12.2  The deduction theorem and its converse hold in S3, S4, and S5 in the Lemmonstyle bases. 
We may note that in Zeman 1967b deduction from hypotheses is defined in a manner differing slightly from that of the present section. The present section requires only that hypotheses involved in the deduction of a given proof line be completely modalized in order that a rule to prefix L to that proof line may be applied. That article requires that all the hypotheses be completely modalized in order to apply the rule RL. Although the deduction theorem can be proved with this stronger definition of deduction, the converse of the deduction theorem cannot, and so the present notion of deduction is preferable.
A question which may arise at this point is that of the deduction theorem in the absolutely strict systems. We did not treat this topic in our study of those systems, and, indeed, it has been claimed (Feys 1965, p. 80) that the deduction theorem does not hold in at least some of those systems (S2, and by easy extension of the arguments offered there, T). The statement of the deduction theorem there is, however, in error; what is claimed is that the deduction theorem concludes to Cab whenever b 'is derived from' a (Feys refers also to a stronger version of this theorem, in which the strict ab would be the conclusion; this, I think, is best thought of not as a version of the deduction theorem, but as a combination of that theorem and some rule to prefix L to a formula). Feys seems to take his claim to mean that whenever we have a rule of inference of form 'If a, then b', then Cab is a theorem. This, of course, is not what the deduction theorem says. If a (and so b) in such a rule of inference is actually a theorem, then Cab is rather trivially a theorem, by PC. On the other hand, if a is taken to be an arbitrary wff, the suggested meaning of the deduction theorem does not hold even in the propositional calculus. The rule of substitution in PC permits us to say 'If a then ' when b is derived from a by replacing one of a's variables uniformly at each of its occurrences by some wff. But we cannot, for arbitrary a, conclude to Cab from this (let a = p and b = q, for example). Thus Feys cannot argue as he does from the fact that Becker's rules hold in S2 while CpqMpMq does not to the conclusion that the deduction theorem does not hold there. The point is that certain rules (such as substitution in PC or universal generalization in quantification theory) which may be applied in unrestricted fashion when moving from theorem to theorem must be restricted when moving from step to step in a deduction from hypotheses.
There is, indeed, a sense in which the deduction theorem does hold in T and S2, but I feel that it is a fairly trivial sense. Assuming the Lemmonstyle bases of Chapter 5, let us add to the clauses of the definition of deduction in Chapter 2 the following; in addition to the steps permitted by the four PC clauses, a step may also be
5¢. 
Inferred from a previous step in the deduction by rule RL (for T) or rule RL2 (for S2), provided none of the hypotheses was used in the derivation of that previous step. 
The reader may satisfy herself using the methods of the present chapter that the deduction theorem and its converse follow given this definition of deduction. Of course, this means that the rules to infer a step La of a deduction from a step a may be applied only when a is a theorem. Because of the extreme restriction on this clause, this definition of deduction is a relatively trivial extension of the definition for PC.