Tableaux for S4 and S4

WE shall now extend the work of Chapter 9 as well as of Chapter 13 to develop models for the completely modalized systems. As Chapter 9 began its studies with the systems T and T, so will this chapter begin with S4 and S4. As was indicated in Chapter 9, the characteristic feature of model structures for the systems of the current section is the fact that the accessibility relation here will be transitive; thus we shall speak of model structures MS4 and MS4 which have a transitive accessibility relation. The accessibility relation in MS4, as in MT, will be reflexive as well. The MPC rules and the rule L-r will be the same here as for MT and MT; note, though, that because of the transitivity of the accessibility relation, any tableau bearing the ancestral of the auxiliarity relation to a tableau tl will itself be auxiliary to tl, and so will have formulas carried into it by applications of rule L-l in tl. This is not true, of course, in the general case for MT and MT. Another way of looking at the situation is to note that in situations in which the rule L-l is to be applied creation of the countermodel demands that p be true in every world accessible to the world (call it w1) corresponding to the tableau tl in which the L-l is performed. Suppose that p is false in some world w3 accessible to a w2 which in turn is accessible to wl. By transitivity, w3 is accessible to wl, and so Lp could not hold in wl. If, then, Lp does hold in wl, p must also hold in w3; more generally, if a world wx has access to a world wy and Lp holds in wx, then p must hold in every world accessible to wy as a part of its holding in every one accessible to wx. The import of this is that if Lp is to hold in wx, it must hold also in wy and indeed, in every world accessible to wx. We may then revise rule L-l for MS4 to read:

L-l(4): If La occurs on the left of a tableau t (of LS4 or LS4), write both a and La on the left of each tableau auxiliary to t (unless, of course, a formula to be written is already there).

As an example, let us consider the tableau construction beginning with CLpLLp on its right. An application of C-r gives us Lp left and LLp right; the LLp then causes the application of L-r, generating an auxiliary tableau into which p and Lp are inserted on the left by the new L-l.

Lp       LLp

This last tableau closes, and so the whole construction closes, and by *9.1 CLpLLp is valid in LS4, as will also be LpLLp. Since all the theses of T will be valid in the structure MS4 (which includes MT) and since Lpp will be valid in MS4, which has a reflexive accessibility relation, we assert:


If a formula is provable in S4 (S4), it is valid in MS4 (MS4).

To prove the converse of *14.1, we shall make use of the sequent-logics LS4 and LS4 of the last chapter. Just as in Chapter 9, we shall view each sequent-logic proof string as divided into segments, the first of which begins with an axiom and each following one with an application of L; the L here, however, is that of LS4, which is

D, LG a



LD, LG La  

