Proofs and Semantic Tableaux

1. What a proof is

An argument is a claim that some conclusion follows from some premises. A proof is what settles that claim: a finite, checkable object that anyone can read line by line and agree with, without having to take your word for anything. The point of a proof is not that it convinces you - a good speech can do that - but that every step in it is one that could not have gone otherwise.

That is a stricter demand than it sounds. "It rains, so the ground is wet" is a reasonable thing to say, but it leans on what you know about rain and ground. Formal logic strips that away and asks a narrower question: given only the shape of the sentences, is there any way at all for the premises to be true while the conclusion is false? If there is no such way, the argument is valid, and the proof is the record of why there is none.

This guide is about one way of producing that record - the method of semantic tableaux, also called truth trees. It is the method this site uses whenever you type an argument into the calculator, and once you have followed it once you can check an argument on paper with nothing but a pen.

2. Valid, and how you would know

Write an argument with a turnstile: the premises on the left, the conclusion on the right. The claim p → q, ¬q ⊨ ¬p says that from a conditional and the denial of its consequent, the denial of its antecedent follows. The turnstile is not another connective. It is a claim about the formulas either side of it, and it is either right or wrong.

The definition of validity points straight at a way of testing it: check every assignment of true and false to the variables, and see whether any of them makes all the premises true and the conclusion false. That is what a truth table does, and for two or three variables it is perfectly good. The trouble is that the table grows as 2ⁿ. Ten variables need a thousand rows, twenty need a million, and the table says nothing about which rows mattered.

A tableau attacks the same question from the other end. Instead of listing every possibility and looking for a bad one, it assumes a bad one exists and tries to build it. If the attempt collapses in contradiction on every route it could take, no such assignment exists and the argument is valid. If the attempt succeeds, what it built is a counterexample you can read off directly.

3. The tableau method

A tableau is a tree of signed formulas. Each line is a formula with a T or an F in front of it, and the sign says what the branch is assuming about that formula - not what the formula's truth value is, but what you would need it to be for the argument to fail. The whole method is four steps:

1. Write each premise with a T. You are supposing the argument's premises all hold.
2. Write the conclusion with an F. You are supposing it fails anyway - this is the assumption you are trying to refute.
3. Take any line that is not yet an atom and apply the rule for its main connective and sign, adding what that rule produces to the end of every branch running through it.
4. Close a branch as soon as it holds both T A and F A for the same formula A. Stop when every branch is closed, or when no line is left to decompose.

Nothing in that loop requires cleverness or a choice of strategy. Every line has exactly one rule, and applying them in any order gives the same verdict - which is why a machine can do it, and why you can trust the result when it does.

4. The rules

There is one rule for each connective under each sign - ten in all. They fall into two kinds, and the difference between the kinds is the whole reason a tableau is a tree rather than a list. An α rule says several things must hold together, so it stacks its results down the branch. A β rule says one of two things must hold, so it splits the branch in two and lets each case go its own way.

Each rule is just the truth condition of its connective, read backwards. A conjunction is true only when both sides are, so T (A ∧ B) stacks T A and T B. A conjunction is false when at least one side is, but the formula does not say which, so F (A ∧ B) has to try both: it branches. The same asymmetry runs the other way for disjunction, and a conditional false means the antecedent held and the consequent failed - the one case where an implication breaks.

Notice what the rules never do: they never invent a formula. Everything a rule produces is a piece of the line it came from. That property - the subformula property - is what makes the method finite, and we come back to it below.

5. Closing a branch

A branch is a single line of reasoning: read from the root down to a leaf and you have one complete set of assumptions. A branch closes when those assumptions contradict each other outright, which means it carries both T A and F A for the very same formula. It does not matter how complicated A is, or how far apart the two lines are - if a branch needs a formula to be both true and false, nothing satisfies it.

Mark a closed branch with ×, naming the two lines that closed it, and stop working on it. Nothing further can be learnt from an assumption that was already impossible.

When every branch closes, the tableau is closed, and that is the proof. It shows that the supposition you started with - all premises true, conclusion false - leads to a contradiction on every route it could take. Since there was no route left, there is no such assignment, and the argument is valid. This is proof by contradiction, laid out so the cases cannot be missed.

6. A proof, line by line

Take modus tollens: p → q, ¬q ⊨ ¬p. Lines 1 and 2 are the premises, assumed true. Line 3 is the conclusion, assumed false - and since the conclusion is ¬p, assuming it false is assuming p true, which line 5 records. Line 4 comes from the negation rule applied to line 2: if ¬q is true, q is false. The conditional on line 1 is the only line left with a connective, and it is a β rule, so the tree forks:

The left branch supposes the conditional held because its antecedent failed - but line 5 already has p true, so the branch contradicts itself and closes. The right branch supposes it held because its consequent was true - but line 4 already has q false, so it closes too.

Both branches closed, so there is no way to have p → q and ¬q true with ¬p false. The argument is valid, and the tree is the reason. Notice that the proof never mentions rain, ground, or what p and q stand for. It did not need to.

7. When a branch stays open

Not every argument is valid, and this is where the method earns its keep. If you work a branch until nothing on it can be decomposed further - only atoms and negated atoms remain - and it has still not closed, that branch is saturated and open. It has not failed to close because you stopped too early. There is nothing left to try.

An open branch is more than a verdict of "invalid". Read the signs off its atoms and you have an assignment: every atom marked T is true, every atom marked F is false. That assignment makes every premise true and the conclusion false, which is exactly what a counterexample is. Logicians call it a countermodel, and it is a concrete answer to "why not?" rather than a refusal.

Affirming the consequent, p → q, q ⊨ p, is the standard case. Its tableau leaves a branch open on p false and q true - a situation where the conditional holds and its consequent holds, and yet the antecedent does not. That single assignment refutes the argument on its own.

8. Why it always finishes

Every rule replaces a formula with its own subformulas, and every subformula is strictly shorter than the formula it came from. So no branch can grow forever: each step moves down a finite ladder of pieces of the original argument, and the ladder has a bottom. Eventually every line on a branch is an atom or the negation of one, and there is nothing further to do.

That is a real guarantee, not a hope. It means the method is a decision procedure for propositional logic: run it on any argument and it will stop, with either a closed tree or an open branch, and never with a shrug. The prover on this site enforces a node budget on top of that, but only as a guard against a pathological formula exhausting a browser tab - the mathematics needs no such limit.

9. Other proof systems

Tableaux are one proof system among several, and they are the refutation-shaped one: they work by ruling out failure. Natural deduction works the other way, building the conclusion forward from the premises with rules like modus ponens and conditional proof, and it reads much more like the way a mathematician argues in prose. A natural-deduction proof of an argument is usually shorter; finding it usually takes more invention.

The sequent calculus formalises the turnstile itself and reasons about entailment claims as objects, which makes it the tool of choice for proving things about proofs. Resolution reduces everything to clauses and a single rule, which is unglamorous to read and extremely fast to run - it is what most automated theorem provers and SAT solvers are built on.

All of them agree on which propositional arguments are valid; they differ in what a proof looks like and in what is easy to find. Tableaux are the friendliest to learn from, because a failed proof is not a dead end - it hands you the counterexample.

10. Practise

The fastest way to learn the method is to run it. Type an argument into the calculator with ⊨, ⊢ or |= and the tableau is drawn alongside the truth table, so you can check the tree against the rows. Then work through some proofs on paper before looking.