The tree that closes

There is a way of proving a formula that consists entirely of taking it apart, and it produces a picture of the proof as a side effect.

The method has three moving parts and no more: assume the opposite, decompose until only letters are left, and look for a letter appearing alongside its own negation.

The single idea #

A formula is true or it is not. If it is not, there is an assignment making it false, and that assignment can be described.

Take the negation of the thing to be proved, and start writing down what would have to hold for it to be true. Most steps are forced: if $A ∧ B$ is true then $A$ is true and $B$ is true, with no choice. Some steps are not: if $A ∨ B$ is true then one of them is, and the argument has to consider both — which is where the tree branches.

Keep going until every formula on a branch is a letter or a negated letter. Then either the branch contains some letter and its negation, in which case it describes nothing and is closed; or it does not, in which case its letters describe an assignment making the original negation true, and the formula is not a theorem.

That is the whole method. There are no axioms, no rules of inference to memorise, and no ingenuity — every step is forced by the shape of the formula being taken apart, and the only choice is which formula to take apart next, which affects the size of the tree and not the answer.

The ten rules, which are five rules twice #

Each connective decomposes one of two ways.

An α step is a formula whose truth forces two things at once, and it produces a single child carrying both. A conjunction is the obvious case: $A ∧ B$ gives $A$ and $B$. So is the negation of a disjunction — $¬(A ∨ B)$ gives $¬A$ and $¬B$ — and the negation of an implication, $¬(A → B)$, which gives $A$ and $¬B$.

A β step is a formula whose truth forces one of two things, and it branches. $A ∨ B$ gives a branch for $A$ and a branch for $B$. The negation of a conjunction branches the same way. And an implication, $A → B$, gives $¬A$ on one side and $B$ on the other — which is exactly what an implication says.

Double negation is the tenth rule and the dullest: $¬¬A$ gives $A$.

The α/β split is worth noticing rather than memorising, because it is the only thing that governs how big a tree gets. Every α step keeps the tree one branch wide; every β step doubles it. A formula whose decomposition is all α steps produces a stick; a formula full of disjunctions produces a bush.

Reading the picture #

Take the tree at the top of the page slowly.

The root is $¬(((p → q) ∧ (q → r)) → (p → r))$ — the negation of what is to be proved. The negation of an implication is an α step, so the first child carries both $((p → q) ∧ (q → r))$ and $¬(p → r)$ with no branching. The conjunction is another α step, giving $p → q$ and $q → r$. And $¬(p → r)$ is a third, giving $p$ and $¬r$.

At that point the branch holds $p$, $¬r$, and two implications. Implications are β steps, so the tree branches: $p → q$ gives $¬p$ or $q$.

On the $¬p$ side the branch already has $p$, so it closes at once — a letter and its negation, which is a description of nothing. On the $q$ side the branch continues, decomposes $q → r$, and closes on both sides: $¬q$ against $q$, and $r$ against $¬r$.

Every branch closed. So there is no way for the negation to hold, so the formula is a theorem, and the tree is the argument written out.

What an open branch is worth #

This is where the method earns its reputation, because a failed proof is not merely a failure.

The open branch’s letters are $¬p$ and $q$. That is not a hint or a direction to look in; it is the counterexample. Set $p$ false and $q$ true: then $p → q$ is true, $q → p$ is false, and the whole implication is false. The method that failed to find a proof handed over the reason there is none.

Compare that with an axiomatic proof system, where failing to find a proof establishes only that none has been found yet. A tableau either closes or produces a counterexample, and there is no third outcome — which makes it a decision procedure rather than a search.

Two verdicts computed two ways #

A proof method is only worth trusting if something independent agrees with it, and this is exactly the situation where a figure can cheat without anyone noticing: a drawing of a tree with crosses on it looks like a proof whether or not the crosses are in the right places.

So every tableau on this page is checked against the truth table. The tableau is built by decomposition and closes or does not; the truth table is computed by walking the parsed formula over all assignments; and the two verdicts are asserted to agree before the figure is drawn. If a tableau closed on a formula that has a false row, or stayed open on a tautology, the build would stop.

Those are the two halves of a proof system’s respectability, and it is worth naming them.

Soundness: everything the tableau proves is true. If the tree closes, the formula is a tautology.

Completeness: everything true is provable. If the formula is a tautology, the tree closes.

Both are theorems, and both are being instanced by every figure here rather than assumed. A cross-check on one formula is not a proof of either theorem; a cross-check on every formula this collection draws is evidence of exactly the kind this site prefers — a claim given a test it could fail.

Satisfiability, which is the same machine #

Feed the tableau a formula rather than its negation and the question changes. All branches closing now means the formula is unsatisfiable; an open branch is an assignment satisfying it.

Those are the same procedure with different input, and the relationship between the two questions is worth stating: $F$ is valid exactly when $¬F$ is unsatisfiable. Everything in this field about proving things and everything about finding models are the same subject seen from two sides, and the tableau is the clearest place to see it because the machine does not change at all.

That equivalence is also why satisfiability, rather than validity, is what practical tools are built around. A solver is asked “is there an assignment”, and a proof is obtained by asking about the negation and being told no.

