Semantic Tableaux More about propositional logic

The truth table testing method outlined and illustrated above is easy in simple cases but where sequents get intricate it becomes difficult to manage without the aid of a computer. A more readily usable technique is to grow truth value assignments on trees, also called semantic tableaux. These are designed to make semantic reasoning fully systematic and to generate decisions automatically as to whether sequents are valid or not.

The idea of a tableau is to make explicit and precise the kind of reasoning used earlier to speed up truth table testing by proceeding "top-down", from the values of whole formulae to those of their parts. We take a set of formulae with labels saying which are true and which false, and process them by analysing them into their subformulae, adding labels to those in accordance with the semantics of the various connectives, until either the analysis is complete or a contradiction results. If there is an assignent of values on which the formulae do have their stipulated values, the tableau will find it; if there is not, the tableau will demonstrate that too.

It is quite easy to write a tableau by listing the formulae, with their labels, in a column. As each formula is analysed, its subformulae with their labels get added to the column. This goes on, assigning values to snaller and smaller subformulae, until finally we get values for the atoms. In some cases, of course, the truth tables do not tell us completely what the truth valus of subformulae are, but instead leave open a range of possibilities. For example, if a disjunction A OR B has the label t (i.e. true) then we can continue the analysis either with A labelled t or with B labelled t, but we don't know which. What happens, then, is that the tableau splits into two branches, one with A true and the other with B true, and we must develop both of these branches in parallel. Since the disjunction is inclusive, we allow the possibility that both A and B are true, so the assignments allowed by the two branches are not necessarily disjoint, but this causes no logical problem and, as it turns out, no extra work. In writing out the tableau, therefore, we simply draw the split into two columns and continue them side by side. As the analysis goes on, the tableau develops into a tree, with its root at the top, branching downwards with the atoms as its leaves at the bottom.

:   NOT, AND and OR in tableaux

t: NOTA f: A	t: A AND B t: A,   t: B	t: A OR B t: A t: B
f: NOTA t: A	f: A AND B f: A f: B	f: A OR B f: A,   f: B

The rules for extending tableaux to analyse negations, conjunctions and disjunctions are shown in basicRules. They should be read as saying that a set of labelled formulae including the one above the line may be developed by replacing that formula with the one or more formulae below the line. In each case, the replacement is the result of semantically analysing the displayed formula in accordance with the truth table for its main connective. Where there is a vertical bar separating two sets below the line, this indicates that there are two successor nodes, so the branch of the tableau splits into two at that point.

Clearly, if a negative formula NOTA occurs with either label (t or f) it can simply be replaced by the same formula without the negation sign, with the label reversed. A conjunction labelled as true is replaced by its two conjuncts, also labelled as true, and a disjunction labelled as false by its two disjuncts similarly. A disjunction labeled true splits the branch, as does a conjunction labelled false.

If a formula A occurs in a branch of a tableau with both labels t and f, then we are looking at a "possibility" that isn't one. A contradiction in a tableau branch causes that branch to die: it gets closed off and no more growth happens from its tip. If every branch dies, the tree dies; in that case we know there was no way the tested formulas could all have had the truth values they were initially supposed to have. If, on the other hand, we get to a state in which every subformula has been processed in every branch in which it occurs and some branch is left alive or "open", we have found an interpretation on which all of the original formulas are true. Conventionally we mark a dead or "closed" branch by writing a cross under it. smallClosed shows a simple example of a closed tableau.

:   Closed tableau

Note that in the interests of brevity we do not need to write out all the labelled formulae in the set X at every node: one formula, or a short vertical stack of them, will suffice. This makes it a little awkward to see just what is in a given tableau node, as we have to look back up the branch to find the formulae and their labels. The payoff for this is an increase in clarity and a considerable decrease in tedium.

It is worth spelling out the reasoning embodied in the tableau. We begin by asking whether the two formulae A OR B and A OR NOTB can both be true together and A at the same time be false. That is, we seek an assignment of truth values which will give them those truth values. Since they may be arbitrary formulae, not necessarily atoms, we do not know which atoms need values, but we do not need to as the tableau closes no matter how complex A and B may be. Any verifying truth assignment must make A OR B true, so it must either make A true or make B true; we examine these possibilities in turn. Suppose (left branch) it makes A true. Ah, this contradicts the fact that it has to make A false. Hence the left branch is dead. Now suppose (right branch) that it makes B true. No problem so far. It must, however, also make A OR NOTB true, so we again examine separately the two options for achieving that. For the same reason as before, making A true runs into a contradiction, so we are left with the right-right branch corresponding to the assumption that NOTB is true. However, this in turn requires B to be false, contradicting the truth of B, which was asserted at the earlier fork point. This branch dies as well. The possibilities are exhausted, so we conclude that the three formulae cannot simultaneously have the suggested truth values.