Suppose now that we have a construction of tableaux beginning with formulas G left and Q right in the main tableau. We then begin to use that construction as a recipe for the writing of a sequent-logic proof just as indicated for MT (MT) tableau constructions in Chapter 9. Let us say that a tableau tx is 'immediately auxiliary' to a tableau ty iff tx was created by an application of L-r in ty itself. The only difference between reconstruction of LT (LT) proofs as in Chapter 9 and LS4 (LS4) proofs as here lies in the way the formulas on the left beginning with L are handled at the L steps which mark the movement from one proof string segment to the next. We shall recall that in an MT (MT) tableau construction, each auxiliary tableau tx is thought of as beginning with a certain number of formulas D on its left and a formula a on its right. The formula a was inserted by L-r from the tableau ty to which tx is auxiliary, and the D come from applications of L-l to the formulas LD standing left in ty. The rule L in LT (LT) infers LD La from D a and permits us to move from the proof string corresponding to tx to that corresponding to ty. The auxiliary tableau tx in an MS4 (MS4) construction, however, will -- in the general case -- be able to be auxiliary to more tableaux than just ty; it is immediately auxiliary to ty, but it is also auxiliary to any tableau to which ty is auxiliary. And the rule L-l(4) for these model structures means that the formulas inserted into tx by applications of L-l will not only be the D, as with MT, but the sequence D, LD, where the LD are all the formulas beginning with L and on the left in all the tableaux to which tx is auxiliary. Where tx had as its initial formulas in MT (MT) D left and a right, in MS4 (MS4) it begins with D, LD left and a right, where L-r in ty (to which tx is immediately auxiliary) inserted the a from La right in ty, and where LD are all and only the formulas beginning with L on the left of ty, regardless of the tableaux in which the various formulas of LD originally occur (that is, the tableaux in which they first caused application of L-l(4)). The sequent beginning the proof string segment corresponding to ty is then LD La; that ending the proof string segment corresponding to tx is D, LG a. When, then, we come to the point (in the construction of an LS4 (LS4) proof on the basis of the recipe given by MS4 (MS4) tableaux) which corresponds to that in the LT (LT) reconstruction from tableaux at which L is applied, we find that we can apply LS4's L as required; the movement from tableau ty to tx in MS4 (MS4) is essentially from the formulas LD left and La right in ty to D, LD left and a right in tx. The inverse of that movement is the movement in LS4 (LS4) by L from D, LG a (the last sequent of the segment corresponding to tx) to LD, LD La, which contracts to LD La, which may be considered the first sequent of the segment corresponding to ty. LS4's L then gives us the inverse of MS4's L-r, and so enables us to extend our 'recipe' for constructing sequent-logic proofs to these systems. We note that LS4 will have just the same relation to MS4 as LT does to MT, and so we shall be able to assert (taking *14.1 into consideration):


A formula is valid in MS4 (MS4) iff it is provable in LS4 (LS4).

By *9.2, then:


MS4 (MS4) provides a decision procedure for S4 (S4).

Tableaux for S3 and S3

The original work on tableaux for S4 appears in Kripke 1963; his formulation there differs somewhat from ours; Kripke 1965a contains a formulation for S3 tableaux; here we present a somewhat different formulation along with one for S3. It will be recalled that the S2 model structure differs from that for T by containing provision for 'non-normal worlds'. The non-normal world is one which behaves normally so far as PC operations are concerned, but which acts as if it had access to the 'impossible possible world', in which every statement would be both true and false, with the result that every statement beginning with an L in a non-normal world is false, while every one beginning with an M is true. Model structures for S3 (S3) will behave like a cross between those for S4 (S4) and those for S2 (S2). The accessibility relation for MS3 (MS3) will be transitive as is that for MS4 (and that for MS3 will also be reflexive), but these model structures will include non-normal worlds just as did those of MS2. MS3 will have, as will MS3, the operations of MPC and the rule for L on the right will be as for MS2:

L-r(2): When La occurs on the right of a (normal) tableau t, split the alternative set to which that tableau belongs; in one of the new alternative sets having a new normal tableau auxiliary to t and beginning with a right, and the other having a non-normal tableau auxiliary to t and beginning with a right.

The rule for L on the left shall be new:

L-l(3): When La occurs on the left of a (normal) tableau t, write both a and La on the left of each normal tableau auxiliary to t (unless, of course, the formula to be written already stands there). Write only a on the left of each non-normal tableau auxiliary to t.

As the last clause of the above indicates, transitivity does not extend to the accessibility relation for non-normal tableaux -- as well it should not. As an example, we test the formula CLLpLLLp; first we apply C-r giving us LLp left and LLLp right:

    LLp       LLLp



Rule L-r dictates that we split the alternative set, as indicated above; the left of the tableaux in the split will take a non-normal and the right a normal auxiliary tableau, each beginning with LLp right:



Lp       LLp
LLp       LLp

