13.

THE SYSTEMS OF COMPLETE MODALIZATION -- SEQUENT-LOGIC, THE BASIC SYSTEMS

WE continue the general pattern we have established for this book by casting the systems of the last several chapters as Gentzen-style sequent-logics. We shall recall that at the heart of the Gentzenization of the absolutely strict systems was the rule ®L which -- subject to restrictions depending on the system involved -- permits the inference of LG ® La from  G ® a. The basic function of this rule for the systems of the present chapter will be similar; the main difference will be that the rule ®L for the systems of the present chapter will permit certain formulas in the sequent which is premiss of this rule to be carried as parameters into the conclusion, without having L prefixed to them. For the present systems, the formulas which may be so treated are those in the antecedent of the premiss which happen already to begin with L. The basic form of this rule for these systems then will be

We wish to prove the converses of *13.2 and *13.3. We may do so by showing that analogues of the LS3° and LS4° ®L rules hold in S3° and S4° respectively. Let us suppose that a formula i(D, LG ® a) holds in S4°; this formula is the interpretation of the sequent D, LG ® a, as defined in Chapters 3 and 8. It should be clear that by methods holding in the system T° we can move from the provability of this formula to that of i(LD, LLG ® La). But LpLLp is a thesis of S4°: Since each of the formulas of LLG is in an A-pos in i(LD, LLG ® La), SSS and LpLLp permit us to delete the initial L of each member of LLG, giving us i(LD, LG ® La) as provable. But this last formula is the interpretation of the conclusion of ®L for this case, giving us an analogue of this rule in S4°. We then have, with the above and *13.3:

Let us now suppose that D, LG ® a is a sequent such that Li(D, LG ® a) is provable in S3°, and that Li(D, LG ® LQ, a), LQ as in LS3°'s rule ®L, is also there provable. Note that -- as applies in Chapter 8 to LS2° -- the provability of the necessity of the interpretation is analogous to the provability of the sequent in LS3° without the use of an ®L with premises having empty antecedent. First of all, we recall that if G is empty, this rule becomes equivalent to ®L for LS2°, which has an analogue in S3°, since S2° is a subsystem thereof. We then consider the cases in which G is not empty. Of these, look first at the situation in which D also is not empty. Here the interpretation of the right premiss is equivalent to a formula

13.1

dCLga

and that of the left premiss to

13.2

dCgALq1 . . . ALqna

where the q₁, . . ., q_n. are the n formulas of Q; but this formula implies in S3° the formula

13.3

LALAq1 . . . qnCdCga,

while 13.1 implies

13.4

CLgCdCga

These last two formulas meet the requirements set by metatheorem *10.7. Such being the case, *10.7 will then allow us to assert that

13.5

LgdCga

is an S3° thesis; this in turn gives

13.6

LgCLdCLgLa

which even in S1° becomes

13.7

LdCLgLa

which is equivalent to the necessity of the interpretation of the conclusion of ®L for this case. If  D happens to be empty, we shall have, instead of 13.1 and 13.2,

13.8

Lga

and that of the left premiss to

13.9

gALq1 . . . ALqna

respectively. It is clear that by steps paralleling those above, we can come to

13.10

LgLa

as an S3° thesis; again, this is the necessity of the interpretation of the conclusion of ®L for this case. But then an analogue of LS3°'s ®L is a derived rule of inference in S3°, and so with the aid of *13.2 we assert

*13.5

a is a thesis of S3° iff ® a is provable in LS3°.

Since the normal form theorem is provable in these sequent-logics, we also have:

*13.6

LS3° (LS4°) provides a decision procedure for S3° (S4°).

Sequent-logics for S3 and S4

The systems of the preceding sections were introduced, with minor differences, in Zeman 1969. Sequent-logics for S3 and S4 were developed prior to those for S3° and S4°; for examples in the literature, see Ohnishi and Matsumoto 1957, Ohnishi 1961, Kanger 1957, Curry 1963, among others. As might be expected, LS3° and LS4° are extended to LS3 and LS4 respectively by adding to each of the former systems the rule L® as discussed in Chapter 8. It should be evident from the work of that chapter that the sequent ®.Lpp will be provable in both of these systems, and furthermore that -- by *5.6 -- an analogue of L® will hold in S3 and S4, making the interpretation of every LS3 (LS4) theorem provable in S3 (S4). Thus we have:

*13.7

a is a thesis of S3 (S4) iff ® a is provable in LS3 (LS4).

