IN the last decade of the nineteenth century, C. S. Peirce developed an ingenious family of logical systems which he called the 'Existential Graphs'. (Much of the original material on these systems is in volume 4 of the Collected Papers of C. S. Peirce.) Two of the systems in this family, called the 'alpha' and the 'beta.' systems correspond respectively to the classical propositional calculus and to quantification theory (see Zeman 1964, 1967). The graphical formulas of the alpha and beta systems were to be 'scribed' upon what Peirce called the 'sheet of assertion'. This sheet of assertion, Peirce informs us, is to be thought of as representing the actual existent universe; the graphical formulas written upon that sheet then represent statements true in that universe. But Peirce had no intention of limiting his logical work to the 'actual existent world'. That which is possible is too important a part of the real for Peirce to ignore; indeed, his desire to account for the logic of the possible may well be a chief motivation leading him to adopt the existential graphs as the format for his logic. The system which Peirce calls 'gamma' is essentially a modal system, and in it we begin to employ not just one sheet of assertion, but a book of such sheets. Just as the sheet of the alpha and beta systems represents' the actual existent world, each of the sheets in the gamma book represents a possible world (one of which is the actual existent world). Peirce's gamma system is then an attempt to set up the logic of possibility, of 'possible worlds'. Unfortunately, Peirce was unable to articulate the mechanism of such a logic, and his gamma system remained an unfulfilled bright idea.

As we have noted, Peirce attempted to formulate the logic of possible worlds by associating with each possible world a unique graphical sheet of assertion upon which would be executed the logical calculations for that world. Kripke's approach is quite similar; however, he associates with each possible world a semantic tableau à la Beth 1955. Kripke's tableaux operate just as do ours of Chapter 4 so far as the connectives of PC are concerned. In addition he introduces rules telling what to do when modal operators appear on the right or left of a tableau. These rules will ordinarily involve tableaux other than the one in which the modal operator occurs, and their specific effects will depend upon the properties of the accessibility relation in the model structure within which we are working. In what follows we study the behaviour of Kripke-style models and tableaux.

Tableaux for modal systems

In Chapter 4 we discussed notions of validity for PC; we showed how validity may be checked by semantic tableaux, and we used the tableaux in a proof of completeness for the system PC. The check for validity was accomplished by attempting to falsify the formula involved; we saw that a formula fails to be falsifiable (that is, is valid) iff the tableau construction executed for it closes. If a given assignment of truth values to the variables of a formula causes the formula to be true, we may say that that assignment provides a model for that formula. On the other hand, if an assignment causes a formula to come out false, that assignment provides a countermodel for the formula. A PC formula, then, is valid-that is, tautologous -- iff we can construct no countermodel to it in the two-valued truth value system; this we have seen is the case iff the tableau construction begun for that formula closes. We shall now extend these notions to the modal systems with which we are now working.

Lp now appears right, and we must, as we have said, assume that there is a possible world in which p is false, which world is accessible to ours. Since we are trying as hard as we can to falsify p in this new world (w2), we initially assume nothing more about w2 than that p is false there. We thus keep track of this step in the attempted construction by beginning a new tableau (call it t2 to correspond to w2; the original tableau may be called t1); we write the formula p on the right of this tableau to indicate that p is to be falsified in world w2:

t1		t2
CpLp p       Lp		p

Note that tableau t2, which represents world w2, has an entirely different status than would a new tableau created by an alternative split of t1 due to an application of C-l, K-r, or A-l. Tableaux created by this kind of split each go off their own way with no further interaction after the split. Tableau t2 above is intimately associated with t1, however, in that discovering whether or not we can make the assignments needed to establish the existence of a countermodel involving wl depends on what happens in w2. Tableau t2, then, stands in an auxiliary position to t1; indeed, we shall call the tableau corresponding to the real world the main tableau, and tableaux created as was t2 will be called auxiliary tableaux. Note that if the formula Lb were to stand on the right of any auxiliary tableau, we should follow the same procedure as above and create a new tableau (representing a world to which the auxiliary tableau has access) auxiliary in turn to the original auxiliary tableau and beginning with p on its right. As tableaux correspond to possible worlds, then, the relation of auxiliarity corresponds to the accessibility relation among worlds. We note that in the case of the example given above, by the way, that we do find a countermodel for CpLp by allowing p to be true in the real world (it is left in tableau t1) and false in a world to which wl has access (it is right in t2). No contradiction (closing tableau) arises from these assumptions, and so a countermodel has been found. In the diagrams, the arrow indicates the auxiliarity relation. We may now state a general rule for tableaux constructed for modal formulas:

Let us now suppose that in a tableau construction we have been working with we come to a stage at which we have La on the left of a tableau, say t1 Since our tableaux are keeping track of our attempt to create a countermodel, this means that in world w1 La must be true. This further means that in any world to which w1 has access, a must be true. If we suppose the accessibility relation to be reflexive, this means that we must write a at least in the left column of t1 itself. And if there are any tableaux auxiliary to t1, we must write a in the left column of each of them to show that the countermodel requires that « be true in the worlds represented by those tableaux. Thus we have as a general rule:

In the discussion of the L rules above, we have, for simplicity, confined ourselves to cases in which the rules C-l, K-r, and A-l are not used. When these rules are employed in a PC tableau construction, they cause a tableau to split into alternative tableaux, each of which gives us an extra chance of falsifying the PC formula in question, a chance of finding a countermodel. When one of these rules is used in a modal construction, we have a similar though more complicated situation. The tableau in which the rule is applied does indeed split just as a PC tableau splits. But it may not be alone in splitting. It may be a tableau auxiliary to another tableau or having another tableau auxiliary to it. Let t1 be a main tableau, and let t1 . . . tn be the n tableaux bearing the ancestral of the relation 'auxiliary to' t1. Let ti, 1 £ i £ n, be a tableau in which a rule such as C-l, K-r, or A-l has been applied, causing an alternative split. Split ti as usual into two tableaux, ti¢ and ti². But also split the rest of the set as well, duplicating the tableaux other than ti; we now have two sets of tableaux, t1 . . .ti¢  . . . tn and t1 . . .ti²  . . . tn, differing only in the tableaux ti¢ and ti². ti¢ and ti² will bear precisely the same relations to the members of their respective sets as did ti. Where splitting with PC tableaux produced alternative tableaux, splitting with modal tableaux will produce alternative sets of tableaux. Each of these alternative sets offers a separate chance to create a countermodel for the formula for which the tableau construction was begun.