As the above diagram shows, we have also carried out the injunction of L-r(3) to insert LLp and Lp left in the normal auxiliary tableau and just Lp left in the non-normal one. The normal auxiliary closes by virtue of having the same formula (LLp) both left and right; the non-normal auxiliary closes as S2 non-normal tableaux can -- by having La, whatever a may be (here a = p), on its left. The whole construction then closes, and CLLpLLLp is valid. Note that if we had started out with CLpLLp instead, the normal auxiliary tableau would close, but the non-normal one would be

p       Lp

which does not close and so gives us a countermodel. As another example, consider the construction which begins with CLCpqLCLpLq on the right of the main tableau. Again, C-r gives us LCpq left and LCLpLq right, and rule L-r(2) instructs us to split

    LCpq       LCLpLq



and begin the non-normal tableau below the split tableau (here on the left) as well as the normal tableau below the other split tableau both with CLpLq on the right. Rule L-l(3) now tells us to put LCpq and Cpq left in the normal tableau and to put Cpq only left in the non-normal one; the rule C-r now tells us to place Lp left and Lq right -- we execute this for the non-normal tableau



Cpq       CLpLq
Lp       Lq
LCpq       CLpLq

We note that the non-normal tableau has Lp on its left and so will close. The normal tableau has LCpq on its left and CLpLq on its right; an examination of the rules for L will show that in this situation they will behave just as do the L rules for MS2, resulting in the closing of the normal tableau (just as an MS2 tableau beginning with LCpq left and CLpLq right will close). The whole construction then closes, meaning that CLCpqLCLpLq is valid in MS3 (MS3). We note that since this formula has as its antecedent beginning with an L, the construction beginning with LCpqLCLpLq will also close. And, as we have indicated, examination of L-l(3) (MS3 al-ready has L-r(2)) will show that any formula valid in MS2 (MS2) will be valid also in MS3 (MS3). Since S2 (S2) plus LCLCpqLCLpLq gives S3 (S3), we have:


If a formula is a thesis of S3 (S3), then it is valid in MS3 (MS3).

As we have done with similar metatheorems, we now set about proving the converse of the above. Once again, we make use of the sequent-logics we have developed. A construction in MS3 (MS3) is like one in MS4 (MS4) except for the alternative splits at the L-r applications and the resulting non-normal tableaux. The differences in the L-l rules for the systems pertain only to non-normal tableaux. The alternative sets which contain only normal tableaux, then, provide us with a recipe for the construction of an LS4 (LS4) proof of the sequent corresponding to the initial state of the tableau construction. But at each L-r in the construction we also have a non-normal tableau, which -- in a closing construction -- must itself close. We wish to show that whenever a closing MS3 (MS3) normal tableau t1 is auxiliary to a tableau t2 and G, LG a is the last sequent of the proof segment corresponding to t1 (making LG La the first sequent of the LS4 (LS4) segment corresponding to t2) we shall be able an the basis of the non-normal tableau generated at the same time as was t1 to show that G LQ, a is provable in LS3 (LS3) and so that LG La is provable by the L of LS3. This non-normal tableau closes, and it closes either by having a formula b on both sides of it, or by having a formula Lg located on its left. Suppose the former. Then we note that by L-l(3) the non-normal tableau will have the formulas G on its left, and by L-r(2), a on its right. Since it closes like an LPC tableau, we shall have G a provable in LPC, and so G LQ, a also so provable.

But then this provides us with a left premiss for LS3's L as required. Suppose now that the non-normal tableau closes by having Lg on its left. This means that the same tableau, if it had Lg on its right also would be a closing LPC tableau. This means further that the sequent G Lg, a is a theorem of LPC and so of LS3. But then let Lg be one of the LQ and G LQ, a is provable; note that the requirements of LS3's L are met in that Lg is indeed a subformula of a or of one of the formulas of G. This all means that if a construction in MS3 (MS3) closes, the LS4 (LS4) proof constructible on the basis of the normal alternative sets of the construction has each of its L steps as a L of LS3 as well, and so is also an LS3 (LS3) proof. By *14.4 and *9.1, then, we have