The order of expansion, which changes the tree and not the answer #

There is one degree of freedom in the method and it is worth being explicit about it, because it is where all the practical difference lies.

At any point a branch may hold several undecomposed formulas, and the method does not say which to take next. Every choice leads to a closed tree if the formula is valid, so the answer is not at stake. The size very much is.

The rule of thumb is to do every available α step before any β step. An α step adds two formulas to one branch and might close it immediately; a β step doubles the width and then has to close both halves. Doing the branching last means fewer branches exist when the closing literals arrive, and the saving compounds through the depth of the tree.

The figures here follow a simpler rule — take the first non-literal on the branch — because a figure should show the method rather than a tuned version of it. On these formulas the difference is a node or two. On a formula with a dozen disjunctions it is the difference between a tree that fits on a page and one that does not.

That distinction, between a method’s answer and a method’s cost, runs through everything here. Nothing in this essay’s correctness depends on the order; the whole of its practicality does.

Why it always finishes #

The method is only a decision procedure because it stops, and it is worth seeing why, because the argument is short and because the place it breaks is the whole of the next level of the subject.

Every rule replaces one formula by formulas that are shorter — strictly fewer connectives — than the one it decomposed. A conjunction of length $n$ becomes two formulas whose lengths add to less than $n$; an implication becomes two branches each carrying something shorter; double negation loses two symbols. Nothing is ever added that was not smaller than what it replaced.

So along any branch the total size of the undecomposed formulas strictly decreases at every step, and a quantity of whole numbers that strictly decreases cannot go on forever. Each branch reaches a state where only literals remain, and there are finitely many branches because each step produces at most two children. The tree is finite, the procedure halts, and the verdict is available.

That is a termination argument by decreasing measure, and it is the same shape as the proofs that Euclid’s algorithm halts and that a Goodstein sequence reaches zero: find a quantity that goes down at every step and cannot go down forever. The three differ only in what the quantity is and how hard it is to see that it decreases. Here it is the length of a formula and the argument is one line; there, the quantity has to be an ordinal and the argument is a theorem.

The reason it matters here is that the argument is exactly what fails one level up. A quantified formula’s rule for ∀ does not replace the formula — it keeps it, and adds an instance — because the same universal claim may need to be used again with a term that has not appeared yet. Nothing decreases, the branch can run forever, and the tree that was guaranteed finite is not.

Where a tableau gets big #

The method is complete, mechanical and, in the worst case, hopeless.

Every β step doubles the width. A formula that is a conjunction of $n$ disjunctions produces up to $2^n$ branches, and there is no reordering that avoids it in general — a good choice of which formula to expand next can help enormously in practice and cannot change the worst case.

That is not a defect of tableaux specifically. Deciding whether a propositional formula is satisfiable is the standard hard problem, and every method known for it is exponential in the worst case. What differs between methods is which cases they are fast on, and modern solvers are built around a different search — clause learning, backtracking with memory of past failures — that is far better in practice and no better in theory.

The comparison worth drawing is with the truth table itself, which is also a decision procedure and always costs exactly $2^n$ rows. The tableau is often much cheaper, because it stops as soon as a branch closes and never enumerates assignments that the structure of the formula has already ruled out. On the transitivity proof at the top of this page the table would have had eight rows; the tree has four leaves and two of them closed early.

The formula above is the propositional core of a rule machines actually use. From $p ∨ q$ and $¬p ∨ r$ it follows that $q ∨ r$ — the two clauses are combined by cancelling $p$ against $¬p$. That is resolution, one rule instead of ten, and it is what real provers are built on because a single rule is far easier to search with.

The tableau proves it rather than assuming it, which is the right relationship between the two: resolution is a derived shortcut, and its correctness is exactly the closure of the tree above.

Why this is the proof system this field draws #

There are other proof systems and most of them are better for other purposes: natural deduction reads like reasoning, sequent calculus has the cleanest metatheory, resolution is what machines actually run.

Tableaux are here for one reason, and it is a reason peculiar to this collection. The proof is already a picture. Nothing was arranged to make it drawable — the branching is the case analysis, the depth is the decomposition, and the crosses are where the contradiction was found. A natural-deduction proof is a list of lines with justifications and can be laid out as a tree only by a convention imposed on it; a tableau is a tree because the method is a tree.

That makes it the one place in this field where the site’s standing claim is straightforwardly true. A figure that is a proof, rather than a picture of one, is rare — a dissection is the other clean case in this collection — and the tableau qualifies because every mark on it is a step the method took, in the order it took them.

There is one caveat that belongs with the claim. The picture is a proof of a propositional formula, and propositional formulas are the easy case: finite, decidable, and settled by the table anyway. Tableaux extend to quantified logic and the extension is where they stop being finite — a rule for ∀ may have to be used again with a new term at any point, and a branch can go on forever without closing and without ever describing anything. What was a decision procedure becomes a semi-decision procedure, which halts when there is a proof and may not when there is not.

That distinction is the one this whole field is built around, and the tableau is where it first becomes concrete. Here, in the propositional case, the tree always finishes. One step up in expressive power, it may not, and the reason it may not is the same reason an infinite tree can have an infinite path.