We note that in the literature on sequent-logics for S3 and S4, a somewhat different version of rule ®L than we have employed is used. The rule ordinarily used is like ours except that it lacks the sequence D in its premises. It is clear that rule L® may be applied a sufficient number of times to D, LG ® a to get LD, LG ® a as a premiss for the mentioned modification of ®L (which, of course, requires that all formulas in the antecedent of the premiss begin with L); the mentioned modification is clearly a subcase of our rule.

The normal form theorem for LS3 and LS4

The normal form theorem for these systems may be proved as an extension of the normal form theorem for LS3° and LS4°. Again, the relevant case is the induction step in the induction on grade at the base step in the induction on rank. For LS3° and LS4° the mix formula beginning with L was inserted at this step into both premises of the mix by applications of ®L. This is also a possibility for LS3 and LS4, but the treatment of this situation is just as for the nought versions of these systems. The other possibility for these systems is that the mix formula be introduced into the left premiss by ®L and into the right by L®. For LS3, such a proof with mix of grade k + 1 and rank 2 will conclude

D, G ® LL, a D, LG ® a   ®L LD, LG  ® La   a, X ® Q   L® La, X ® Q
	MIX
LD, LG, X  ® Q

This may be replaced by

D, LG ® a a, X ® Q
	MIX
D, LG, X ® Q L® LD, LG, X ® Q

Apply the final L® as often as needed to prefix L to each member of D.

The new mix falls within the scope of the induction hypothesis and so may be eliminated. The procedure for LS4 will be the same, the only difference being that the original proof ending will not need a left premiss for the ®L; the replacing proof ending will be identical to that shown above. In all other details the proof for the normal form theorem is the same as that for LS3° and LS4°. We then have

*13.8

The normal form theorem holds for LS3 and LS4.

We may use the sequent-logic LS4 to establish a relationship between the system IC of Chapter 2 and the modal system S4; this relationship was first established by McKinsey and Tarski 1948; the methods used there were algebraic. Let us suppose that a is a formula of IC; we shall define a translation function r as follows;

This function gives a means of translating any IC wff into a formula of S4; as examples we present the translations of the axioms of IC:

r(C1)	=	LpLqLrLpLqLpLr
r(C2)	=	LpLqLp
r(K1)	=	KLpLqLp
r(K2)	=	KLpLqLq
r(K3)	=	LpLqKLpLq
r(A1)	=	LpALpLq
r(A2)	=	LqALpLq
r(A3)	=	LpLrLqLrALpLqLr
r(N1)	=	LpLNLpLNLp
r(N2)	=	LNLpLpLq

We shall note that the following applies

*13.10

Where a is an axiom of IC, r(a) is a theorem of S4.

Proof of the above is simply a matter of carrying out the messy details of the individual proofs; for example, for r(C1):

13.11

CLpCLqLrCCLpLqCLpLr

PC, RL

By S3°'s pqLpLq and S1° we go from the above to

13.12

LpCLqLrLpLqLpLr

and by means of Lpp and SSS, we replace CLqLr (which is in an A-pos) in 13.12 by LqLr to obtain r(C1). The proof in S4 of the remainder of the axiom translations presents no difficulty and is left as an exercise for the reader.

