Tableaux

A tableau (plural tableaux), also called a truth tree, tests a claim by searching for a counterexample. A truth table writes out every case. A tableau instead breaks formulas into smaller pieces and follows only the cases that could work. The basics guide explains the connectives and the words used here.

Searching for a counterexample

Take the argument P ∨ Q, ¬P ∴ Q. A counterexample would make both premises true and the conclusion false. So it would make three formulas true at once: P ∨ Q, ¬P and ¬Q. A tableau starts from exactly that list and asks: can all of these be true together?

It answers by breaking each formula into simpler formulas that must be true if it is. For example, P ∧ Q can only be true if P and Q are both true, so the tableau writes P and Q below it. Breaking a formula up like this is called expanding it, and the tableau rules say how to expand each kind of formula.

Branches are possibilities

Some formulas can be true in more than one way. P ∨ Q is true if P is true, or if Q is true. The tableau cannot know which, so it splits in two, with one branch for each way. A branch is one path through the tree, from the top down to one of its ends, and it describes one possibility.

So there are two kinds of rule. A stacking rule writes its results one under the other, on the same branch: P ∧ Q gives P and Q. A branching rule splits the branch: P ∨ Q gives P on one side and Q on the other.

Closing a branch

If a branch contains a formula and its negation, such as P and ¬P, it cannot describe a real possibility, since P cannot be both true and false. The branch is closed: the app marks it ✕ with the two lines that clash, and nothing more is added to it. A branch that contains ⊥ closes too, since ⊥ is never true.

Reading the result

If every branch closes, every possibility ends in a contradiction: the starting list cannot all be true. What that tells you depends on the question, because each kind of task starts from a different list:

• Argument. It starts from the premises and the negated conclusion. If every branch closes, the argument is valid.
• Formula. It starts from the negated formula. If every branch closes, the formula is a tautology.
• Set. It starts from the formulas of the set. If every branch closes, the set is inconsistent.
• Two formulas. For A and B, it starts from ¬(A ↔ B), which is true exactly where the two differ. If every branch closes, they are equivalent.

If a branch holds no clashing pair, and every formula on it that has a rule has been expanded, it is a complete open branch, marked ○. It describes a real possibility. Give every sentence letter that appears on its own on the branch the value T, and every other letter F. This choice of values, a valuation, makes every formula on the branch true, the starting list included. It is called a countermodel.

So a complete open branch gives the opposite verdict. The argument is invalid, and the countermodel is a counterexample. The formula is not a tautology. The set is consistent, and the app calls the valuation a model. The two formulas are not equivalent.

Worked example: every branch closes

“The key is in the drawer or in my coat. It is not in the drawer. So it is in my coat.” With P for “the key is in the drawer” and Q for “the key is in my coat”, this is P ∨ Q, ¬P ∴ Q, a pattern called disjunctive syllogism.

1. Write the starting list. The premises go in as they are, and the conclusion is negated: line 1 is P ∨ Q, line 2 is ¬P and line 3 is ¬Q. The app writes this list for you and labels each line premise or negated conclusion.
2. Pick a line to expand. Lines 2 and 3 are negated letters, which cannot be broken down: no rule applies to them. Line 1 is a disjunction, so the ∨ rule applies.
3. Apply the rule. P ∨ Q is true if P is true or Q is true, so the ∨ rule is a branching rule. The tree splits: P goes on the left branch (line 4) and Q on the right (line 5). The app labels each new line “1, ∨”: from line 1, by the ∨ rule.
4. Close the left branch. Read the left branch from the top: P ∨ Q, ¬P, ¬Q, P. It holds P (line 4) and ¬P (line 2), which clash, so it closes.
5. Close the right branch. The right branch holds Q (line 5) and ¬Q (line 3), so it closes too.
6. Read the result. Every branch is closed, so no valuation makes the premises true and the conclusion false. The argument is valid.

Worked example: an open branch

Now an invalid argument: “The key is in the drawer or in my coat. So it is in the drawer.” This is P ∨ Q ∴ P.

The starting list is P ∨ Q (line 1, the premise) and ¬P (line 2, the negated conclusion). The ∨ rule splits line 1 into P (line 3) and Q (line 4).

The left branch closes: it holds P (line 3) and ¬P (line 2). The right branch holds P ∨ Q, ¬P and Q. Line 1 has been expanded, lines 2 and 4 have no rule, and no two lines clash. The branch is complete and open.

Read the countermodel off the open branch. Q appears on its own, so Q is true. P appears only as ¬P, so P is false. Check it: P ∨ Q is true and the conclusion P is false. This is a counterexample, so the argument is invalid. The app shows the verdict Invalid, with P = F, Q = T under “Countermodels from the open branches”.

Solve and Practice

In Solve, the default, the app does the work. Step makes one move and Complete finishes the tableau. You can also select a line and press its button (for line 1, “Expand line 1”) to choose the next move yourself. An expansion goes onto every open branch below the line, and the app closes each branch as soon as it holds a contradiction. The verdict appears as soon as it is settled: when every branch is closed, or when one branch is complete and open. Each complete open branch then shows its countermodel.

In Practice, you make every move and the app checks each one:

• To expand a line, select it and press its button (for line 1, “Expand line 1…”). In the dialog that opens, write what the rule adds: one branch for a stacking rule, two for a branching rule, and press Expand. The app accepts the formulas in any order. If they are wrong, it says so without giving the answer away.
• To close a branch, select a formula and its negation on that branch, or a single ⊥, and press Close branch.
• To mark a finished branch open, select its last line and press Mark open. The app refuses if the branch can still be closed, or still has a formula to expand.

