## THE ABSOLUTELY STRICT SYSTEMS -- TABLEAUX

Modal models

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.

This idea has recently (and independently) been revived, however, in somewhat different dress. Prior 1957 introduces us to the 'Diodorean modal system' (about which more will be said in later chapters) in which possibility and necessity are defined by reference to future instants of time. An instant of time can easily be construed as a possible world, and so Prior's Diodorean system is a logic of possible worlds in the general spirit of Peirce. In 1959, Kripke took a step that resembles Peirce's formalism even more than does Prior's. He provided a method of constructing semantic models for a modal system (specifically S5; the method was later extended to other systems; see, for example, Kripke 1963). Central to the method of Kripke is the notion of 'possible world'. A Kripke-style semantic model will contain a number of elements; these elements and the relationships between them are defined abstractly, but the primary intuitive interpretation for them, perhaps, is to refer to them as possible worlds. In some logical respects, these worlds are independent of each other. A statement a may be true in world w1 but false in world w2; if a contains no modal operators, its truth or falsity in a given world depends entirely upon the state of affairs in that world and in no way on conditions in another. But if a contains modal operators (L's or M's), its truth or falsity in world w1 may well depend on the state of affairs in world w2. The worlds in a Kripke model may then be related to each other in a certain way; an intuitively clear way of explaining what this relation is is to call it the 'accessibility relation'. The state of affairs in world w2 can affect the truth or falsity of modalized statements in world w1 only if world w2 is 'accessible to' world w1. We might picture a computer grinding away in world w1, determining the truth and falsity of statements submitted to it; we could reasonably expect this computer to have available to it full information on the state of affairs in world w1 itself (that is to say, the accessibility relation is reflexive -- w1 has access to itself). So long as the statements submitted to it contain no modal operators, the computer will function in a provincial manner, utilizing only information about its own world. But as soon as modal operators are introduced, the computer in w1 will have to get on the telephone and query the computers in certain other worlds about the situations in their respective worlds. The worlds it queries are all and only those accessible to it, those bearing the accessibility relation to it. The accessibility relation is, as we have noted, often reflexive; it might also have (though it need not have) other properties associated with relations, such as transitivity or symmetry; indeed -- as we shall see -- by altering the properties associated with this relation we shall be able to construct models for a variety of different modal systems. The total set of models constructible for worlds with an accessibility relation having a given set of properties is called a 'model structure'.

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.

As with an 'oblique method' check for validity in the PC, checks for validity in our modal systems will be, basically, attempts to construct countermodels for the formulas in question. These countermodels will be provided, if they exist within a given model structure, as in the PC case by assigning truth values (1 and Æ, or true and false) to the variables of these formulas. We think of the countermodel construction as beginning in the 'actual' or 'real' world; if the formula being checked contains no modal operators, then the countermodel construction attempt stays entirely within that real world; the truth values assigned in this case are truth values pertaining only to the actual world, and the results here are PC results. The simple assignment of the value true or false to a variable is assignment relative to a given world, however, and a formula might consistently be assigned true in, say, the real world, but false in some possible world. We run into cases in which truth or falsity in worlds other than the real world must be considered when we meet formulas containing modal operators. The general rule to be followed in the valuation of modal formulas in the world w1 takes account specifically of the worlds to which w1 has access, and it states that the formula La will be true in world w1 iff a is true in every world to which w1 has access. It then follows that La is false in w1 if a is false in any world accessible to w1; Ma is true in w1 iff a is true in any world accessible to w1 ; Ma is false in w1 iff a is false in every world to which w1 has access. Thus the necessity operator in this context emerges as a kind of universal quantifier and the possibility operator as a kind of existential quantifier, the quantifiers ranging over the set of possible worlds.

We used semantic tableaux as a handy way of keeping track of our work in the oblique method of PC evaluation. With appropriate modifications, we may use them in a similar manner here. The rules for behaviour of PC connectives are just the same here as they were in Chapter 4; this corresponds to our earlier indication that the PC operations proceed in a given world without reference to any other world. Now let us suppose for the moment that the formula in which we are interested, for which we wish to try to construct a countermodel, has its PC connectives so situated in it that there will be no need to use the rules C-l, K-r, and A-l. The situations which in Chapter 4 called for alternative splits will then not arise. The formula is written into the right column of a tableau; this tableau is thought of as representing the real world, and the inscription of the formula on its right indicates that we wish to falsify the formula in that world, to find a countermodel for it. Now suppose that in the process of performing the tableau construction operations we come up with a formula La on the right of the tableau. Since the tableau is keeping track of the valuations needed to find a countermodel of the original formula, this means that La must be false for this purpose in the real world. La will be false in this world (call it w1) iff a is false in any of the worlds accessible to w1, so we continue our attempt to construct a countermodel by assuming that there is a possible world (call it w2) in which a is false. As a simple example, let us try a construction for the formula CpLp. We first write CpLp right in a tableau, and then perform the PC operation C-r:

 CpLp p Lp

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:

 L-r: If La occurs on the right of a tableau, construct a new tableau auxiliary to that tableau and beginning with only a on its right.