We now shall assume that r(Cab) and r(a) are both provable in S4. Since the first of these formulas is r(a)r(b) and strict detachment holds in S4, r(b) is also provable in S4. Thus there is an analogue under the translation we are discussing in S4 for the IC rule of detachment. We now look at the IC rule of substitution. Suppose that j(a) is the IC formula which results from the substitution p / a in j(p). Consider the S4 wff r(j(p)) and suppose that it is an S4 thesis. Let us further suppose that the substitution indicated above is such that a is a prepositional variable. Then make the substitution  p / a in r(j(p)); the L required before every occurrence of a is there as a result of having been before every occurrence of p, and the result of the substitution is r(j(a)). Suppose now that in the IC substitution a = Cbg or a = Nb. Then in the S4 formula make the substitution p / Cr(b)r(g) or p / Nr(b) respectively. Once again the resulting formula will be r(j(a)). The L required before the C or N in each case is in place already as a result of having been in place before each occurrence of p in r(j(p)). Now suppose that a in the IC substitution was Kbg or Abg. Do the substitution p / Kr(b)r(g) or p / Ar(b)r(g) respectively. Here there is still an L left over before every place where p originally stood, and so before each initial K or A in the substituted formula. These L's must be eliminated, as the connective combinations LK and LA do not occur in the range of r. Therefore note first the LK or LA combinations that stand in C-pos in the formula; by means of Lpp and SSS replace each of these by K or A respectively. Next note the formulas beginning with LK or LA that stand in A-pos. By means of KLpLqLKpq and ALpLqLApq, both of which hold in S2°, distribute the L in each case getting the formula KLr(b)Lr(g) or ALr(b)Lr(g) where before the formulas beginning with LK or LA stood. If b or g is a propositional variable or begins with a C or an N, r(b) or r(g) begins with an L, and so by S4's LpLLp strictly implies Lr(b) or Lr(g) respectively, and so by SSS the extra L may be eliminated. If b or g begins with K or A, we have it standing in A-pos and so we again distribute the L; again the new L's will precede either another L, in which case they may be eliminated, or a K or A, in which case they are distributed again. The distribution eventually must bring each distributed L 'in contact with' an L preceding a propositional variable, a C or an N; each L originally preceding a K or an A in A-pos then may be eliminated, and we have r(j(a)) provable provided r(j(p)) is: we then have in S4 an analogue under the translation of the rule of substitution for IC; since we have also an analogue of detachment and *13.10 holds, we may then assert:

Now we shall wish to prove the converse of *13.11; to this end we shall employ the sequent-logics LS4 and LIC. Let G be a sequence of IC wffs; then r(G) shall be the sequence of S4 formulas resulting from the application of r to each member of G. We shall then work to establish:

We shall proceed by induction on the length of the longest proof string in the proof of r(G) ® r(Q); let the number of rule applications in that proof string be n; consider first the situation in which n = 0. Here the sequent in question is an axiom, r(a) ® r(a). G ® q₁ is then a ® a, which is an axiom of LIC; this establishes the base case.

Suppose now that *13.12 holds whenever n £ k. Consider the case when n = k + 1. The (k + 1)th step may be a structural rule weakening or contraction, but not cut, by *13.8. If by weakening in the antecedent, then r(a) is inserted into a sequent r(D) ® r(Q); by the induction hypothesis, one or more of the D ® q_i, i between 1 and n, will be LIC provable; since G = a, D, one or more of the G ® q_i is also LIC provable, by weakening in LIC. If the (k + 1)th rule is weakening in the succedent, we note first that if Q has just one member q, then G ® holds in LIC by the induction hypothesis and by weakening G ® q holds. If Q has m, m £ 1, members, the LS4 sequent in question came about by inserting r(q_m) into the succedent of a sequent with n = k; by the induction hypothesis, then, one of the sequents G ® q_i, i from 1 to m - 1 holds in LIC; then one or more of the set formed by adding G ® q_m to this set also holds.

If the (k + 1)th step is contraction in the antecedent, then the premiss to that step is r(a), r(G) ® r(Q) where r(a) is the contracted formula and a is in G. By the induction hypothesis, one of the a, G ® q_i is provable in LIC, and so by contraction there, so too will be one of the G ® q_i. If this step is contraction in the succedent, then the premiss to that step is r(G) ® r(Q), r(q_m) where q_m. is contracted wff and is also in Q; by the induction hypothesis, one of G ® q₁, . . ., G ® q_m, G ® q_m holds in LIC; but this is the same as saying that one of the G ® q_i, i from 1 to m, holds, as required.

The (k + 1)th step may also be by a logical rule. Given the nature of the function r, it may be one of the rules for A or K, or one of the rules for L. If this step is by rule K®, then r(G) = r(Kab), r(D), which is ti say. r(G) = Kr(a)r(b), r(D); the premiss to this step is then r(a), r(b), r(D) ® r(Q). This sequent falls into the scope of the induction hypothesis, making one of the sequents a, b, D ® q_i provable. By K® in LIC, then one of the sequents Kab, D ® q_i (= G ® q_i) is so provable. If the rule is ®K, then r(Q) = r(L), Kr(a)r(b); the premises for this rule are then r(G) ® r(L), r(a) and r(G) ® r(L), r(b); with q₁, . . ., q_{m - 1} the members of L, this means that, by the induction hypothesis, either one of G ® q_i, i from 1 to m - 1, or both of G ® a, G ® b are LIC provable; in the first case weakening and in the second ®K in LIC make one or more of G ® L, Kab provable in LIC.

