4.

GROUNDWORK - PROPOSITIONAL LOGIC AND TABLEAUX

THE last chapter developed certain powerful systems corresponding both to the classical and to the intuitionist propositional calculi. These systems enable us to find a proof for a given formula of IC or PC iff that formula is provable; in effect, they provide us with a decision procedure for each of these systems. One might initially look upon the present chapter as an attempt to refine the methods of the last chapter by making these decision procedures easier to apply. We shall, indeed, begin our presentation as if this were our motivation. It will turn out, however, that the present subject-matter is considerably more than a mere aid to calculation, ancillary to the sequent logics of the last chapter. It provides us with an introit to the semantics of the classical PC and, as it will turn out, to the semantics of many modal systems as well.

Proof tableaux

Powerful though the sequent-logics are, they have certain mechanical disadvantages for use as decision procedures. Not the least of these is one determined by a feature of these logics very important in making them powerful; this is the subformula property. Once a formula appears in a cut-free proof in a sequent-logic, it does not later disappear, but must be written at each following step of the proof, either as a subformula of a larger formula or itself as a parametric formula. If a hundred steps follow the introduction of a, then a is written out a hundred times. It might be well to seek to find a method in which some of the work involved in writing and rewriting such formulas is avoided. Such a method was provided by Beth 1955; we shall now investigate a version of his approach. Study of the sequent-logics begins with the notion of the wff of the ordinary propositional calculi. Α 'larger context' for the wff is then developed by the definition of sequences and sequents; within this larger context, the sequent-logic proof-theory is developed. The method of Beth is to develop a different 'larger context for the wff, a context which permits execution of operations paralleling those of the sequent-logics, but permitting greater compactness and saving of labour. While the sequent is the basic 'working unit' of the Gentzen systems, the basic working unit of Beth's approach is called the 'tableau'. Where one of Gentzen's sequents may be broken down into the two sequences that are its antecedent and its succedent respectively, the tableau of Beth may be analysed into a right and a left column, the left column corresponding to Gentzen's antecedent and the right column to his succedent. As we shall see, however, the tableau does the job not just of one sequent, but of a set of sequents; in fact, it does the job of all the sequents in a proof string of a given sequent-logic proof.

In the sequent-logics, if we wish to prove a given sequent, we do it, strictly speaking, by beginning with axioms and then working by the rules through successively longer and more complex sequents until we have reached the desired endsequent, say G ® Q Tableaux work in the opposite direction. If we wished to show, using tableaux, that G ® Q is provable in one of our sequent-logics, we should begin by writing all the formulas of Γ in the left column and all those of 0 in the right column of a tableau. We should then proceed to decompose those formulas (employing rules which, as one might expect, are inverses of sequent logic rules). What we watch for in this decomposition process may best be shown by some examples. Consider the sequent ® CKpqCrq. We begin a tableau for this sequent by writing

The first tableau operation to be applied will involve the decomposition of CKpqCrq. It begins with a C and is on the right of the tableau, so the sequent-logic rule paralleled here is ®C; we then write Kpq on the left and Crq on the right of the tableau:

The new formula on the left begins with a K, and so the sequent-logic rule corresponding to it is Κ®; the premiss for this rule with Kpq as main formula would have p and q in its antecedent as side formulas, and so, recalling that we are working backwards, we write p and q to the left of the tableau:

One compound formula remains which has not been operated upon; this is Crq on the right, and again the relevant rule is ®C. The r then goes to the left and the q to the right of the tableau:

We have gone as far as we can in this particular tableau, and we have reached a significant point in tableau construction. Note that the wff q occurs as a 'free-standing' formula both on the left and on the right of the tableau. When this happens for any wff, we say that the tableau in question 'closes'. We have mentioned that a tableau corresponds to a sequent logic proof string. The occurrence of the same wff on both sides of a tableau corresponds to beginning a proof string with an axiom of the sequent logic. In fact, the above tableau gives us a 'recipe' for the construction of a proof in, say, LPC for ® CKpqCrq. We should begin that proof with the axiom a ® a, where a is the formula for which the tableau closed (in this case q). We should then note all the formulas standing in the tableau which have not caused the application of a rule (in this case, the formulas qualifying are p and r; CKpqCrq, Kpq, and Crq have each been the occasion of a rule application). Take the formulas for which there has been no rule application, and insert them into a ® a by appropriate applications of weakening, those on the left of the tableau into the antecedent and those on the right into the succedent (remember that we are now discussing LPC proofs; we shall examine the situation for LIC shortly):