A formula a is valid in MS3 (MS3) iff a a is provable in LS3 (LS3), and so also iff a is a thesis of S3 (S3).

By *9.2, then


MS3 (MS3) provides a decision procedure for S3 (S3).

Tableaux for S5

The very first of the Lewis modal systems to have a 'possible worlds' semantics provided for it was S5, in Kripke 1957. Our formulation differs somewhat from Kripke's, but it makes use of the fact, as his did, that the accessibility relation in model structures corresponding to S5 is symmetrical as well as transitive and reflexive. We note once more that there is no S5; in Chapter 11 we showed that the addition of MLpLp to S1 makes Lpp and pMp provable. Paralleling this in the model structures of the present section is the obvious fact that if the accessibility relation is transitive and symmetrical and there is any accessible world, then the relation must be reflexive as well. Indeed, in a model in which the accessibility relation has these properties, every world will have access to every world; in a sense there is no one real world in such a model except by arbitrary designation (or, one might prefer to say, by an application of the axiom of choice).

Kripke expressed the transitive-symmetrical nature of the accessibility relation in his tableaux for S5 in terms of true formulas; that is, his L-l rule takes account of the fact that if a formula La is to be true in any S5 possible world, then a must be true in every S5 possible world (because every world has access to every world). The rule L-l would then call for the insertion of a on the left of every tableau of that construction. As an example let us try a construction beginning with CMLpLp on the right of a tableau; C-r first gives us MLp left and Lp right, and N-l then gives us LNLp right (MLp = NLNLp)

MLp       Lp

The rule L-r in the Kripke formulation now calls for us to create two auxiliary tableaux, one beginning with p right and one beginning with NLp right




We have applied N-r in the right one of these two. It is clear that if the above were an MS4 construction, say, that we should have reached the end of the line; it would give us a countermodel to CMLpLp. In an S5 construction like this, however, every tableau is auxiliary to every other, in effect. In particular, we are interested in the accessibility of the tableau beginning with p right to the one beginning with NLp right; rule L-l commands us to write p on the left of the former as a result of the Lp left in the latter:



The result is a closing tableau construction and the validity of CMLpLp. We may call this model structure for S5 as formulated by Kripke MS5. We clearly have, with the above:


If a formula is provable in S5, it is valid in MS5.

We note at this point that if La is false in any MS5 world, then it is false in all. We may then consider that this gives us permission under MS5's L-r to write La right in any MS5 tableau when it occurs right in one. We shall use this later.

We shall find it convenient also to take a somewhat different approach to S5 semantics, an approach which emphasizes the role of falsehood of formulas rather than their truth. What we shall take advantage of is the fact that if a formula La s false in any SS world, then it must be false in every S5 world -- this again is dictated by the mutual accessibility of these worlds. We shall reflect this orientation in a model structure MS5; first of all, the tableau operations of LPC will apply in this structure. The version of L-l will be much like that for LS4, but we shall require a variation in terminology for our statement of it for MS5. We note that in MS5 formulas can be inserted by L-l into a tableau tx from a tableau ty in spite of the fact that tx, while auxiliary to ty, was not 'ancestrally generated' from ty by rule L-r. We shall say that a tableau tx is ancestrally generated from a tableau ty if it is ty or is created by an application of L-r in ty or in a tableau ancestrally generated from ty. We then state:

L-l(5): If La occurs left in a tableau t, write a and La left in every tableau ancestrally generated from t (unless such formulas already occur there).

We also shall employ the following version of L-r:

L-r(5): If the formulas La, LQ are all the formulas beginning with L on the right of a tableau, create an auxiliary tableau beginning with a, LQ on the right.