First of all, it is clear that -- since we take the rules for PC connectives of Chapter 4 as part of all of our systems -- if a wff is a thesis of PC, then the tableau construction begun for it closes; tableau analogues of the PC rules of inference also will hold. Let us now suppose that a tableau construction begun with the formula La closes. The main tableau of this construction will contain at all times only La on its right (the only rule that can be applied within that tableau is L-r, which creates a new tableau); the construction then begins

La

a

Since the main tableau never contains more than La and its only 'connection' to the rest of the construction is through the auxiliary tableau (with a right) shown above, the tableau beginning with a on its right must close for the whole construction to close; we then conclude that if La is valid, so too is a; we then have in MT° an analogue of T°'s rule RLE (If La, then a).

Look again at the above diagram, but this time let us assume that the formula a is valid. Here the tableau construction beginning with a at the right of the main tableau closes; examine then the status of a construction beginning with La; it is clear that such a construction will begin just as does our above example; since a is valid, then, the construction for La will close, and we may assert that if a is valid, so too is La, and we have an analogue of T°'s rule RL (If a, then La).

Let us now examine the status of the tableau construction beginning with the formula CLCpqCLpLq on its right. The first two rule applications in this construction will be C-r, giving us:

				CLCpqCLpLq
LCpq				CLpLq
Lp				Lq

We have now gone as far in the main tableau as we can. Note that if the accessibility relation were reflexive, we should (by rule L-l) have to write Cpq and p on the left of this tableau; since this relation is not specified as reflexive, however, we do not do this. In not investigating the cases in which this relation is reflexive (or transitive, or symmetrical, etc.) we are being more rather than less general; the more properties we assume for this relation, the more formulas will be entered into the construction, and so the greater will be our chance of the construction's closing. By assuming fewer properties, then, we validate fewer formulas. We now look at the Lq right in this tableau. By L-r, we must construct an auxiliary tableau beginning with q right; rule L-l then has us enter Cpq and p on the left there:

CLCpqCLpLq LCpq       CLpLq Lp       Lq

Cpq       q p

The Cpq on the left in our auxiliary tableau forces an application of rule C-l:

CLCpqCLpLq LCpq       CLpLq Lp       Lq

Cpq       q     p             p q

Although we have shown only the auxiliary tableau explicitly as splitting, we have, of course, split the entire construction into two alternative sets -- each containing two tableaux (a main and an auxiliary) and each closing. Thus the construction beginning with CLCpqCLpLq closes, and so that formula is valid in MT°. That formula may be considered the proper axiom of system T°; since all PC theses are valid in this model structure and all the rules of inference of T° have analogues in MT° (validity in that structure is inherent through them), this means that:

*9.3	If a is a thesis of T° (T), then it is valid in MT° (MT). Note that MT is like MT° except that the accessibility relation is reflexive; CLpp is easily seen to be valid given this condition.

Let us quickly now take a look at a formula which is not provable in T°. Specifically, this is the formula CLpp. Tableau constructions beginning with this formula are kept from closing by a principle based on a suggestion of Kripke 1963, p. 95. There he indicates that by omitting the property of reflexivity from the accessibility relation (as we have been doing) we also keep constructions for CLpp and its consequences from closing. Our approach here is based on this suggestion, but is more thorough in its application than is indicated by Kripke. He suggests that when we omit the property of reflexivity, we specify further that every world will have some world accessible to it. Thus, when we come to a situation like a tableau beginning with CLpp, where the main tableau will have L on the left but not on the right, we must create an auxiliary tableau, even though there is no L on the right:

CLpp Lp       p

p

The p to the left in the auxiliary tableau is, of course, due to the Lp on the left in the main tableau. Here a falsifying assignment is found, with p false in the main world and true in all others; since the real world is assumed not to have access to itself, Lp is then true in it, and the countermodel has been found. But Kripke's suggestion will not do as it stands for the 'nought' systems. Note the formula CLpMp which does not hold in T°:

CLpMp Lp       Mp (i.e., NLNp) LNp

We have carried the PC operations as far as we can; our modal formulas are two beginning with L on the left; assuming that there is a world accessible to the one represented above, both p and Np must be entered left in that world's tableau:

p         Np       p

As indicated, with an application of N-l that tableau closes. With the assumption that there is a world accessible to each world, then, we have CLpMp valid. This assumption, then, will not do for T° or our other nought systems. We propose to modify Kripke's suggestion by making no assumption at all about the availability of accessible worlds. Given this approach, each of the above constructions would fail to close by the simple fact that La would be assumed to come out true always in a world which has no worlds accessible to it. But is this not an arbitrary assumption? Hardly -- it is soundly based in logic. We have commented that the necessity operator behaves like a universal quantifier, quantifying over possible worlds. Indeed, we may follow Prior 1964 and come up with a quantificational analysis of modal operators from the 'possible worlds point of view'. We shall take ordinary quantification theory to be part of our metalanguage here, and we shall make use in it of two special predicates. One of these is a relation between the objects that we have been calling worlds; it is written Uxy and will be thought of as being true iff world x has access to world y. The other is a relation between worlds and statements; it is written Txa and is true iff a is true in world x. It is clear that, given our semantic definitions of modal operators, TxLa will be a true statement iff (y)(Uxy É Tya) holds. But this last assertion says nothing at all about the existence of a world accessible to x; it merely asserts that if such a world exists, then a holds in it. If indeed no such world exists, then the antecedent of (y)(Uxy É Tya) is false, and the statement holds, much like a categorical A statement in the syllogistic taken without existential import. Thus we are justified in claiming that, when the accessibility relation is not reflexive, if La occurs on the left of a tableau with no tableaux auxiliary to it, nothing further is to be done to it; its presence there is self justifying. So the tableau constructed for CLpMp would end at the stage

				CLpMp
