Appendix

The Deduction Theorem in S4, S4.2 and S5

THE immediate purpose of our discussion of the deduction theorem in these modal systems is to show that

CLCpqCLCqpCdpdq

is a theorem-schema of S4, S4.2, and S5. But a statement of the deduction theorem for these systems is itself, I think, of considerable general interest.

Actually, there is no trick to merely stating the deduction theorem for any system. The problem is in getting an appropriate definition of "proof from hypotheses" for the system in question. Once we have such a definition, the statement and proof of the deduction theorem will ordinarily offer no problem. The systems with which we will be concerned are considered to be formulated on a PC base. They will contain, first of all, any basis sufficient for the complete CPC, including the rules of substitution and detachment. Each of these systems will also contain the rule "RL" : "If a is a theorem, so too is La."

The additional axioms are, for S4:

  1. CLCpqLCLpLq
  2. CLpp

For S4.2, axioms 1 and 2 and also:

 

3.

CMLpLMp

For S5, axioms 1 and 2 and also:

 

4.

CNLpLNLp

Since these systems are formulated on a PC base, we might suspect that a good part of the definition of "proof from hypotheses" will be exactly as for the CPC. This is the case; here we shall make use of Church's definition of "proof from hypotheses" for the CPC.(n1) The clauses of the definition as he states them are quite easily extendable to our modal systems. We may thus state what will amount to most of the definition:

  A finite sequence of wffs Bl, B2, . . ., Bm is called a "proof from the hypotheses Al, A2, . . ., An" if for each i, i £ m, either
  1. Bi is one of the Al, A2, . . ., An, or
  2. Bi is a variant of an axiom, or
  3. Bi is inferred by the rule of detachment from Bj and Bk, where j, k < i and Bj is of form Bk É Bi, or
  4. Bi is inferred by the rule of substitution from Bi, where j < i, and the variable substituted for does not occur in the Al, A2, . . ., An.

Note that Clause 2 above may be extended without difficulty to include the axioms of the modal systems with which we are concerned. We assume that the meaning of "varia    nt" is understood.

But one thing is missing from the above definition, so far as S4, S4.2, and S5 are concerned. This is a consideration of the role of the rule RL in a "proof from hypotheses." It is obvious that this rule is analogous to the rule of "universal generalization" in predicate calculi; we might, then, expect to get a hint of how to account for this rule by an examination of the way that "universal generalization" is accounted for in statements of the deduction theorem for predicate calculi.

In the definition of "proof from hypotheses" in the predicate calculus, the following move is permitted(n1) in the inference of a Bi from a Bj by universal generalization: Bi may be of form (a)Bj, where j < i and the variable a does not occur free in any of the hypotheses Al, A2, . . ., An.

The problem for us to find, for the systems S4, S4.2, and S5, an appropriate analog of the statement "The variable a does not occur free in any of the hypotheses Al, A2, . . ., An.

Such an analog is available. Prior has shown that S5 is derivable,(n2) and I have shown that S4 and S4.2 are derivable,(n3) by subjoining to the CPC the following rules:

 

R1:

If Cab is a theorem, so too is CLab.
 

R2:

 If Cab is a theorem, so too is CaLb, provided a is completely modalized.

The definition of "completely modalized" varies among these systems, and is the factor which distinguishes them. In S4, a wff is completely modalized iff either:

  1. It is a law of the system, every propositional variable of which is in the scope of a modal operator belonging to a, or
  2.  It is of the form KLgKLd . . . Ln, with Lg as a limiting case.

In S4.2 we have -- in addition to the above -- that a is completely modalized if:

 

3.

It is of the form NLNLb

In S5, a wff a is completely modalized provided every propositional variable of a is in the scope of a modal operator belonging to a.

Now, note that the complete quantif ication theory is formulable by subjoining to a complete CPC base the following:

 

RP1:

If Cab is a theorem, so too is CPxab.
 

RP2:

 If Cab is a theorem, so too is CaPxb, provided x is not free in a.

The similarity of the above rules to Rl and R2 for 'L' is obvious. And this similarity tells us what the analog for S4, S4.2, and S5 for, "The variable a does not occur free in any of the hypotheses Al, A2, . . ., An" will be. Let us now move to a statement of the final clause in our definition of "proof from hypotheses" for S4, S4.2, and S5.

  A finite sequence of wffs Bl, B2, . . ., Bm is called a "proof from the hypotheses Al, A2, . . ., An" if for each i, i £ m, either one of the four previously mentioned clauses holds, or
  5. Bi is inferred from Bj by RL, where j < i and each of the hypotheses Al, A2, . . ., An is completely modalized in the sense of the system in which we are working.

With these five clauses, then, defining "proof from hypotheses" in S4, S4 .2, and S5, we shall write

Al, A2, . . ., An B

for "there is a proof from the hypotheses Al, A2, . . ., An for the wff B."

The deduction theorem now will merely state that when

Al, A2, . . ., An B

then also

Al, A2, . . ., A(n - 1) An É  B

The proof of this theorem for the first four clauses of the definition of "proof from hypotheses" will be just like Church's proof.(n1)

The only extension of the proof needed is to cover our clause 5; this is easily accomplished. Let each of the Al, A2, . . ., An be completely modalized. And let B be Bi, such that if k < i, then

Al, A2, . . ., A(n - 1) An É  Bk

that is, the deduction theorem holds for Al, A2, . . ., An Bk. And also, Bi is inferred from Bj, j < i, by RL. This means that, by our definition of proof from hypotheses, and since Bi is B,

Al, A2, . . ., An B.

Now, since j < i, then also j < k, and we have

Al, A2, . . ., A(n - 1) An É  Bj

But then, since each of the hypotheses is completely modalized, we have also, by RL and our definition of proof from hypotheses:

Al, A2, . . ., A(n - 1) L(An É  Bj)

It is easily provable as a theorem of S4, S4.2, or S5 that, where a is completely modalized,

  CLCapCaLp  

But this means that we may move to

Al, A2, . . ., A(n - 1) An É  LBj

since we originally assumed that An, along with the other hypotheses, is completely modalized. But Bi was inferred from Bj by RL, and so is of the form 'LBj'. And this means that the deduction theorem holds for clause 5 of our definition. Note the role in the above proof of our requirement that all of the hypotheses be completely modalized.

Now we may quickly prove that the schema

CLCpqCLCqpCdpdq

is indeed a theorem schema of S4, S4.2, and S5. With the rule of substitutivity of strict equivalence, the following holds for these systems:

LCpq, LCqp Cdpdq

Note that the hypotheses in this case are completely modalized in any of three systems in question. But by the deduction theorem for these systems, the schema we wished to prove is proven.

Note that we could not in the general case in these systems have s stated:

Cpq, Cqp Cdpdq

even though -- as a rule -- the substitutivity of material equivalence holds in these systems. For in the general case there is no guarantee that the rule RL will not have to be applied to get the desired result, and by our definition of proof from hypotheses, its application would not be allowed in the last case, since the "hypotheses" there shown are not completely modalized in any of the three systems in question.