If the (k + 1)th step is by A®, then G = Aab, D, and the premises of this step are r(a), r(D) ® r(Q) and r(a), r(D) ® r(Q). In LIC, then, it will be the case that one or more of the sequents a, G ® q_i as well as one of the sequents b, G ® q_i is provable. Let, then, a, G ® q_x, and b, G ® q_y, be so provable. If x = y, get Aab, G ® q_x by A®; if x or y but not both = 0, insert q_x or q_y as appropriate by weakening in the empty succedent, and apply A® as above. If x ¹ y and neither is 0, use ®A to get a, G ® Aq_xq_y and b, G ® Aq_xq_y as provable in LIC; an application of A® now gives us Aab, G ® Aq_xq_y. as provable. Now, it is the case that in LIC a sequent of form :X ® Agd is provable iff one or both of X ® g and X ® d is provable. Thus one or both of Aab, G ® q_x and Aab, G ® q_y are provable, and since x and y are £ m, one or more of the Aab, G ® q_i are provable, as required. If the (k + l)th step is by ®A, then Q = L, Aab and the premiss of the rule application is r(G) ® r(L), r(a), r(b), with L = q₁, . . ., q_{m - 1},. By the induction hypothesis then one of the sequents G ® q_i, i from 1 to (m - 1), or G ® a, or G ® b is provable. But as we have noted, this is equivalent to saying that one of the sequents G ® q_i, i from 1 to (m - 1), or G ® Aab is provable, as required for *13.12.

The (k + 1)th step may also be by one of the L rules. First let us consider the possibility that the rule, L® or ®L, involves a side formula which is a propositional variable. This side formula was introduced into the proof originally either as part of an axiom or in a weakening step. If p was introduced by a weakening step, introduce instead Lp at that point; the L-introduction rule earlier assumed to introduce Lp is then unnecessary unless that step was ®L with premiss D, LG ® p and conclusion LD, LG ® Lp. In this case the new proof would not be reduced to k steps unless D were empty, for L® would have to be applied as often as necessary to prefix L to each member of D. To handle this situation we note that LS4 could have been formulated with a version of ®L in which D is always empty. All other details of the current proof will follow through in that version, and the present difficulty does not arrive. Thus, whenever a variable introduced by a weakening step is later prefixed by an L, the proof in question may be shortened as required by the induction hypothesis. If a variable later prefixed by an L is originally introduced as part of an axiom, we note the following. In LS4, every proof may be replaced by one with the same conclusion, but beginning only with axioms a_i ® a_i where a_i is a propositional variable. Suppose otherwise; then there is a proof with an axiom b ® b at the top of one of its branches which sequent cannot be the conclusion of one of the LS4 rules and having b beginning with a connective; but examination of LS4's rules shows that every provable sequent which contains a connective can be the conclusion of a rule application, contrary to the hypothesis. Every proof of LS4, then, can begin only with axioms containing no connectives. But the special subclass of LS4 provable sequents we are now considering contains only formulas in the range of the function r; in such formulas every variable is prefixed by an L. Considering the L and its variable as a unit, we may apply the above argument to show that every sequent of this subclass is provable in a proof beginning only with axioms of form La_i ® La_i, where a_i is a variable. So we begin the proof in question with La_i ® La_i instead of a_i ® a_i and omit the (k + 1)th (L-introducing) rule. Again, there is a problem in our formulation if that rule happens to be ®L with premiss D, LG ® p, where p = a_i; again, we handle this problem by noting that we could have used the equivalent formulation in which D in this rule is always empty. We note, then, that whenever the (k + 1)th step is an L rule and the side formula is a propositional variable, the proof may be shortened to bring it under the induction hypothesis.

The other possibilities when the (k + l)th step is an L rule are that the L is prefixed by that rule to a formula beginning with a C or with an N. Suppose, first of all, the former, and suppose that the L rule in question is L®. The antecedent G of the LIC sequent for which the value of r is the (k + 1)th step of our LS4 proof is then Cab, D. The premiss of the L-introduction in question then is Cr(a)r(b), r(D) ® r(Q). This sequent, because of the initial C, contains a formula not in the range of p. But it itself is derivable by a C® whose premisses are r(D) ® r(Q), r(a) and r(b), r(D) ® r(Q), both of which are in the range of r and for which n is less than k. By the induction hypothesis, then, one or more of the sequents D ® a and D ® q_i, i from 1 to m, as well as one or more of the sequents b, D ® q_i, i from 1 to m, is LIC provable. Suppose that one of the D ® q_i holds. Then, simply by weakening, one of the Cab, D ® q_i holds as well, as required. Suppose, on the other hand, that D ® a holds. Since one of the b, D ® q_i holds, we may use it and D ® a as premises for C® to obtain the required sequent as provable.