Lp				Mp (i.e., NLNp)
LNp

At this stage, the only formulas in the tableau which have not occasioned rule applications are the Lp and LNp on the left; with no world accessible to the world in question, both of these formulas receive the assignment true, as required for the countermodel. Consider on the other hand a formula La located on the right of a tableau in MT°. For this to be justified, the statement ~TxLa must hold, where x is the world in question. But this will hold iff the negation of (y)(Uxy É Tya) holds; this formula is (3y)(Uxy.~Tya). This statement is analogous to the O statement in the syllogistic, and, unlike the statement analogous to the A statement, it asserts that a world accessible to x exists; thus, when L occurs on the right in a tableau, an auxiliary tableau must be constructed. We may note in passing that our treatment of tableaux for the nought systems resembles the syllogistic without existential import, while Kripke's suggestion would give us something with existential import, with a 'valid principle of subaltemation' (CLpMp).

Our next project is proving the converse of *9.3. We shall do this by extending the PC completeness proof of Chapter 4 to the modal systems we have been studying. As that proof makes use of the sequent-logic LPC, we shall here make use of the sequent-logics of the last chapter. In Chapter 4 we correlated tableaux with proof strings of the system LPC and noted that the rules for tableaux so considered (as proof tableaux rather than semantic tableaux) were the same as those for tableaux considered as semantic tableaux; it turned out then that we could use a closing construction of semantic tableau as a 'recipe' for constructing an LPC proof for the sequent for which the construction of tableaux closed. Our approach here will be much the same; in this case, however, tableaux in general will not represent whole proof strings, but rather portions of proof strings of a proof in the sequent logic LT° (or LT). An entire proof string from axiom to end sequent will correspond to a whole alternative set of tableaux in a construction. We shall consider the LT° (LT) proof string to be divided at certain points; specifically, where the rule ®L is employed. We may consider the portion of a proof string from the axiom to the premiss of the first ®L the initial segment of that proof string; the portions from the conclusion of one ®L to the premiss of the next are then intermediate segments, and the portion from the conclusion of the last ®L to the end sequent is the final segment. Each such segment then corresponds to a tableau, auxiliary or main (the final segment to the main tableau, and the initial segment to the tableau in which the construction of the alternative set was terminated by virtue of one formula's being both left and right (call this the terminal tableau)). We may use a closing construction of MT° (MT) tableaux to construct a proof in LT° (LT) as follows; we shall use the construction carried out above for CLCpqCLpLq as an example. The construction will contain a number of alternative sets (in our case, two) each of them closing; each will then have a terminal tableau with a formula bi (for the ith such alternative set) occurring both left and right in it. Where there were n such alternative sets, the proof in which we are interested will contain n proof strings, and so n 'branch tips'. Corresponding to the ith alternative set of tableaux we shall write the axiom sequent bi ® bi. In our example the two such sequents are p ® p and q ® q. Construction of the initial segments of the proof strings from the terminal tableaux is a matter of PC rules (in the case of MT tableaux, it may also involve the use of L®, which corresponds to rule L-l as the PC tableau rules do to their sequent-logic counterparts, and which behaves just as would a PC rule); the reader may refer to Chapter 4 for details on constructing LPC proofs from MPC tableaux. Based, then, on the terminal tableaux of our construction, we write our two axioms and then insert p into the antecedent of q ® q and q into the succedent of p ® p by weakening to correspond to the upper occurrences of p and q in the respective tableaux; we then perform C® to correspond to the C-l:

We now have the initial segments of both proof strings in the proof to be constructed according to our tableaux. We note again that in a proof corresponding to an MT construction, applications of L® may occur within a segment of a proof such as above. ®L, however, will not so occur, either in a proof corresponding to an MT or to an MT° construction. This rule represents the movement from a tableau to the tableau to which the first is auxiliary. The end sequent of a segment of proof will represent the formulas inserted into that auxiliary tableau from the tableaux to which it is auxiliary. Where G ® q is that end sequent, Lq is the formula which by application of L-r led to the initial establishment of the auxiliary tableau; the LG are formulas inserted by applications of L-l in the tableau in which the Lq occurs. In our case Lq is Lq and the LG are LCpq and Lp. We shall note that in the general case we must talk of the formulas in LP as being distributed through the tableaux to which the tableau containing q right initially is auxiliary. In the case of MT° and MT, however, where the accessibility relation has at most the specified property of reflexivity, we shall be entitled to claim that tableau t1 (with t1 ¹ t2) is auxiliary to tableau t2 only if t1 was originally constructed as a result of an application of L-r in t2. Thus if a formula is inserted left in t1 as a result of an application of L-l other than in t l, for MT° and MT we must consider that application to have been in t2, the only tableau (other than itself, in MT) to which t1 is known to be auxiliary. All the formulas in the LG mentioned above, then, are considered to be in the tableau having Lq right; G ® q is then the sequent representing the 'initial state' of the auxiliary tableau, and an application of ®L to that sequent gives us LG ® Lq, which represents the 'final state' of the tableau to which the first is auxiliary; in our example, this is

We have thus developed a proof for the formula for which our tableau construction was begun. We note that given any closing construction of MT° (MT) tableaux, we could put together a corresponding LT° (LT) proof as above. The terminal tableaux give us our starting-points for the proof as a whole; the operations performed within any tableau give us the LPC steps (LPC + L® for MT) situated within the segments of our proof strings; the formulas inserted into a tableau by L-r and L-l rules from above correspond to the formulas in the last sequent of an initial or intermediate proof string segment; the formulas in a tableau which caused applications of L-rules correspond to the first sequent of an intermediate or a final segment. Suppose tableau t2 is in a closing alternative set and is auxiliary to tl. t2 then has certain formulas G left and q right which resulted from applications of L-rules in t1 LG are then left in t1 and Lq is right. The sequent corresponding to the final state of t1 (the point at which no further PC operations could be performed) is then LG ® Lq and that corresponding to the initial state of t2 (before any PC operations were performed there) is G ® q. The formulas in G were all and only those inserted in t2 by L-l from t1 because the accessibility relation has no specified properties; t2 is thus auxiliary to t1 and only to t1 (this also holds for MT where this relation has only reflexivity as a specified property). The movement from tableau t1 to t2 is then the inverse of MT°'s rule ®L, and any closing construction of MT° tableaux will then enable us to put together an LT° proof as above. Note that the rule ®L performs all L insertions, both those corresponding to the tableau rule L-r and to the tableau rule L-l. This is not the case in the construction of a proof corresponding to an. MT tableau construction. Here L-l applies to the tableau t1 as well as t2, and so the final state of t1 has the formulas G left as well as LG. When putting together an LT proof from an MT construction, then, after performing the ®L as noted above, insert the formulas G by weakening to get the sequent G, LG ® Lq; where L-l was applied in t1 for a formula Lg we apply L® to g in the segment of proof corresponding to t1; this gives us two instances of Lg in the sequent resulting from the L®, one of which is removed by contraction. This last applies, of course, only to tableaux t1 which are not terminal tableaux; in the case of terminal tableaux the rule L® will be used directly as the inverse of L-l, exactly as LPC rules are used as the inverses of MPC rules. In the case of either an MT° or an MT tableau construction which closes, then, we shall by appropriately altering the techniques of Chapter 4 be able to put together an LT° or LT proof, respectively, for the formula for which the tableau construction was begun (more properly, for the sequent ® a, where a was that formula). By the above considerations, then, along with *9.1 and *9.3 we have:

The ordinary and the sequent-logic versions of S2° and S2 differ from those of T° and T in that in them certain restrictions are placed upon the prefixing of L to certain formulas; these restrictions are expressed in S2°'s version of the rule RL and in LS2°'s ®L. The model structures and tableaux we establish for S2 and S2° will reflect these restrictions. Kripke 1965a extends the models of Kripke 1963 to cover systems which he calls 'non-normal'; among these systems is S2. The S2 models differ from the T models in that they can contain a new kind of world, which Kripke refers to as a 'non-normal world'. In contrast, as one might expect, the worlds of T are 'normal'. The PC connectives behave in non-normal worlds precisely as they do in normal ones; the difference comes in the behaviour of the modal operators. In fact, in a non-normal world for S2° or S2 the statement La will always be false; as a consequence, any statement beginning with M will always be true. Kripke explains this by saying that the non-normal world has access to no world, even to itself. He refers to the accessibility relation for S2 as being 'quasi-reflexive'; with such a property, a world is said to have access to itself iff it has access to some other world; a non-normal world is said, then, to have access to no other world and so not to itself. As we have noted, however, it seems logically more appropriate to hold that in a world with access to no worlds, the statement La will always be true rather than false. We shall then view non-normal worlds not as having access to no worlds, but, perhaps, as being 'over-sceptical' as to the truth of necessary statements, regardless of the worlds accessible to them. As a matter of fact, S2 non-normal worlds behave as if they had access to a very special world, one in which every statement can be falsified (thus making La always false in the non-normal world). But this very special world would be very special indeed, for if we can assert the falsity of every statement, we shall be able to assert the truth of them all as well (thus making Ma always true in the nonnormal world). Such a very special world would be, of course, a world of contradiction, a completely inconsistent world (the impossible possible world!), and so we hesitate to accord it a place of honour (or any place) in our models. If we may continue being fanciful, we might suggest that the information-gathering devices in a non-normal world are in need of repair, and that they merely think that they have access to an inconsistent world. Whatever we may say about non-normal worlds, we must agree, I think, that 'nonnormal' is an appropriate term to apply to them. In S2 and S2° nonnormal worlds, then, every statement beginning with an L is always false, and every one beginning with an M is always true. Note that we need not here employ the notion of quasi-reflexivity; the properties of the accessibility relation will be the same for S2 and S2° as for T and T° respectively.

The formulation of T° (T) of Chapter 7 may be changed to the formulation of S2° (S2) of that chapter simply by weakening the rule RL (which infers a thesis La from a thesis a) to

We wish to show that this rule preserves validity in MS2° and MS2; thus we assume that a as in this rule is valid. Consider, now, La. If such an La is written right in a tableau, by rule L-r(2) we must split the alternative set and create two new tableaux, one of which is normal, the other non-normal, each starting with a on the right. By hypothesis, the formula a is valid, and so the new alternative set containing the normal tableau with a right closes. We consider, therefore, the alternative set containing the non-normal tableau. First of all, a may be a PC theorem. In this case a tableau beginning with a right will close by the MPC rules alone; since these rules operate in non-normal tableaux just as they do in normal, this means that a non-normal tableau so beginning will close, and so in this case the whole construction beginning with La closes, and La is valid. Secondly, a may be of form CLbg. In this case, the non-normal tableau begins with CLbg; an application of C-r then places g right and Lb left. But whenever a formula beginning with L appears left in a non-normal tableau, that tableau closes and La (LCLbg) is then valid. The other postulates of S2° and S2 are the axioms and rules of the PC, the axiom CLCpqCLpLq, and -- for S2 -- the axiom CLpp. With the exception of CLCpqCLpLq, to show that these axioms are valid and that the rules are validity-preserving in MS2° (MS2) is exactly the same as to show this in MT° (MT), since except for CLCpqCLpLq and RL2 no use of MS2°'s rule L-r(2) is required. As we have seen, RL2 is validity-preserving in the presence of L-r(2). So far as CLCpqCLpLq is concerned, we need only note that the non-normal tableau arising in the MS2° construction for this formula will begin with q on the right (reference to our earlier MT° example involving this formula shows that the main tableau in the construction after two C-r's has Lq on the right) and will by L-l receive Cpq and p on the left. It will then close as a PC tableau, and the MS2° construction as a whole will close. We thus conclude that *9.6 holds.

