Analytic tableaux

It can be difficult in arguments like the one above to keep track of what’s known and what isn’t at each point in the argument. In fact the argument above wasn’t too bad since on the two occasions we had to split the argument into cases we were immediately able to rule out one or both. We aren’t always so fortunate.

There are several versions of tableaux. I’ll use a version where we write true statements to the left of a vertical line and false statements to the right of it. We use existing statements to fill in more and more lines until we reach a point where we need to split into two cases. Then we’ll draw diagonal lines down to a new pair of vertical lines, one for each case, and proceed in the same way with each of them. These are called branches. We can close off a branch whenever we have a statement which appears on both the left and right hand side of a vertical line. We proceed in this way until all branches are closed or until we’ve explored all possible consequences of all statements in all branches.

The tableau corresponding to \({ \{ [ (p ⊃ q) ∧ (q ⊃ r) ] ⊃ (p ⊃ r) \} }\) is given in the accompanying figure.

The contradictions which allow us to close off branches are indicated by underlining the expression which has previously appeared on the other side of the vertical line.

Tableau rules

All expressions in our language are built by joining simpler expressions with logical operators. For each operator there is a pair of tableau rules, one for the case where the expression appears to the left of of the vertical line. We’ve met both of these for the operator ⊃. When an expression of the form \({ P ⊃ Q }\) appears to the left of the vertical bar the tableau branches into a branch with the \({ P }\) on the right of the bar and one with a \({ Q }\) on the left, reflecting the two ways \({ P ⊃ Q }\) could be true, i.e. either \({ P }\) is false or \({ Q }\) is true. On the other hand when an expression of the form \({ P ⊃ Q }\) appears to the right of the bar there is no branching. We get a \({ P }\) to the left of the bar and a \({ Q }\) to the right, reflecting the fact that \({ P ⊃ Q }\) can be false only if \({ P }\) is true and \({ Q }\) is false. The standard way of depicting these rules is with diagrams. In addition to the vertical bar from earlier these diagrams have a horizontal bar. Above this horizontal bar is the statement whose consequences we’re exploring and below the bar are those consequences, which are always one or the other of the subexpressions from which the expresssion was made, and which may appear on either side of the vertical bar. The diagrams for \({ ⊃ }\) are \[ \begin{array}{r|l} ( P ⊃ Q ) & \cr \hline & P \end{array} \qquad \begin{array}{r|l} ( P ⊃ Q ) & \cr \hline Q & \end{array} \qquad \begin{array}{r|l} & ( P ⊃ Q ) \cr \hline P & \cr & Q \end{array} \] There are similar rules for \({ ∧ }\). \[ \begin{array}{r|l} ( P ∧ Q ) & \cr \hline P & \cr Q & \end{array} \qquad \begin{array}{r|l} & ( P ∧ Q ) \cr \hline & P \end{array} \qquad \begin{array}{r|l} & ( P ∧ Q ) \cr \hline & Q \end{array} \] The first of these rules appeared once in our example, when we split the expression \({ [ ( p ⊃ q ) ∧ ( q ⊃ r ) ] }\) on the left hand side of the vertical line to a \({ ( p ⊃ q ) }\) and a \({ ( q ⊃ r ) }\), also on the left.