Suppose again that the L rule involved is L®, and that the side formula for that step begins this time with N. G (in LIC) is then Na, D, and the premiss of the L-introduction is Nr(a), r(D) ® r(Q). Again, it does not fall into the range of the function r, but the proof is again invertible so that the premiss leading-to the premiss of the L-introduction is the sequent r(D) ® r(Q), r(a); this is in the scope of the induction hypothesis and in the range of the function r, so one of the sequents D ® q_i, i from 1 to m, and D ® a is LIC provable. If one of the former, insert Na by weakening to obtain one of the sequents Na, D ® q_i as provable. If the latter, then apply N® first to get Na, D ®; this sequent qualifies, although any of the q_i; may now be inserted right by weakening.

Now suppose that the L in question is introduced on the right, by ®L. Since this rule demands a singulary succedent, Q is precisely Cab or Na. If Cab, then the premiss of the ®L is r(G) ® Cr(a)r(b) (note that we have D empty here by the same argument given in the last paragraph); this last sequent can have, by appropriate inversions, r(a), r(G) ® r(b) as its premiss. This sequent is in the range of p and is provable in fewer than k applications; a, G ® b is then LIC provable (note that if a, G ® is provable, we add b by weakening), and so we get G ® Cab in LIC by ®C. If Q is Na, we have r(G) ® Nr(a) and so r(a), r(G) ® provable in k or fewer steps. Thus a, G ® holds in LIC, and by ®N we then have the required G ® Na. If, then, r(G) ® r(Q) is provable in LS4, we shall always have one or more of the sequents G ® b_i, i from 1 to m, provable in LIC; so * 13.12 holds, and we have, by this and *13.11:

It will be noted that this rule permits a multiple succedent, one with more formulas than one, provided the formulas in that succedent which are parametric begin with L. If  Q is empty, the rule becomes ®L of LS4°; LS5 then contains LS4; further, note the proof:

Lp ® Lp ®N ® Lp, NLp ®L ® Lp, LNLp N® NLNLp ® Lp ®C, Df. M ® CMLpLp
	®L
® MLpLp

Let us now consider this version of ®L from the point of view of S5. If d is the conjunction of the formulas of D, g the conjunction of the formulas of G, and q^L the disjunction of the formulas of LQ, the interpretation (in the sense in which we have been using that term to relate the sequents of a Gentzen system with ordinary formulas) of the premiss of ®L is equivalent in S5 to the formula CdCLgAq^La. This in turn is equivalent (by PC methods) to CKLgNq^LCda. In *11.1 it has been shown that *10.5 applies to S5 as follows: if Cab is an S5 thesis and if each of a's variables is in the scope of a modal operator belonging to a, then CaLb is an S5 thesis. But every variable of KLgNq^L is in the scope of such a modal operator, and so we are able to infer to CKLgNq^Lda., which in S1° yields CKLgNq^LCLdLa.; by PC this last gives CKLgLdAq^LLa.. This formula is, of course, equivalent to the interpretation of the conclusion of LS5's ®L rule. We then conclude that if a given sequent is provable in LS5, its interpretation is a thesis of S5, and with *13.14 this gives us

We have remarked that LS5 differs from the other sequent-logics we have been studying in an important respect. The most obvious respect so far in which it differs from them is that its ®L has parametric formulas in its premiss's (and its conclusion's) succedent. This leads to a significant thing -- the normal form theorem is not provable in LS5. Specifically, we shall refer to the induction step in the induction on rank in that proof (see Chapter 3), and in that step to the subcase in which the left premiss of the mix to be eliminated is generated by a rule application with the mix formula parametric in its succedent, and the left rank of this mix is, of course, ³ 2. As we noted in our discussion of the normal form theorem for LS3° and LS4°, the case in which this rule -- the one generating the left premiss for the mix of this subcase -- is ®L is excluded for this subcase, for otherwise the left rank would have to be 1, which is contrary to the hypothesis. But for LS5 we must consider ®L as a possibility for the generator of the left mix premiss. Suppose we had a proof (at this subcase) ending thus (with mix formula La):