We turn now to the converse of *9.6. We wish to show that when a construction in MS2° (MS2) beginning with a tableau initially having formulas G left and Q right closes, a proof in LS2° (LS2) for G ® Q may be constructed. We note that each alternative set in such a construction will involve a certain number of tableaux; let the largest alternative set in the construction be of length n +1, n ³ 0; n is then the number of applications of L-r(2) used in constructing that set. Suppose now that when we have a closing construction beginning with G left and Q right in MS2° (MS2) for which n £ k, then a proof in LS2° (LS2) can be constructed for G ® Q. Consider now such a construction of length k + 1. The main tableau of each alternative set of this construction will have auxiliary to it no tableau or a tableau the initial formulas (the formulas inserted into it from the main tableau) of which are a set D on the left and a formula l on the right. If no tableau is auxiliary to the main tableau, then the main tableau itself closes by having a formula both left and right in it (this may be considered the base case of the induction). If a tableau beginning with D left and l right is auxiliary to the main tableau, then that tableau itself begins a closing MS2° (MS2) tableau construction for which n £ k; by the induction hypothesis, D ® l is then provable in LS2° (LS2). Auxiliary to the main tableau is also a non-normal tableau having D left and l right as initial formulas. By hypothesis, this tableau closes. If it closes as a result of having a formula (not beginning with an L) both left and right in it, then only PC rules have been used in it; the normal tableau paralleling it begins with the same formulas and so has the same rule applications, with identical results -- it too closes. It is then a terminal tableau, and no ®L has been employed in the proof in LS2° (LS2) of D ® l, and so this rule may be used to give LD ® Ll as provable. Suppose now that the non-normal tableau closes as a result of having a formula La on its left side. La will then also occur on the left of the normal auxiliary tableau beginning with D left and l right. Examine then the proof string segment corresponding to this tableau. In it there will be a sequent La, P ® S. Suppose that the proof of this sequent requires applications of ®L with empty antecedent; such steps are of form