The diagrams for the remaining operators are \[ \begin{array}{r|l} ( P ∨ Q ) & \cr \hline P & \end{array} \qquad \begin{array}{r|l} ( P ∨ Q ) & \cr \hline Q & \end{array} \qquad \begin{array}{r|l} & ( P ∨ Q ) \cr \hline & P \cr & Q \end{array} \] \[ \begin{array}{r|l} ( ¬ P ) & \cr \hline & P \end{array} \qquad \begin{array}{r|l} & ( ¬ P ) \cr \hline P & \end{array} \] \[ \begin{array}{r|l} ( P ⊼ Q ) & \cr \hline & P \end{array} \qquad \begin{array}{r|l} ( P ⊼ Q ) & \cr \hline & Q \end{array} \qquad \begin{array}{r|l} & ( P ⊼ Q ) \cr \hline P & \cr Q & \end{array} \] \[ \begin{array}{r|l} ( P ⊻ Q ) & \cr \hline & P \cr & Q \end{array} \qquad \begin{array}{r|l} & ( P ⊻ Q ) \cr \hline P & \end{array} \qquad \begin{array}{r|l} & ( P ⊻ Q ) \cr \hline Q & \end{array} \] \[ \begin{array}{r|l} ( P ≡ Q ) & \cr \hline P & \cr Q & \end{array} \qquad \begin{array}{r|l} ( P ≡ Q ) & \cr \hline & P \cr & Q \end{array} \qquad \begin{array}{r|l} & ( P ≡ Q ) \cr \hline P & \cr & Q \end{array} \qquad \begin{array}{r|l} & ( P ≡ Q ) \cr \hline & P \cr Q & \end{array} \] \[ \begin{array}{r|l} ( P ≢ Q ) & \cr \hline P & \cr & Q \end{array} \qquad \begin{array}{r|l} ( P ≢ Q ) & \cr \hline & P \cr Q & \end{array} \qquad \begin{array}{r|l} & ( P ≢ Q ) \cr \hline P & \cr Q & \end{array} \qquad \begin{array}{r|l} & ( P ≢ Q ) \cr \hline & P \cr & Q \end{array} \] \[ \begin{array}{r|l} ( P ⊂ Q ) & \cr \hline P & \end{array} \qquad \begin{array}{r|l} ( P ⊂ Q ) & \cr \hline & Q \end{array} \qquad \begin{array}{r|l} & ( P ⊂ Q ) \cr \hline & P \cr Q & \end{array} \] There is no need to memorise any of these. In each case you can reconstruct the diagram by asking yourself “How could this expression be true?” for the ones where it appears on the left and “How could this be false?” for the ones where it appears on the right.

Satisfiability

What happens if there’s a branch you can’t close? In other words, what happens if you’ve processed all consequences of all statements in the branch and have not found any statements which appear on both the left and the right of the line? In that case there is at least one choice of truth values which make all the statements on the left true and make all the statements on the right false. Finding such a choice is easy. You look for statements of degree zero, i.e. variables on their own without logical operators. Any which appear on the left are assigned the value true and any on the left are assigned the value false. Any which don’t appear at all can be assigned either value. With these choices every statement of any degree on the left will be true and every statement of any degree on the right will be false.

Why does the method above work? Suppose it didn’t. Then there would be a statement of lowest degree which is assigned the wrong value. Because of the way our grammar is defined this statement is constructed by applying a logical operator to statements of lower degree. These statements will appear on either the left or the right hand side of the vertical line lower down and, because they are of lower degree, they will have have been assigned the correct truth value.

Similarly, if you start with an expression on the left hand side of the vertical bar and can’t close a branch then that means there are values of the variables for which the expression is true, i.e. that it is satisfiable. Not only do such values exist but you can find them by assigning variables which appear on the left the value true and variables which appear on the right the value false.

Another example

Consider the statement \({ \{ [ ( ¬ p ) ⊃ ( ¬ q ) ] ⊃ ( p ⊃ q ) \} }\). Is it a tautology, i.e. true for all values of \({ p }\) and \({ q }\)? Is it satisfiable, i.e. true for some values \({ p }\) and \({ q }\)? Is it neither?

To check whether it’s a tautology we start a tableau with the expression \({ \{ [ ( ¬ p ) ⊃ ( ¬ q ) ] ⊃ ( p ⊃ q ) \} }\) to the right of the bar and then apply our various rules.