Tableau tx is auxiliary to tableau ty, of course, iff tx's world wx is accessible to ty's world wy.

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:

 L-l: If La occurs on the left of a tableau, write a on the left of each tableau auxiliary to that tableau.

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.

Each alternative set is an attempt to construct a countermodel; all that is needed to show that that attempt fails is to demonstrate that an assignment required in just one of the proposed worlds of that countermodel is impossible. Such an assignment is impossible iff the tableau corresponding to that world closes. So we shall apply the terminology of closing to alternative sets; an alternative set will be said to close iff one of the tableaux belonging to the alternative set closes. A construction of tableaux will be said to close iff every one of the alternative sets belonging to it does.

Once a construction of tableaux is begun, there are three possible outcomes. First, the construction may close; if it does so, clearly it does so in a finite number of steps. Secondly, it may be carried on to the point at which no rule of tableau construction can be applied, and the construction fails to close. When this occurs, we have constructed a recipe for the consistent assignment of truth values in various worlds to the subformulas of the original formula, consistent assignment, that is, of truth values which result in the falsification of that original formula. We then have found a finite countermodel to that formula. Thirdly, and perhaps surprisingly, under certain conditions it is possible that the construction might be carried on as far as we wish without closing and without yielding a finite countermodel. This can occur when (with certain formulas) the accessibility relation is transitive. Assume this property, and consider the formula CLMpMLp. We apply, first,, all the PC steps we can to it in a tableau (placing the formula in primitive notation):

 CLNLNpNLNLp LNLNp NLNp LNLp

We now apply L-l to the two formulas on the left (we assume reflexivity of the accessibility relation here) and then N-1 to the resulting formulas

 CLNLNpNLNLp LNLNp NLNp LNLp NLNp LNp NLp Lp

Having gone as far as we can with this tableau, we create auxiliary tableaux by the application of L-r to the LNp and Lp (we show only the auxiliary tableaux). Note that L-1 will cause NLNp and NLp to be placed left in each of these; the rule L-l applies not only to tableaux existing when it first comes into play for given formulas (in this case LNLp and LNLNp) but it applies to auxiliary tableaux created later as well.  NLNp Np NLp

 NLNp p NLp

We next do N-1 for the formulas left in each auxiliary tableau.  Np NLNp LNp NLp Lp

 p NLNp LNp NLp Lp

If we now execute L-r again, we do it four times, constructing two tableaux auxiliary to each of the above auxiliary tableaux; since the accessibility relation is assumed to be transitive, each of these new auxiliary tableaux will also be auxiliary to the main tableau, and so will receive NLNp and NLp left by virtue of the L-1 applied in the main tableau:  NLNp Np NLp

 NLNp p NLp  NLNp Np NLp

 NLNp p NLp

At this point it should be evident that we are about to begin a repeating process, and that no matter how far we carry it, it will just keep recycling. Thus we have an example of a tableau construction that neither closes nor yields a finite countermodel.

If a tableau construction closes, we clearly have shown that a countermodel does not exist for the formula in question, and that formula then is valid. If a tableau construction reaches a point where no further rules can be applied and no closure has resulted, we have shown how to construct a finite countermodel. If, as in the above example, the construction neither closes nor terminates without closing, we can work as long as we please at the construction of a countermodel. By what is essentially an application of Konig's lemma (1926), we use this fact to assert, in this last case, the existence of an infinite countermodel. We are now in a position to say:

 *9.1 A formula is valid in a given model structure iff the tableau construction (with auxiliarity relation corresponding to the accessibility relation of that model structure) begun for that formula closes.