The a on the right in the new tableau reflects the fact that, as in all these systems, a must be false in some world accessible to the original world. The LQ right in the new tableau reflect the S5  semantic characteristic of 'if not-necessary in one world, then not-necessary in all worlds'. Let us now test the formula CMLpLp in MS5; the original tableau will be just as in the Kripke formulation MS5 above; by our L-r(5), however, we create one auxiliary tableau with NLp and Lp right; an application of N-r then places Lp left in that tableau:

MLp       Lp

Lp       NLp

Our construction then closes. We might also have tried to carry out this construction by creating a new tableau with p and LNLp right; as it turns out, this route gets us nowhere -- which matters not, for the way we did choose results in the contradiction shown in the above tableau construction.

For reasons that will become clear, we shall find it necessary to include in the basis of MS5 a further rule, of a kind different from those we have heretofore considered. This rule involves an alternative split, and is actually a correlate of the sequent-logic rule cut:

  At any time, an MS5 alternative set may be split, with the resulting alternative sets identical except for having a new formula a on the left of one of the tableaux of one of the sets and on the right of the corresponding tableau of the other set.

This rule may be intuitively justified by noting that a will be either true or false in any world, and specifically in the world corresponding to the tableaux in which a was inserted. It is clearly the inverse of cut; we note that where cut eliminates formulas which were introduced in a proof so that they do not appear in the end sequent, this rule adds a formula which did not appear in the original inventory of the main tableau.

It should be clear that all the theses of S4 will be valid in MS5 and that the rules of that system are validity-preserving in that system (the rules of MS4 are included in those of MS5). Since CMLpLp and -- by application of L-r -- MLpLp are valid in MS5, we may then assert:


If a formula is a thesis of S5, it is valid in MS5.

As in the preceding sections of this chapter, we shall prove the converse of the above by means of a sequent-logic, LS5. When we set down LS5 in the last chapter, we noted that the normal-form theorem was not provable for it. This, however, does not prevent its being a useful bridge between S5 and its semantics. We recall that LS5 is like LS4 except for having as its L rule:

D, LG LQ, a



LD, LG LQ, La  

It is clear that this rule bears precisely the same relation to the L-r(5) of MS5 as does the L of LS4 to the L-r of MS4. We note that where the 'cut-like' special rule for MS5 is used in a construction, the rule cut would be employed in the corresponding LS5 proof. With this in mind and altering the proof of *14.2 to refer to the L of LS5 and the rule L-r for MS5 rather than the corresponding rules of LS4 and MS4, we get:


A formula a is valid in MS5 iff a is provable in LS5 and so also iff a is a thesis of S5.

The above result is made possible by the fact that the 'direction of generation' of tableaux in MS5 is antisymmetrical -- formulas are entered into tableaux only from tableaux which are their 'ancestral generators' unlike the procedure in MS5. Tableau constructions in MS5, then, can be placed in correspondence with proofs in LS5, whose direction of generation is also antisymmetrical.

The system MS5 has the advantage of offering us a very easy correlation between the realm of S5 proof and that of S5 models. It does this, as noted, by maintaining an antisymmetrical generation of tableaux. But this antisymmetrical generation is not coincident with the relation of auxiliarity as has been the generation of tableaux in model structures studied up until this point. Thus we reach certain points in which the rules for L in MS5 are inadequate to place formulas in certain tableaux in which they must occur by the auxiliarity relation; as an example, note the construction begun for the formula CMLpp, which is an S5 thesis and so must be valid in MS5

MLp       p

After these preliminaries of applying the LPC C-r and N-l, we use MS5's L-r and then, in the new tableau, N-r:


Since every world in this model structure must have access to every other world, we should be able to write Lp and p left in the upper tableau, for they must, by this accessibility relation, be true in the world corresponding to this tableau. This would result in that tableau's closing. But since the L-l of MS5 operates in the antisymmetrical way noted, we cannot do this. The key to our problem here is the cut-like rule we earlier mentioned as in MS5. We note that Lp and p will have to be true in the world corresponding to the main tableau for creation of a countermodel, and so we must consider what happens in that situation; we then use the cut-like rule to split the construction, writing Lp left (and so making p writable) in the main tableau of one of the alternative sets resulting from the split; and right in the main tableau of the other,

    MLp       p