® d
	®L
® Ld

There can be, of course, no applications of ®L between such steps and the sequent La, P ® S. Replace the above step by

® d WK a ® d
	®L
La ® Ld

Now carry out the rest of the proof as before, with La as a parametric formula. Where the original proof has the sequent La, P ® S the new proof has La, La, P ® S; we now eliminate one of the La by contraction. Since each proof string in the original proof of La, P ® S contained at most one ®L with empty antecedent and we have showed how to eliminate those, we conclude that this sequent is provable without the use of such rules. Since this sequent is in the same segment of proof string as is D ® l, then, no occurrences of ®L intervene between these sequents, and D ® l is then provable without the use of ®L with empty antecedent. ®L may then be applied to it in LS2° (LS2) to get LD ® Ll, which is then provable whenever the non-normal tableau auxiliary to the main tableau closes, whether that closing be by PC means or by having an La left. But this sequent will serve as the first sequent of the final proof-string segment in a proof of the sequent corresponding to the initial state of the whole construction, that is, G ® Q. This segment is generated by LPC rules (and L® in LS2) appropriately applied as indicated by the MS2° (MS2) rules used to place wffs within the main tableau (these do not include L-r(2)). The provability of G ® Q in LS2° (LS2), then, follows from that of LD ® Ll. Thus we also have it that if a tableau starts out with just a formula b right and the resulting construction closes in MS2° (MS2), then ® b is provable in LS2° (LS2). We have, then, basically by *9.1 and *9.6 along with the above:

*9.7	A formula b is valid in MS2° (MS2) iff ® b is a theorem of LS2° (LS2), and so iff b is a theorem of S2° (S2).

By *9.2, then, we get

*9.8	MS2° (MS2) provides a decision procedure for S2° (S2).

Tableaux for S1° and S1