The occurrence of such infinitely cycling chains of tableaux makes the question of decision procedures for modal systems somewhat more complicated than is the case with the system PC; nevertheless, we can use tableaux to provide such procedures; The formula for which the construction was begun contains only a finite number of subformulas. Since the number of distinct tableaux which can be constructed from a given set of formulas is limited by the size of that set, there is only a finite number of distinct tableaux which can be included in the construction beginning with any given formula. If we suppose that a construction goes on without end, there will then be a stage of the construction at which tableaux begin to appear which are contained in tableaux which have already been entered into the construction; a tableau is contained in another iff all its formulas on the left appear on the left of the other, and all its formulas on the right are on the right of the other. If tx is contained in ty, then, the state of affairs in wx may be considered a 'substate' of that in wy; whatever happens in wx happens in wy as well. If discovery of a countermodel is not shown impossible in ty (which by hypothesis it is not) then it cannot be shown to be impossible in tx either. So far as tableaux are concerned, if ty does not close, then the included tx will not close either. Investigating tx adds nothing to our knowledge, and tx may be abandoned as a blind alley. We then agree that if a tableau arises in a construction but turns out to be included in an earlier tableau, we shall apply no rules to it. It is clear that with this convention each construction will terminate, and we shall be able to recognize the tableaux which represent an infinite countermodel as well as those which give us finite countermodels or show the impossibility of countermodels. We then may assert:

 *9.2 It is decidable whether or not a tableau construction closes, and so whether or not a given formula is valid in a model structure.

Tableaux for and T

We shall recall that the sequent logics for and T were actually simpler in statement than were those for S2 and S1. The same will be the case with the systems of tableaux corresponding to these systems. We shall, in fact, find it to our advantage to start our discussion with tableau systems corresponding to and T, which may be viewed as the basic systems of modal tableaux.

As we have noted, we may specify a model structure by stating the properties its accessibility relation is to have. Suppose we consider first of all the model structure whose accessibility relation has no specified properties; call this structure MT°. We shall develop a correlation between MT° and the system .

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 '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 ; since all PC theses are valid in this model structure and all the rules of inference of 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. 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 :

 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 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:

 p ® p WK p ® p, q
 q ® q WK q, p ® q

C®

Cpq, p ® q

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

 Cpq, p ® q ®L LCpq, L p ® Lq

We have now entered the realm of the next tableau 'up the line'. In the case of our example, this is also the main tableau of each of our alternative sets; the segment of proof string involved, then, will be the final segment of each string. Within a segment, again, we perform only PC operations (or PC operations plus L® in MT); in the case of our example, we are instructed by the tableau operations to perform ®C twice:

LCpq, L p ® Lq

®C
 LCpq ® CL pLq ®C ® CLCpqCL pLq

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:

 *9.4 A formula a is valid in MT° (MT) iff ® a is a theorem of LT° (LT) and so also iff a is a theorem of T° (T).

By *9.2, then:

 *9.5 MT° (MT) provides a decision procedure for T° (T).

Tableaux for S2° and S2

We shall now begin to speak of model structures MS2° and MS2. These will be like MT° and MT except that they will include nonnormal worlds. The non-normal worlds will be used to increase our chances of finding a countermodel to a given formula; we employ the non-normal worlds according to certain principles. First of all, the 'real world' is always a normal world. Secondly, as we have noted, every non-normal world behaves as if it had access to the 'inconsistent world'. Thirdly, the accessibility relation in M52° is like that in MT° and the accessibility relation in MS2 is like that in MT. We shall alter our rule L-r to take into account the possibility of non-normal worlds; since the non-normal world is to give us an extra opportunity to falsify a formula, we shall think of this rule in MS2° and MS2 as involving a split; one of the branches of the split goes on just as would an alternative tableau set in MT° or MT and contains only normal tableaux; the other branch of the split involves a non-normal tableau.

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

All other operations in normal tableaux go on as in MT° and MT. As we have noted, PC operations go on as usual in non-normal tableaux; no modal operations are needed, however, in these tableaux. If La occurs on the right of such a tableau, no further justification is needed, as all formulas beginning with an L are false in a nonnormal world. On the other hand, if a formula beginning with L occurs on the left of a non-normal tableau, that tableau will be considered to close, for the same reason (a non-normal tableau may also close as does a PC tableau, by having a formula not beginning with an L on both its left and its right sides). An alternative set concluding with a non-normal tableau will be considered to close iff that non-normal tableau closes; the whole tableau construction will close iff all of its alternative sets -- including the ones involving non-normal tableaux -- close. Let us now show:

 *9.6 All S2° (S2) theses are valid in MS2° (MS2).

The formulation of (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

 RL2: If a is a thesis, then so too is La, provided it is a PC theorem or is of form CLbg.

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

 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.1 (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 Lb1, . . ., Lbn right. If any of these formulas, say Lbi, 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 bi is false, and Lbi is then located consistently in our MS1° (MS1) tableau. For the Lbi 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 Lbi let there be a world yi in which bi is false, and have yi Ï a. No contradiction arises from this assumption, and so each such Lbi 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).