It will be noted that an application of L-l within the main tableau having Lp left will place p left in that tableau, and so will make that tableau close. The assumption that Lp is true in the main tableau then yields a contradiction. On the other hand, if in the other tableau we let LNLp be the La of MS5's L-r, we generate an auxiliary tableau as follows:


Lp is carried along as the member of LQ; an application of N-r in this auxiliary tableau gives us Lp left as well as right, a closing situation, and the entire construction closes. We then might use the construction as a recipe for the construction of an LS5 proof; the proof that would be so constructed appears almost in its entirety in the last chapter as the proof of the sequent LNLp, p. It is clear that the non-coincidence of ancestral generation and auxiliarity is directly analogous to the non-provability of the normal form theorem in LS5. And we shall find similar correlations in other modal systems in which the auxiliarity relation (accessibility relation) makes necessary different ordering of tableaux (worlds) from that required to obtain between steps in a sequent-logic proof.

The model structure MS5 does not have this drawback. The insertion of formulas from one tableau to another coincides with its auxiliarity relation, and so it comes within the scope of *9.1 without the use of a cut-like rule; further, the absence of such a rule brings it under *9.2 as well, meaning that if S5 is complete with respect to MS5, then MS5 provides a decision procedure for S5. To establish this we shall have to show that:


 If a formula is valid in MS5, then it is valid in MS5.

The problem of proving the above arises when a formula La occurs on the left of an MS5 tableau which is not the main tableau. If no such formula occurs in a construction, we can clearly parallel the construction in MS5, with the latter construction closing when the former does. Suppose that whenever no more than k formulas beginning with L and located on the left occur in an MS5 construction which closes, a closing construction for the original formula for which the construction was begun holds also in MS5. Consider the case in which there are k + l such formulas; note one of these formulas, say La. The main tableau in the MS5 construction must have La and a inserted left in it by rule L-l. Instead of applying this rule to insert La and a into the main tableau, split the alternative set in which the main tableau occurs, placing La left in the main tableau of one of the resulting sets and right in the main tableau of the other. This procedure may be justified by the inclusion of LPC in LS5. By L-l a will also be left in the main tableau having La left; indeed, by this rule La and a may be written left in each tableau of this alternative set. But this alternative set is now like the original in all respects and so closes just as the original did. Since La and a were inserted left in the tableaux of this new alternative set by virtue of an La in the main tableau, however, there are only k applications of L-l needed in tableaux not the main tableau. This set then comes under the induction hypothesis of the main induction, and there is an MS5 closing construction beginning with the same formulas now in the main tableau of this alternative set (that is, beginning with the formulas with which the original construction began, plus La left in the main).

Now consider the alternative set in which La was written right in the main tableau. As we noted (immediately subsequent to the statement of *14.7), the reflexive-transitive-symmetrical property of MS5's accessibility relation means that if La is false in one world, then it is false in all. This means that with La right in the main tableau of this set, it may be written right in any tableau of this set, including the one which originally had on its left the offending La, the one causing the introduction of La and a into the main tableau. This set then closes by having La left and right in that tableau, and it closes without the offending L-l, falling then under the induction hypothesis. But then a closing MS5 construction beginning with the same formula as the original MS5 construction plus La right is constructible, as well as a closing MS5 construction (as shown above) beginning with that same formula plus La left. But then by the cut-like rule of MS5 a closing construction beginning with the same formula as did the original MS5 construction is available, and so *14.10 holds, and we have, by *14.8, *14.9, *14.10, and *9:1:


 A formula a is valid in MS5 iff it is valid in MS5 and so also iff a a is provable in LS5 and so also iff a is a thesis of S5.

By the above and *9.2


MS5 provides a decision procedure for S5.