The systems S1° and S1 might seem, at least in the Lewis formulations, to be simpler than any of the other systems we have been studying; after all, the other systems are formed by the addition of postulates to S1° or S1. This, however, is evidently untrue, as is illustrated in the sequent-logic and the PC based formulations of Sl° and S1 and in the absence of the semisubstitutivity of strict implication in these systems. In fact, it is only quite recently that semantics and decision procedures analogous to those we have discussed for the other Lewis modal systems have been discovered (the sequent-logics of the present book and the algebraic systems of Shukla 1970 and Cresswell 1969; K. Fine, in unpublished work, has given Henkin-type completeness proofs for these systems). We shall begin by working generally with the semantic methods of Cresswell 1969. We shall consider a model structure MS1°; like MS2° this structure will have in it non-normal worlds which differ from those worlds of MT°, but also from the non-normal worlds of MS2°. Once again we find it more appropriate to consider the non-normal worlds capable of having access to certain worlds; we shall note however, that the accessibility relation here differs somewhat from that appropriate to normal worlds. The model structures we have been heretofore examining may be thought of as consisting of a set of elements E with one member of the set 'designated'; this set we have referred to as the set of possible worlds and the designated world is the 'real world'. Also, we have in these systems a relation U defined on E; this we have called the accessibility relation. For MS1° and MS1 we shall need an additional set of elements; call this set S, and think of S and E as being disjoint. The relation U for MS1° and MS1 will be three-place, and will be written Utxy, where x, y Î E and t Î S. An intuitive interpretation of S might be to think of it as being the 'set of all instants of time'; Utxy would then be read 'x has access to y at time t' We keep our predicate T as before; Txa is read `a is true in x'; this is independent of members of the set S. We need not view the members of the set S as instants of time, of course; we need only think of E and S together as providing the material for our set of elements for these structures. The elements here are simply ordered pairs whose first members are from S and second members from E; in the language of possible worlds, then, each element would be a 'world-instant'. TxLa, then, would be (t)(y)(Utxy É Tya), when x is a normal world; the simple assertion of La would hold when TxLa and x happens to be the 'real world'.

As might be expected, the behaviour of the modal operators in non-normal worlds differs from that described above. Necessity in one of these worlds is 'weaker' as well as 'stranger' than necessity in a normal world; the weakness comes because TxLa will require for non-normal x not the universal quantification for t above, but rather, that ($t)(y)(Utxy É Tya). The strangeness comes because in addition, TxLa for non-normal x will require that there be a certain world in which a must be false. All in all, we say that TxLa for non-normal x iff ($t)(y)(Utxy É Tya) . ($y)TxNa. This is to say that in a non-normal world x a statement is 'necessary' iff at some instant it holds in all worlds accessible to x at that instant, and that further, there is some world which at that instant has a as false; this holds regardless of whether the statement holds in worlds accessible to the non-normal world at other instants of time. So far so good, but as we shall see, the accessibility relation for non-normal worlds in these structures has another rather unusual property. Let us first consider a relation which we shall designate s. This relation will be defined in terms of the accessibility relation for non-normal worlds; it is a relation between non-normal worlds and sets of worlds; sxa will mean that the (non-normal) world x bears this relation to the set of worlds a. sxa iff ($t)(y)(y Î a É ~ Utxy). ($y)(y Î a). a then is a set of worlds (non-empty) which at some time is completely excluded from access by x. Cresswell 1969 sets this relation as primitive and does not make use of the notion of accessibility as we have done. He uses the relation as part of his definition for non-normal necessity for S1. The whole of the definition for non-normal necessity in MS1° may be expressed in terms of this relation. In Cresswell's terms, La will be true in an MS1° non-normal world x iff sx(w | TwNa). Now, by our definition of L in a non-normal world x, we have:

9.1

TxLa º ($t)(y)(Utxy É Tya) . ($y)TyNa

By PC methods, then, we get

9.2

TxLa º ($t)(y)(~Tya É ~Utxy) . ($y)TyNa

By the nature of the predicate T we have ~Tya iff TyNa iff y Π (w | TwNa); so:

9.3

TxLa º ($t)(y)(y Π (w | TwNa) É ~Utxy) . ($y)(y Π (w | TwNa))

By our definition of s this means

9.4

TxLa º sx(w | TwNa)

So our method of interpreting L for non-normal worlds in MS1° corresponds to that derived from Cresswell 1969. But as it turns out, this relation s  for MS1° has an unusual property. Suppose that a world x is such that, for sets of worlds a and b, sxa and sxb. Then, Cresswell tells us, a and b are not disjoint, i.e.

9.5

sxa . sxb . É a Ç b ¹ Æ

Expanded into terms of U and transposed, this is equivalent to

9.6

a Ç b = Æ É  ((t)($y)(y Î a .Utxy) Ú (t)($y)(y Î b .Utxy) Ú (y)(y Ï a) Ú (y)(y Ï b))

If, then, a and b are disjoint sets of worlds, every non-normal world will always have access to some member of a, or to some member of b, or one or both of a and b are empty. Whether expressed in terms of U or of s, this condition has an unnatural and ad hoc feel about it; this semantics for S1° and S1 illustrates again, I think, the 'pathological' nature of these systems.

As was the case with the other model structures of this chapter, we shall investigate validity in MS1° and MS1 by means of tableaux. Again, we shall begin a non-normal tableau as well as a normal one when we apply the rule for L on the right of a tableau; this rule is the same as that for MS2° (i.e. it is L-r(2)). In MS1, as one might expect, the accessibility relation is reflexive (both for normal and non-normal worlds) and so the rule L-l for MS1 tableaux will call for the placement of a left in tableaux in which La occurs left. The condition for La to be true in a non-normal MS1 world, then, includes what is expressed, say, in 9.4, and demands as well that a be true in that non-normal world. Let us now show that

*9.9	If a formula is a thesis of S1° (S1), it is valid in MS1° (MS1).

S1° is like S2° except for its version of the rule RL and its having postulated the rule BKW. The rule RL1 for S1° is:

RL1:	If a, then La, provided either
	(a) a is a PC thesis, or
	(b) a is  of form CKLbLgd where LAbg;

For S1 the rule is extended by the clause:

or, (c) a is  of form CLbb; this clause applies to S1 only.

The rule BKW is

BKW:	If both ab and ba, then LaLb.

In checking the axioms and the other rules of inference in S1° (S1), we find that any non-normal tableaux occurring in MS1° (MSl) models for these axioms and rules will close as they do for MS2° (MS2) (indeed, they are the same as the models constructed in the latter systems for the same cases); they will close as PC tableaux, with a given formula occurring both left and right in them; they do not then require any evaluation procedures for formulas in them beginning with L. The axioms of S1° (S1) are then MS1° (MS1) valid, and the rules of inference other than RL1 and BKW are validity-preserving. We must then check on the validity-preserving status of RL1 and BKW. First, consider BKW. We assume that LCab and LCba are both valid, that is, that Cab and its converse hold in every world accessible to the real world. It is clear that with LCab holding, LCLaLb will be such that the normal tableaux constructed for it will close; we turn then to the non-normal tableau created by the application of L-r(2) for the above formula. This tableau has CLaLb on its right, and after an application of C-r it becomes:

				CLaLb
La				Lb

If the above situation can apply without contradiction, i.e. without this tableau closing in MS1°, then both of the following statements must hold (taking the world represented by this non-normal tableau as x):

9.7

($t)(y)(Utxy É Tya) . ($y)~Tya

corresponding to the La left and

9.8

(t)($y)(Utxy . ~Tyb) Ú (y)Tyb

By hypothesis, the constructions begun for LCab and its converse close, meaning that these formulas hold in the real world and indeed in any normal world; Cab will then hold in each world accessible to a normal world; with our domain as the non-normal worlds, then, we have

9.9

(y)(Tya º Tyb)

But in the presence of 9.9, 9.8 becomes

9.10

(t)($y)(Utxy . ~Tya) Ú (y)Tya

This last formula is, of course, equivalent to the negation of 9.7; the tableau attempted above, then, cannot be constructed, and an analogue of BKW holds in MS1°. In MS1 we have the additional requirement of reflexivity for the accessibility relation; thus a must be written left in the MS1 version of the above tableau; by the strict equivalence of a and b, b must also be written left there. This means that for Lb to be false in that world, the condition expressed by 9.8 must again apply, along with that expressed by 9.7. Again, then, we have an impossible situation, the tableau may be said to close, and an analogue of BKW holds in MS1.

We now turn to the status of rule RL1 in these systems. First of all, if a is a PC thesis and a construction is begun for La, the non-normal tableau begun for that construction will start with a right, and so will close by the MPC rules; La will then be valid in MS1° (MS1). Now turn to clause (c) of this rule (which applies for S1), where a is a thesis of form CLbb. Since the accessibility relation is reflexive in MS1, b must be written left in any tableau in which Lb is left; a construction beginning with LCLbb will have Lb left and b right in both the normal and the non-normal tableaux immediately auxiliary to the main tableau; both normal and non-normal tableaux will then close, and LCLbb is then valid in MS1. Let us now turn back to clause (b). Suppose that a construction begun for a formula CLbCLgd closes, and so does the one begun for LAbg. If we begin a construction for the formula LCLbCLgd, we get a non-normal tableau (let us say, corresponding to the non-normal world x) in that construction with CLbCLgd right, and so with Lb and Lg left (the normal part of this construction closes by hypothesis). By the behaviour of L and the defined relation s (see formula 9.5) in nonnormal worlds, the following must then obtain:

9.11	s  x(w | ~Tyb)
9.12	s  x(w | ~Tyg)

Now recall the peculiar property of this relation as expressed in 9.5, that no two sets of worlds "s'ed" by a given world are disjoint. This means that, given 9.11 and 9.12, there is at least one world in which b and g are false at the same time. But this is contrary to the assumed validity of LAbg. Placing Lb and Lg together left in an MS1° non-normal tableau is then contradictory, and the tableau may be said to close. Clause (b) of RL1 is then validity-preserving in MS1° (MS1). The only S1° (S1) postulates which will force the use of non-normal tableaux in MS1° (MS1) in a function other than as MPC tableaux, then, are the rules BKW and RL1; these rules have just been shown to be validity-preserving in MS1° (MS1), and *9.1 then permits us to say that *9.9 holds.

We shall now set about proving the converse of *9.9; to do so, we shall first set down model structures MS1°¢ and MS1¢ and show them to be equivalent to MS1° and MS1 respectively. All rules for these new systems are the same as for the other S1° (S1) models we have been considering; where these systems will differ is in the statement of conditions for the closing of non-normal tableaux; we shall then show that the conditions here stated are equivalent to those for the closing of MS1° (MS1) tableaux. A non-normal tableau for MS1°¢ or MS1¢ will be said to close when

(a)	the same formula appears on both sides of it, or
(b)	La appears left, Lb appears right, and the construction begun for ab closes, or
(c)	La and Lb occur on the left and the construction begun for LAab closes.

We shall wish to show that

*9.10

A formula is valid in MS1° (MS1) iff it is valid in MS1°¢ (MS1¢).

Suppose that a formula is valid in MS1°¢ (MS1¢). The conditions for validity so far as normal tableaux are concerned are the same in MS1°¢ (MS1¢) as in MS1° (MS1), so we need examine only the situation of the non-normal tableaux. If a non-normal tableau closes as a result of clause (a) above, clearly the MS1° (MS1) tableau corresponding to it will also so close. If such a tableau closes by clause (b) above, we may follow the general argument of the BKW case in the proof of *9.9 to show that the corresponding MS1° (MS1) tableau closes; if the tableau closes by (c), the case clearly parallels the RL1 case in the proof of *9.9. The reader may then easily supply the details of the proof that if a formula is valid in MS1°¢ (MS1¢) it is also valid in MS1° (MS1).

Establishing the converse of this is somewhat more complicated. We shall twist the question about here somewhat and set out to prove the converse of the above by showing that if there is a countermodel in MS1°¢ (MS1¢) to a given formula, then there is a countermodel to that formula in MS1° (MS1). First of all, if a countermodel arises because of happenings in normal tableaux (that is, if a countermodel can be constructed in MT° (MT)), then clearly one can be constructed in MS1° (MS1). We suppose, then, that the countermodel arises because of a non-normal tableau in MS1°¢ (MS1¢). Then there is a non-normal tableau in the construction begun for our formula which is such that

(a)	no formula a occurs both left and right in it, and
(b)	if La occurs left in it and Lb right, then ab is invalid, and
(c)	if La and Lb occur left in it, then LAab is invalid. We note that this includes the case in which if Laoccurs left, La must be invalid, for LAaa is valid iff La is.

Let us assume as a preliminary case for MS1°¢ that (a) above holds, and that (b) and (c) both hold by virtue of the tableau's having no formula beginning with an L on its right when it has one on its left, and no more than one formula (and that formula invalid) on its left under any circumstances. These conditions are met if there are no formulas beginning with an L in the tableau. Recall, however, that there will always be a normal tableau beginning with the same formula as does this non-normal tableau; since the non-normal tableau has no formulas beginning with L in it, neither then would the normal tableau; these two tableaux will, indeed, be identical; since the non-normal tableau is assumed not to close, then the normal one would not close either; this situation is covered in the case considered above when the formula is not valid in MT° (MT). Another possibility is that the non-normal tableau has exactly one formula beginning with an L on its left (and that formula not valid) and no formulas beginning with L's on its right. Let that formula be La; as we have noted, by clause (c) this formula is invalid; clause (a) is assumed to hold, and (b) holds because of no L-formula right. There must be at least one world in which a is false. Let a = (w | TwNa), and let our non-normal world be x, with s xa. We have then met the requirements of MS1° for a consistent assignment of true to La in x, and we have a countermodel in that system. The only other possibility left in this preliminary case is that (with (a) holding) there are no formulas left beginning with L (rendering (b) and (c) above true), and an arbitrary number Lb₁, . . ., Lb_n right. If any of these formulas, say Lb_i, is valid, then there is no world in which bi is false, and so this non-normal world cannot bear the relation s to the set of all worlds in which b_i is false, and Lb_i is then located consistently in our MS1° (MS1) tableau. For the Lb_i which are not valid, proceed as follows. Let there be a set of worlds a such that the non-normal world in question bears the relation s to a and only to a. Then for each invalid Lb_i let there be a world y_i in which b_i is false, and have y_i Ï a. No contradiction arises from this assumption, and so each such Lb_i is consistently placed. All that is necessary to extend this preliminary case to MS1¢ is to specify that in the subcase in which La is placed right in the tableau that a also be right there; if a cannot consistently be placed right there, the tableau would have closed, which is contrary to the hypothesis.

We have thus covered the situations in which, with (a) holding, (b) and (c) hold because their antecedents are false. Let us now consider the case in which (a) and (c) hold, and (b) holds because there is a formula La left and an Lb right, and ab fails to obtain. Once again, because of (c) La is invalid, and so there are worlds in which it is false; let a be the set of all such worlds, and let our non-normal world be x, with s xa, and if b ¹ a, ~ s xb. La is then true in x (considered as an MS1° world); if Lb were to be true in x, then b would have to be false in all and only the worlds in which a is false, for x bears the relation s only to the set a. But then ab would be valid, contrary to our hypothesis. Lb is then false in non-normal world x, as required. Once again, to extend this case to MS1, we need only assume that a be true in x also.

We now consider the case in which (a) and (b) hold, and (c) is true by virtue of there being formulas La and Lb left in the non-normal tableau, with LAab invalid. In this case there are worlds in which both a and b fail to hold. Let a be the set of all worlds in which a is false, and b the set of all worlds in which b is false; note that the (existent) set of worlds in which both a and b are false is the intersection of a and b, which is then non-empty. We then can have both s xa and s xb consistently, and we then can construct a countermodel in MS1°. To extend the case to MS1, simply require that a and b be true in x. We have thus shown how to construct an MS1° (MS1) countermodel for any formula which is invalid in MS1°¢ (MS1¢), and so have established that if a formula is valid in MS1° (MS1) then it also is valid in MS1°¢ (MS1¢); this completes the proof of *9.10.

We now wish to show that if a formula is valid in MS1° or MS1°¢ (MS1 or MS1¢), then it is provable in S1° (S1). We shall do this by making use of the sequent-logics LS1° and LS1. The proof will closely parallel that for MS2° and MS2 of the last section. The induction there was on the number n of applications of L-r(2) used in constructing the longest alternative set of a closing construction of tableaux. We assume that when we have a closing construction of MS1°¢ (MS1¢) tableaux beginning with formulas G left and Q right, and for which n £ k, a proof for G ® Q can be constructed in LS1° (LS1); we consider the case for n = k + 1. As in the last section, if k = 0, then G ® Q is provable in LT° (LT) without the use of ®L and so is also provable in LS1° (LS1). For larger k, there is a normal tableau auxiliary to the main tableau and beginning with the formulas D left (inserted from main by L-l) and l right (inserted from main tableau by L-r(2). This tableau itself begins a closing MS1°¢ (MS1¢) construction for which n = k; by the induction hypothesis D ® l is then a theorem of LS1° (LS1). Now deriving from the main tableau is also a non-normal tableau beginning with D left and l right. By hypothesis this tableau also closes, and so one of the following three conditions applies:

(a)	The same formula appears both left and right in it, or
(b)	La appears left in it, and Lb right, and the construction begun for ab closes, or
(c)	La and Lb appear left in it, and the construction begun for LAab closes (includes case in which La appears left and construction begun for La closes):

We show first that in each case LD ®Ll is derivable in LS1° (LS1). If case (a), then the non-normal tableau closes as a result of the MPC rules (MPC + L-r for MS1); the parallel normal tableau will also then close in that manner, and D ® l is then a theorem of LPC (LPC + L® for MS1¢), and LD ® Ll is then derivable in LS1° (LS1).

Consider now case (b). In this case there is an LS1° proof for La ® Lb without the use of ®L with empty left premiss. La and Lb occur left and right respectively in our auxiliary tableau; they occur as subformulas of D or l; their derivation from these formulas required no use of L-r, and so the proof of  D ® l from La ® Lb requires no use of ®L with empty left premiss, and this then applies to the whole proof of D ® l; LD ® Ll is then provable in LS1° (LS1) for case (b).

Consider now case (c). This parallels the case in the last section in which just La stood left in an MS2° non-normal tableau. By a similar argument, we may see that D ® l a is then provable in an LS1° (LS1) proof which has as a sequent in each of its proof strings one of form La, Lb, D¢ ® L and that no applications of ®L stand between any such sequents and D ® l. It is easily seen that a provable sequent with La and Lb left and ® LAab holding (or La left and ®La holding) parallels the situation hypothesized in rule RL1 for S1° (to infer LbCLgd from CLbCLgd when LAbg holds). It is clear then that each La, Lb, D¢ ® L is then derivable in LS1° (LS1) without use of ®L without empty left premiss, and then so too is D ® l. In case (c) also, then, LD ® Ll is provable in LS1° (LS1).

In any case, then, we can come to LD ® Ll as an LS1° (LS1) theorem. The LD correspond to the formulas in the main tableau which gave rise to the D in the auxiliary tableau, and the Ll is the formula which originally by L-r(2) started the construction of the auxiliary tableau. LD ® L, then, stands as a starting sequent for the final segment of our LS1° (LS1) proof. The operations in the main tableau of the construction give us the recipe for getting from that sequent to G ® Q; no applications of ®L are required, and so this sequent is provable in LS1° (LS1) as required. By *9.1 and *9.9 and *9.10 along with the above, then, we have

*9.11

A formula is valid in MS1° (MS1) iff it is valid in MS1°¢ (MS1¢), and so iff  ® a is provable in LS1° (LS1) and so iff a is a thesis of S1° (S1).

By *9.2, then:

*9.12

MS1° (MS1) provides a decision procedure for S1° (S1).