:   IMP and IFF in tableaux

t: A IMP B f: A t: B	t: A IFF B t: A,  t: B f: A,  f: B
f: A IMP B t: A,   f: B	f: A IFF B t: A,  f: B f: A,  t: B

Naturally we need rules for dealing with the other connectives. The rules for developing conditionals are motivated by the fact that A IMP B has the same truth table as NOTA OR B (try it and see). A IFF B has the same truth table as (A AND B) OR (NOTA AND NOTB) so the rules sketched in moreRules are correct.

In order to test a formula using a tableau to see whether it is a tautology, we must start the tree by giving the formula the label f (false). This is because a tautology is a formula which, in virtue of truth tables, cannot be false, and the tableau is a method for reducing to absurdity the supposition that it is false.

To test a sequent for validity, naturally, we start by writing the premises in a column, all with the label t, and then add the conclusion with the label f. This should make perfect sense: we want to know whether a given argument form is valid or invalid, so we try to find a way for the premises to be true and its conclusion false. If there is such a way, the sequent is invalid. If not—if every branch of the tree closes—the sequent is valid

:   Tableau proof of sequent
p IMP (q OR r)   ⊢   NOT(s AND q) IMP ((p AND s) IMP r)
Click here to see it happen step by step.
Click here to construct it yourself.

tableauProof shows a closed tableau constituting a proof of a sequent. Compare the closed tableau with the following natural deduction proof of the same sequent:

SP {p IMP (q OR r) ⊢ NOT(s AND q) IMP ((p AND s) IMP r)} PL {1} {1} {p IMP (q OR r)} {A} PL {2} {2} {NOT(s AND q)} {A} PL {3} {3} {p AND s} {A} PL {3} {4} {p} {3 ANDE} PL {3} {5} {s} {3 ANDE} PL {1,3} {6} {q OR r} {1, 4 IMPE} PL {7} {7} {q} {A} PL {3,7} {8} {s AND q} {5, 7 ANDI} PL {2,3,7} {9} {NOTNOTr} {2, 8 [ ] RAA} PL {2,3,7} {10} {r} {9 NOTNOTE} PL {11} {11} {r} {A} PL {1,2,3} {12} {r} {6, 10 [7], 11 [11] ORE} PL {1,2} {13} {(p AND s) IMP r} {12 [3] IMPI} PL {1} {14} {NOT(s AND q) IMP ((p AND s) IMP r)} {13 [2] IMPI} EP

:   Tableau refuting
p IMP (q OR r)   ⊢   NOT(s AND NOTq) IMP ((p AND s) IMP r)
Click here to try it.

By contrast, nonProof shows the tableau for the very similar sequent resulting by substituting NOTq for the second occurrence of q. This time the sequent is invalid, as is shown by the existence of an open branch. The labels on atoms in that branch record an assignment of truth values to those atoms which is consistent with the formulae from which the tableau starts. Reading up from the bottom (leaf) of the branch, we may collect the labelled atoms thus:

t: q
t: s
t: p
f: r

Since these truth value assignments to atoms resulted from the analysis of the formulae above them in the tableau, they must be sufficient to make the input formulae p IMP (q OR r) and NOT(s AND NOTq) IMP ((p AND s) IMP r) true and false respectively. They do, and the tableau follows the reasoning involved. Since q is true, NOTq is false and q OR r is true, which makes the sequent premise p IMP (q OR r) true as well. Since NOTq is false, s AND NOTq is false, and so its negation is true. Since p and s are both true, so is p AND s; hence, since r is false, (p AND s) IMP r is false. It follows that the conclusion of the sequent, NOT(s AND NOTq) IMP ((p AND s) IMP r), is false, so the sequent is invalid.

A tableau editing tool, rather similar in style to the proof editor, is provided so that you can practice constructing tableaux. It is not difficult to use, but not completely self-explanatory either, so you may wish to check out the user guide for instructions and explanations.