Hint suggests a next move. The verdict appears once every branch is closed or marked open, and only the branches you marked open show a countermodel.

Strategy: stack before you branch

The order of moves never changes the verdict, but it changes the amount of work. After a branching rule, every later expansion has to be written on each of the new branches. So use stacking rules first and branching rules as late as you can, and close a branch as soon as it holds a contradiction. Solve and Hint follow this order.

Compare two ways through the set P ∨ Q, ¬P ∧ ¬Q:

• Stacking first. The ∧ rule on line 2 adds ¬P and ¬Q (lines 3 and 4). Then the ∨ rule on line 1 splits into P and Q (lines 5 and 6), and each branch closes at once. That makes 6 lines.
• Branching first. The ∨ rule gives P and Q (lines 3 and 4), and neither branch closes yet. Now the ∧ rule has to add ¬P and ¬Q to both branches (lines 5 to 8) before they close. That makes 8 lines.

Both tableaux close, so the set is inconsistent. With longer lists the gap can grow much larger, since each branching rule can double the number of branches that later lines must be written on.

Common mistakes

• Negating the wrong thing. For an argument, only the conclusion is negated; the premises go in as they are. The app writes the starting list for you, but you need this on paper.
• Splitting a negated disjunction. ¬(P ∨ Q) is true only if P and Q are both false, so its rule stacks ¬P and ¬Q on one branch. It is ¬(P ∧ Q) that branches.
• Getting the → rule wrong. P → Q branches into ¬P and Q, not into P and Q.
• Closing across branches. The two clashing lines must both lie on the branch: on the path from the top down to the branch’s end.
• Closing on near misses. A branch closes only on a formula and its exact negation. P and ¬Q do not clash, and neither do P ∧ Q and ¬P: that clash appears only once P ∧ Q is expanded and puts P on the branch.
• Stopping too soon. A branch is open only once every formula on it that has a rule has been expanded.
• Reading too much into an open branch. For a formula, an open branch shows only that the formula is not a tautology. It may still be true on many valuations.

The rules

The app uses nine rules, one for each kind of formula that can be broken down. A sentence letter, a negated letter, ⊥ and ¬⊥ have no rule. In the tables, A and B stand for any formulas. Each rule lists the ways its formula can be true: A → B, for example, is true when A is false or B is true.

The entries in the Rule column are the labels the app shows beside each new line, as in “1, ∨”. A branch closes when it contains a formula X together with ¬X, or contains ⊥.

Soundness and completeness

Two theorems show that the method gives the right answers. Let Γ be a finite set of formulas. A tableau for Γ is one that starts from the formulas in Γ, and it is finished when every branch is closed or complete. Γ is unsatisfiable if no valuation makes all its formulas true.

• Soundness: if a tableau for Γ closes, Γ is unsatisfiable. Every rule keeps a satisfiable branch satisfiable: if a valuation makes every formula on a branch true, it also makes true everything a stacking rule adds, or everything on at least one of the branches a branching rule creates. A closed branch can never be made true, so a tableau for a satisfiable set always keeps an open branch.
• Completeness: if Γ is unsatisfiable, every finished tableau for Γ closes. Put the other way round: if a finished tableau has a complete open branch, Γ is satisfiable. The valuation that makes exactly the letters standing alone on the branch true makes every formula on the branch true. This is proved by induction on the length of formulas, and it is why the app’s countermodels always work.

Write Γ ⊨ A when the argument with premises Γ and conclusion A is valid. Then Γ ⊨ A if and only if a finished tableau for Γ with ¬A added closes. The same goes for the other questions: A is a tautology if and only if the tableau for ¬A closes, and A and B are equivalent if and only if the tableau for ¬(A ↔ B) closes. The order of moves cannot change the verdict, so any finished tableau will do.

Termination

A tableau for a finite list of formulas cannot grow forever. Each line is expanded at most once, and every rule adds only formulas that are shorter than the one it expands, counting each letter, ⊥ and connective as one symbol. So each branch can only grow so long, and since a rule splits a branch into at most two, the whole tree is finite. Expanding until nothing is left always stops: a tableau, like a truth table, is a decision procedure, a method that always stops with the right answer.

Finite is not the same as small. Each branching rule can double the number of branches, so in the worst case a tableau grows exponentially, like a truth table. Solve stops completing a tableau automatically once it would grow past 2,000 lines.

Tableaux, truth tables and proofs

A complete open branch stands for a group of truth-table rows at once: a letter that does not appear on the branch, either on its own or negated, could take either value (the app makes it false). A closed tableau rules out every row without listing them, often in a few lines where a truth table would need thousands. The short truth table is a close cousin: it also assumes a counterexample and fills in what is forced, splitting only where it must.

A closed tableau is also a kind of proof: a refutation, showing that the starting list cannot all be true. A natural deduction proof, the subject of the proofs guide, works forwards from the premises instead. Both methods are sound and complete for propositional logic, so an argument has a proof exactly when its tableau closes.

Further reading

Tableaux go back to Evert Beth and Jaakko Hintikka in the 1950s. The classic account is Raymond Smullyan’s First-Order Logic (1968), which calls them analytic tableaux, sorts formulas into α (stacking) and β (branching) types, and proves soundness and completeness in this style.

For more on the semantic ideas behind them, see the part on truth tables in forall x: Calgary, the free textbook whose proof rules the app uses.