Now, in reverse order to the order used in constructing the tableau, apply the logical rules corresponding inversely to the rules used in constructing the tableau:

It is clear that the last sequent may be converted by a final application of ®C to the sequent for which the tableau construction was begun in the first place. Thus finding a closing tableau here gives us a method of constructing a proof for that sequent. We may comment now on a difference in the proof construction recipe when it is applied for the system LIC. If we wish to use a tableau to construct a proof in LIC, the method of inserting formulas by weakening will differ from that above. As we saw in the last chapter, all LPC rules are invertible with respect to each other; it is then all right to apply all weakenings which will occur in a given proof at the very beginning of that proof. In LIC, however, invertibility does not hold in the general case, and so there will be proofs in which weakenings must occur at specific locations, and not always at the beginning. So suppose that an LIC proof is to be reconstructed from a tableau which has closed. First write the relevant axiom as with the LPC case. Now note each formula a which has not been the occasion of a tableau-constructing operation. a itself was written into the tableau at a definite stage in the construction, either at the very first stage as a formula of the original sequent, or as the result of the application of a rule which we may call R. If the former situation, simply insert a into the LIC proof as its very last step. If the latter case, begin constructing the LIC proof from the axiom already written down by applying the relevant LIC rules in reverse order to that in which their inverses were applied in the tableau construction, and immediately before reaching the application of R^-1, the inverse of the above-mentioned rule R, insert a by weakening. Thus the weakenings in the LIC proof will be distributed as necessary throughout the proof. The same could, of course, be done with LPC proofs in this situation, but as we have noted, the invertibility of LPC rules makes the situation there simpler, in that all weakenings may be disposed of at the very beginning of the proof.

Now we must realize that the tableau constructed above represents the simplest kind of situation in tableau construction. Note that the operations involved all correspond to single-premiss rules of the sequent-logics. The rules A®, C®, and ®Κ, however, are two-premiss rules. They involve the combining of two proof strings in a sequent-logic proof; below the application of one of these rules the two proof strings involved are the same, and above they are generally distinct. We have a parallel situation when Α or C begins a formula on the left or Κ begins a formula on the right of a tableau. Just as the relevant sequent-logic rules involve the combining of two proof strings into a common 'lower part', so do their parallel operations in the tableaux involve the splitting of a tableau into two tableaux having a common 'upper part (corresponding to the common part of the two proof strings joined by a two-premίss sequent-logic rule) but generally distinct below this common part.

As an example, if Apq occurs on the left of a tableau, we should first copy out the tableau, giving us two identical tableaux, and then we should write p on the left of one of these tableaux, and q on the left of the other, and then proceed with the construction of both of those tableaux. Actually, we should not in practice ordinarily write out the second tableau in its entirety, but should indicate the point of the split by a horizontal line extending out from the centre line of the original tableau and with the centre line of the new tableau extending down from its end; the two tableaux below the horizontal fine share all that is above it. Consider as an example a tableau for the sequent ® CCCpqpp; this will have as its first two lines:

We are now faced with a C in the left part of the tableau. As indicated above, we split the tableau; the antecedent of the formula on the left (CCpqp is that formula) will go into the right half of one of the tableaux formed by the split (this reflects the left premiss of the classical rule C®) the consequent of CCpqp will go into the left half of the other tableau.

We note immediately that the alternative tableau to the right has already closed. We now continue with the left tableau.

So the left tableau also closes (recall that the part above the horizontal line is in both tableaux). We may use the above pair of tableaux to construct the following LPC proof:

When we scribe splitting tableaux as we have done, they fall into a tree structure paralleling the tree structure in sequent-logic proofs. If we follow a continuous line from the top of the tableau diagram to the bottom of one of the 'branchings', it is like moving from the end sequent to the very tip of one of the branches of a sequent-logic proof along one of its proof strings. Moving along a continuous line from the top of the tableau diagram to the bottom of one of its branchings is actually tracing out one of the alternative tableaux formed by the splits of tableaux in the set of tableaux which began with the formulas at the top of the diagram. If we use the system of tableaux as a recipe for the construction of a sequent-logic proof, we shall see then that each tableau in the set corresponds as we have mentioned to a complete proof string in the sequent-logic proof. It becomes clear, then, that when we have a tableau splitting as above, the test of theoreιnhood for the sequent for which the tableau system was started is whether every alternate tableau in the system closes; a tableau closing parallels a sequent-logic proof beginning with an axiom. Α system of tableaux such as we have been discussing will be said to close iff each of its alternative tableaux closes.

