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 Lr 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 Ll 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 Ll 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 Ll 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 Ll for MS4° to read:
Ll(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 Cr gives us Lp left and LLp right; the LLp then causes the application of Lr, generating an auxiliary tableau into which p and Lp are inserted on the left by the new Ll.


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:
*14.1  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 sequentlogics LS4° and LS4 of the last chapter. Just as in Chapter 9, we shall view each sequentlogic 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 


®L 
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 sequentlogic 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 Lr 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 Lr from the tableau ty to which tx is auxiliary, and the D come from applications of Ll 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 Ll(4) for these model structures means that the formulas inserted into tx by applications of Ll 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 Lr 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 Ll(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 Lr, and so enables us to extend our 'recipe' for constructing sequentlogic 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):
*14.2  A formula is valid in MS4° (MS4) iff it is provable in LS4° (LS4). 
By *9.2, then:
*14.3  MS4° (MS4) provides a decision procedure for S4° (S4). 
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 'nonnormal worlds'. The nonnormal 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 nonnormal 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 nonnormal 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°:
Lr(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 nonnormal tableau auxiliary to t and beginning with a right. 
The rule for L on the left shall be new:
Ll(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 nonnormal tableau auxiliary to t. 
As the last clause of the above indicates, transitivity does not extend to the accessibility relation for nonnormal tableaux  as well it should not. As an example, we test the formula CLLpLLLp; first we apply Cr giving us LLp left and LLLp right:
CLLpLLLp  
LLp  LLLp  

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





As the above diagram shows, we have also carried out the injunction of Lr(3) to insert LLp and Lp left in the normal auxiliary tableau and just Lp left in the nonnormal one. The normal auxiliary closes by virtue of having the same formula (LLp) both left and right; the nonnormal auxiliary closes as S2° nonnormal 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 nonnormal 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, Cr gives us LCpq left and LCLpLq right, and rule Lr(2) instructs us to split
CLCpqLCLpLq  
LCpq  LCLpLq  

and begin the nonnormal 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 Ll(3) now tells us to put LCpq and Cpq left in the normal tableau and to put Cpq only left in the nonnormal one; the rule Cr now tells us to place Lp left and Lq right  we execute this for the nonnormal tableau





We note that the nonnormal 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 Ll(3) (MS3° already has Lr(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:
*14.4  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 sequentlogics we have developed. A construction in MS3° (MS3) is like one in MS4° (MS4) except for the alternative splits at the Lr applications and the resulting nonnormal tableaux. The differences in the Ll rules for the systems pertain only to nonnormal 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 Lr in the construction we also have a nonnormal 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 nonnormal 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 nonnormal 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 Ll(3) the nonnormal tableau will have the formulas G on its left, and by Lr(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 nonnormal 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
*14.5  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
*14.6  MS3° (MS3) provides a decision procedure for S3° (S3). 
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 transitivesymmetrical nature of the accessibility relation in his tableaux for S5 in terms of true formulas; that is, his Ll 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 Ll 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; Cr first gives us MLp left and Lp right, and Nl then gives us LNLp right (MLp = NLNLp)
CMLpLp  
MLp  Lp  
LNLp 
The rule Lr 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 Nr 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 Ll 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:
*14.7  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 Lr 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 Ll 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 Ll 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 Lr. 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 Lr in ty or in a tableau ancestrally generated from ty. We then state:
Ll(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 Lr:
Lr(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 notnecessary in one world, then notnecessary 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 Lr(5), however, we create one auxiliary tableau with NLp and Lp right; an application of Nr then places Lp left in that tableau:


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 sequentlogic 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 validitypreserving in that system (the rules of MS4 are included in those of MS5¢). Since CMLpLp and  by application of Lr  MLpLp are valid in MS5¢, we may then assert:
*14.8  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 sequentlogic, LS5. When we set down LS5 in the last chapter, we noted that the normalform 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 


®L 
LD, LG ® LQ, La 
It is clear that this rule bears precisely the same relation to the Lr(5) of MS5¢ as does the ®L of LS4 to the Lr of MS4. We note that where the 'cutlike' 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 Lr for MS5¢ rather than the corresponding rules of LS4 and MS4, we get:
*14.9  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¢
CMLpp  
MLp  p  
LNLp 
After these preliminaries of applying the LPC Cr and Nl, we use MS5¢'s Lr and then, in the new tableau, Nr:

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 Ll of MS5¢ operates in the antisymmetrical way noted, we cannot do this. The key to our problem here is the cutlike 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 cutlike 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,
CMLpp  
MLp  p  
LNLp  



It will be noted that an application of Ll 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 Lr, we generate an auxiliary tableau as follows:



Lp is carried along as the member of LQ; an application of Nr 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 noncoincidence of ancestral generation and auxiliarity is directly analogous to the nonprovability 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 sequentlogic 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 cutlike 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:
*14.10  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 Ll. 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 Ll 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 Ll 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 reflexivetransitivesymmetrical 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 Ll, 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 cutlike 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:
*14.11  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
*14.12  MS5 provides a decision procedure for S5. 