All rules which can be applied have been applied and we can’t close either of the two branches which were created by splitting the statement \({ [ ( ¬ p ) ⊃ ( ¬ q ) ] }\) so \({ \{ [ ( ¬ p ) ⊃ ( ¬ q ) ] ⊃ ( p ⊃ q ) \} }\) is not a tautology. But the tableau tells us more than this. We can pick an open branch, for example the left branch, and look at which variables appear to the left and right of the bar. In this case \({ p }\) is on the left and \({ q }\) is on the right so taking \({ p }\) to be true and \({ q }\) to be false must make the statement \({ \{ [ ( ¬ p ) ⊃ ( ¬ q ) ] ⊃ ( p ⊃ q ) \} }\) false. In this case we would have got the same values for \({ p }\) and \({ q }\) by choosing the other open branch, but that’s an accident of this particular statement.

We don’t, strictly speaking, need to check that assigning true to \({ p }\) and false to \({ q }\) makes \({ \{ [ ( ¬ p ) ⊃ ( ¬ q ) ] ⊃ ( p ⊃ q ) \} }\) false but we certainly can. If you want to convince someone that \({ \{ [ ( ¬ p ) ⊃ ( ¬ q ) ] ⊃ ( p ⊃ q ) \} }\) is not a tautology, and therefore cannot be a theorem, it suffices to provide them with this counterexample. There’s no need to show them the whole tableau and explain its meaning since they can check the value of the statement for these particular values and verify for themselves that it’s false.

At this point we know that \({ \{ [ ( ¬ p ) ⊃ ( ¬ q ) ] ⊃ ( p ⊃ q ) \} }\) for some values of \({ p }\) and \({ q }\) but we don’t yet know whether it’s true for other values of \({ p }\) and \({ q }\). In other words, we don’t yet know whether it is satisfiable. To check this we start another tableau, this time with \({ \{ [ ( ¬ p ) ⊃ ( ¬ q ) ] ⊃ ( p ⊃ q ) \} }\) to the left of the vertical bar.

Once again we weren’t able to close any branches. It wouldn’t have mattered if we were able to close some. As long as there is one open branch the statement is satisfiable. We can find values of \({ p }\) and \({ q }\) which make the statement true by looking at where the variables are relative to the vertical bar on any open branch. If we take the rightmost branch, for example, then \({ q }\) appears to the left and \({ p }\) doesn’t appear at all. We can therefore take \({ q }\) to be true and take either value for \({ q }\). For definiteness we’ll take it to be true as well.

We don’t need to check that this works but we certainly can. More importantly, so can anyone else, so to convince someone that the statement \({ \{ [ ( ¬ p ) ⊃ ( ¬ q ) ] ⊃ ( p ⊃ q ) \} }\) is satisfiable it suffices to give them the example where \({ p }\) and \({ q }\) are both tree.

In this case we would have got a different example from choosing a different branch. Had we chosen the leftmost branch we would have got the example where \({ p }\) is false and \({ q }\) is true.

Consequences

We can use the tableaux method to check whether a statement is a consequence of a list of other statements as well. We just put it to the right of the vertical bar and those statements to the left and fill in the tableau as before. If all branches close then it is indeed a consequence. If not then by choosing an open branch and looking at which side of the bar each variable lies on we can find truth values for them which cause the premises to be true and the purported consequence to be false. Our earlier method of proving, or disproving, tautologies can be viewed as a special case since a statement is a tautology if and only if it is a consequence of the empty list of statements.

Tableaux as nondeterministic computations

The method of analytic tableaux is an example of nondeterministic computation, like the parsing method for context free languages we considered earlier. There’s a specified initial state and at each point there is a set of operations available, specified by the tableaux rules, but no particular order of operations is specified. The situation for tableaux is better than for context free languages. Different orders of operations will give different tableaux, but no matter which order we choose we will reach an end state where either all branches have been closed or there is an open branch where all rules which can be applied have been applied. Which type of state we reach doesn’t depend the order in which we apply the rules, although some orders may get us there faster than others. This is very different from the situation for context free grammars. There some orders may lead to a parse tree while others will end with a list of tokens which don’t match the input and still others won’t terminate at all.