Let us comment now on several features which will be peculiar to tableaux used for the intuitionist system. These features are predicated upon the fact that no provable sequent in LIC will have more wffs than one in its succedent. Since a tableau is analogous to a proof string rather than to a single sequent, intuitionistic tableaux may have more formulas than one on their right, but there are certain restrictions to be observed here. These restrictions may be summed up in the following: although more wffs than one may appear on the right of an intuitionistic tableau, no more than one of these formulas at any time may have 'action pending' on it. A formula has action pending on it iff it has not been the occasion of a tableau rule application; simple variables always have action pending on them. The formulas with action pending at a given stage of construction of a tableau are all and only those in the sequent corresponding to that stage of construction. By seeing to it that at no time more than one wff on the right has action pending on it, we insure that in the proof string corresponding to our tableau no sequent has more than one wff in its succedent. Consideration of the various LIC rules will show that several will be involved here. One is the intuitionist C®. all two-premiss rules of LIC and LPC except intuitionist C® have in common the feature that if the side formulas were to be erased from the premisses and the main formula from the conclusion, the resulting three sequents would be identical. This permits us to say that when a tableau splits as we have described above, the portions of the resulting tableaux above the split are identical. This is not the case with LIC's C®.. When an intuitionist tableau splits because of C on the left, both alternative tableaux will be identical above the split on their left sides. But where Cab is the wff causing the split, the alternative tableau receiving a on its right (corresponding to the left premise of LIC's C®) may differ from the original. The cases in which it will differ are those in which there is a wff with action pending on the right of the original tableau. In these cases that wff is omitted in the tableau we are now considering; in effect it is replaced by a. The wffs with no action pending on the right are inserted into this tableau. The tableau which receives b on its left (corresponding to the right premiss of LIC's C®) is the same as the original tableau except for the b on its left. Note that if the above restriction had been applied to the tableaux we constructed for ® CCCpqpp, the alternative tableau taking Cpq on its right would not have closed, for there would be no p on its right. We leave it to the reader to verify that tableaux split as restricted above correspond to the respective proof strings in a proof containing the intuitionist C®.

Another rule we might expect to be affected here is one involving N. This is because the N rules will 'move formulas' from one side to the other of tableaux. Specifically, we are interested in the rule

applied when Ν occurs on the left of a tableau. As we might expect, when Na occurs on the left of a tableau, we write a on the right of that tableau. But for intuitionist tableaux we may do so only if there is no wff with action pending on the right. Note that it is not necessary to restrict the rule for Ν on the right.

The final intuitionistic rule affected, although in a different manner, is ®A. When Αab occurs on the right of a classical tableau, we should correctly expect that both a and b will be written on the right of that tableau. In the intuitionistic system we cannot do that (for reasons noted above), but we still must explore both the a and the b possibility (Αab as main formula in the conclusion of ®A could arise from either a or b as side formula, we know not which). So we think of ourselves as splitting the tableau, and placing a on the right of one of the tableaux resulting from the split and b on the right of the other. But this is a different kind of split from those considered to this point. Rather than requiring that both sets of tableaux generated by the split close, for the entire set of tableaux to be said to close, it is required merely that either one of them close. And this agrees with the intuitive interpretation of the inverse of ®A. Now let us note a potentially confusing change in view-point. We shall have occasion, important occasion, to look upon the construction of a set of tableaux as an attempt to falsify rather than to prove or verify a formula. We use this point of view rather than the point of view heretofore assumed in assigning a name to the kind of split associated with intuitionist ®A. If the sequent with which a tableau set is begun contains a split due to an Α on the right, and if that sequent is not a thesis of LIC, then both sets resulting from that split must fail to close. We shall then call the kind of split resulting from Α on the right a 'conjunctive' split, and the other kind of split we have studied an 'alternative' split, even though these names appear paradoxical if we view a tableau construction as an attempt to show that a given sequent is a thesis.

Proof tableaux formal characterization

We shall now set down more formally the rules for construction of tableaux. As with the logical sequent-logic rules, there will be a pair of rules for each connective, one for the left column and one for the right. They will be designated 'C-l' for 'C on the left', 'C-r' for 'C on the right', 'K-l', 'K-r', etc. As we have noted, we construct a tableau for a given sequent G ® Q; the construction is begun by writing the formulas in G on the left and those in Q on the right of the tableau. Then we apply rules as follows:

It will be recalled that in the instructions for reconstructing a sequent-logic proof from a closing set of tableaux, we remarked that all formulas in the tableaux other than the wff for which the tableau closed which have not been the occasion of rule applications must be inserted by weakening. The restrictions on rules C-l, A-r, and Ν-l above guarantee that if a set of intuitionistic tableaux is begun with no more than one formula on the right, then there will be no more than one formula on the right of any tableau in that set at any time which has not been the occasion of a rule application; thus weakening in the succedent in the proof reconstructed from such a set will never be performed with a non-empty succedent. Since no tableau rules other than C-l, A-r, and Ν-l  add to the number of wffs on the right which have not been the occasion of rule applications, the proof reconstructed from a closing set of intuitionist tableaux will be such that no sequent in that proof will have a succedent with more formulas than one. No more than one formula that has action pending on it can stand on the right of any intuitionistic tableau at any time; thus when the rule Ν-r is applied, the formula to which it is applied is the only one on the right eligible for a rule application. After this application there are no formulas on the right eligible for rule application. This parallels the requirement in the proof to be reconstructed from the closing set of intuitionistic tableaux that ®N, like weakening on the right, also be applied only with empty succedent.

We now go on to prove several metatheorems.

Proof is immediate, for there is clearly only a finite number of ways in which tableaux for a given sequent can be constructed, since the sequent itself is of finite length.

As we noted earlier, if a set of tableaux closes, it can be used as a recipe for the construction of a proof in the appropriate system for the sequent in question. Thus *4.2 holds.

Suppose that a sequent is provable in a proof one step long: it is then a ® a, an axiom, whose tableau clearly closes. Now suppose that whenever a sequent is provable in a proof whose longest proof string is no longer than k steps, there is a closing tableau set constructible for that sequent. Consider the case in which the longest proof string has k + 1 steps. If the (k + 1)th step is by a logical rule, then the metatheorem holds, for our tableau rules are essentially inverses of the logical sequent-logic rules. If the (k+ 1)th rule applied is weakening, then the kth step is the sequent G ® Q and the (k + 1)th is a, G ® Q or G ® Q, a. Adding a either to the left or to the right side of a tableau will not prevent that tableau from closing if it were going to do so without a, and so if the tableaux for the kth step close in this case, so too will those for the (k + 1)th. If the (k + 1)th step is by contraction, the situation for classical tableaux is not affected, because of *3.11, which shows the redundancy of contraction in LPC. For intuitionistic tableaux, we may handle this case by understanding that occurrences of formulas on the left of an intuitionistic tableau may be the occasion of more than one rule application. The formulas on the left parallel, then, the quasi-principal constituents in rules C® and N® of the modified LIC, in which (by *3.11 also) contraction is redundant. *4.3 then holds. We combine the last two metatheorems

By *4.4, *4.1, and the equivalence of LIC (LPC) to IC (PC) we state:

Semantic tableaux

We now turn specifically to the classical systems we have been discussing. Our purpose will be to view classical tableaux from a point of view different from that above. We are all familiar with the ordinary two-valued truth value system and with the method of evaluating PC wffs in it. Here (one might read 1 as 'true' and 0 as 'false') Cab = 1 unless a. = 1 and b = 0, in which case it = 0; Kab = 0 unless both a and b are 1, in which case it is 1; Aab = 1 unless both a and b are 0, in which case it is 0; Na = 0 when a = 1 and 1 when a = 0. Given the above information, one can construct a 'truth table' for any PC wff which will determine effectively whether or not that formula is a 'tautology'. Α tautology, of course, is a wff which always takes the value 1, regardless of the values assigned το its variables.

One way of testing a formula for tautologism is to adopt some systematic format, usually a table of some kind, suitable for recording the 2ⁿ different assignments of 1 and 0 to the n distinct variables of that wff. It also will have places to record the computed values for each of the subformulas of that wff at each of those 2ⁿ assignments. The test consists of actually running through all 2ⁿ assignments and noting the computed value at each for the whole formula. If this value is 0 for any assignment, the wff is not a tautology. This method is mechanically applicable and effective, but it can also be awkward and time-consuming as anyone who has applied it to a middle-sized formula with as few as three variables will testify. There is another, often quicker method of evaluating a PC wff for tautologism; this is the 'oblique', or 'indirect' method. Rather than construct a full truth table for a formula, the evaluates will begin making assignments of 1 and 0 to the subformulas of that formula, assignments which will falsify it if it is falsifiable. If he succeeds by this method in falsifying the formula, he knows that it is not a tautology. However, if his attempts at falsification require that some subformula receive at the same time an assignment of 1 and one of 0, he has come up with a contradiction based upon the assumption that the wff is falsifiable; this means that it is not falsifiable, that it is a tautology. The formula CCpqq, for example, can be falsified only if Cpq can be assigned 1 at the same time that q is assigned 0. In the indirect method we make those assignments; we now look at Cpq and-noting that q must be assigned 0 in it-we see that it can indeed receive the value 1 as required, provided ρ = 0. This assignment may be made consistently, and so CCpqq is not a tautology, failing at p = q = 0. On the other hand, consider the formula CKpqCrq. This can be false only if Kpq takes 1 and Crq takes 0 at the same time. But for Crq to take 0, q must be 0 while for Kpq to be 1, q must be 1. This is impossible; by assuming that CKpqCrq is falsifiable, then, we have derived a contradiction, and this formula is a tautology. There are a variety of methods in the literature for keeping track of work in the oblique method. We have available to us one of the handier of those methods; a system of tableaux much like those we have been studying can serve very well to keep track of work in this method. We again employ tableaux each of which is divided into a left and a right column. In this case, the left column is associated with the value 1 and the right with the value 0. We start out by placing the formula to be tested for tautologism in the right part of our tableau, for we are going to attempt to falsify it.

We then inquire what values the subformulas of this formula must take if it is to receive ultimately the value 0. The only way the main formula can be 0 is if its antecedent takes 1 while its consequent takes 0. We keep track of this fact by writing Kpq on the left ('true') side of the tableau, and Crq on the right ('false') side:

We thus keep a running account of the work we are doing in our attempt to falsify the formula. We now examine the newly written formulas. In order to be true, Kpq must have both p and q true. We record this by writing both of these formulas on the left of the tableau

Finally, to be false, Crq must have r = 1 and q = 0, so r is written to the left and q to the right:

The contradiction involved is clearly shown by q's appearing on the left (true) as well as the right (false) side of the tableau. Tableaux employed as above may be called 'semantic tableaux'. When a formula (as with q above) appears on both sides of a semantic tableau, we shall say that that tableau closes, as we did with proof tableaux.

The formula CKpqCrq is such that there is only one possible path to falsification of it, only one way to try to make it false. This is not the case with certain other formulas. Consider CCCpqpp. We begin an attempt to falsify this formula by writing it on the right side of the tableau, and then writing its antecedent on the left (true) and its consequent on the right (false) side:

We now know that for falsification CCpqp must be true and p false. But CCpqp may be true in either of two cases-it is true if p is true, or if Cpq is false. We must consider both cases, and so we split the tableau into two alternative tableaux (as we did with some proof tableaux), one with p on the left and the other with Cpq on its right (we use the 'tree format' of the proof tableaux):

We note that the tableau with p on its left closes; CCCpqpp cannot be made false in that manner, then. Now, in the other tableau Cpq must be falsified, and so we write p to the left and q to the right:

This tableau also, then, has p left (true) as well as right (false), and so it also demonstrates an impossibility of assignment. But this exhausts all the possible ways of falsifying CCCpqpp, and so it is a tautology.

We say that a set of alternative semantic tableaux as above closes iff each tableau in the set closes. Note again, by the way, that the apparently backward naming of the above kind of split tableaux as 'alternative' tableaux is not at all backwards when we view the construction of tableaux as an attempt to falsify rather than to verify a formula. It is easy to see that semantic tableaux will split as above whenever they have a formula beginning with a Κ on the right, or with a C or an Α on the left.

Let us now set down a set of rules for the construction of semantic tableaux just as we did for proof tableaux. C-ls will be the rule applied when a formula beginning with C occurs on the left of a tableau; C-rs when such a formula appears on the right, etc. We state the rules for semantic tableaux:

Note that each of the rules for the left side reflects exactly the conditions needed to render a statement beginning with each of the respective connectives true (taking, of course, the left as the true and the right as the false side) and each of the rules for the right side expresses the conditions necessary for falsification of the formulas beginning with the respective connective. Α semantic tableau constructed by these rules, then, is an attempt to falsify a wff, and this attempt will succeed iff the wff is indeed falsifiable, there being only a finite number of possible ways to falsify any wff. We then state:

Let us now compare the rules for the construction of semantic tableaux with those for the construction of proof tableaux. We note that C-ls has exactly the same effect on a given tableau as does the classical C-l; C-rs has the same effect as C-r, and in general, each semantic tableau rule has just the same effect on α tableau as does its classical counterpart for proof tableaux. It is clear, then, that

By *4.5, *4.6, and *4.7, then, we have

This is both a consistency and a completeness result for PC; all tautologies are theorems, and since only tautologies are theorems, KpNp for example, is not provable in PC.