Tableaux

Origin. Beth (1955), Smullyan (1968). Tree-based proof search. Formulas labeled signed. Branch closure for contradiction. Foundation for automated reasoning.

Models. Systematic decomposition. Signed formulas: T:φ or F:φ. α-rules (non-branching), β-rules (branching). Closed tableau = proof.

Formalism.

Signed formulas: T:φ (φ is true) F:φ (φ is false)

α-rules (conjunctive): T:A ∧ B → T:A, T:B (same branch) F:A ∨ B → F:A, F:B F:A → B → T:A, F:B T:¬A → F:A

β-rules (disjunctive): F:A ∧ B → F:A | F:B (split branches) T:A ∨ B → T:A | T:B T:A → B → F:A | T:B F:¬A → T:A

Branch closure: Branch closed if contains T:A and F:A. Tableau closed if all branches closed.

Completeness: Closed tableau for ¬φ proves φ. Open branch → countermodel.

First-order: γ-rules: T:∀xA, F:∃xA (instantiate any term) δ-rules: F:∀xA, T:∃xA (fresh variable)

Modal tableaux: Labeled formulas: w:φ Accessibility: wRv Rules propagate across worlds.

Symbols.

Symbol	Unicode	Name	Meaning
α	U+03B1	Alpha	Non-branching (conjunctive) rule type
β	U+03B2	Beta	Branching (disjunctive) rule type
γ	U+03B3	Gamma	Universal rule: instantiate by any term
δ	U+03B4	Delta	Existential rule: instantiate by a fresh parameter
×	U+00D7	Multiplication sign / Closure	Marks a branch containing T:A and F:A
¬	U+00AC	Negation	Swaps the sign of a signed formula
∧	U+2227	Conjunction	α on T, β on F
∨	U+2228	Disjunction	β on T, α on F
→	U+2192	Implication	β on T, α on F
∀	U+2200	Universal quantifier	γ on T, δ on F
∃	U+2203	Existential quantifier	δ on T, γ on F
T:	—	Signed true	Assertion that the formula holds
F:	—	Signed false	Assertion that the formula fails
w:φ	—	Prefixed formula	φ holds at world w in a modal tableau
wRv	—	Accessibility atom	v reachable from w

Metatheory. Beth introduced semantic tableaux in 1955; Hintikka's model sets supplied the model-existence argument and Smullyan's First-Order Logic (1968) gave the uniform α/β/γ/δ classification the method is now stated in. Completeness follows from Hintikka's lemma: every open, downward-saturated branch is a Hintikka set and so determines a model, hence a formula with no closed tableau is satisfiable; running the systematic construction is a proof of Gödel completeness, and with König's lemma it yields compactness. Tableaux and cut-free sequent calculi are notational variants — a closed tableau for F:φ is a cut-free LK derivation of ⊢ φ read upside down, the α/β split is the invertible/branching split of the sequent rules, and the δ-rule's freshness condition is the eigenvariable condition. Free-variable tableaux replace the γ-rule's blind instantiation by unification, deferring the choice of term. Propositional tableaux terminate, so validity is decided; first-order tableaux are a semi-decision procedure. D'Agostino (1992) showed the standard tableau method does not polynomially simulate the truth-table method; the KE calculus of D'Agostino and Mondadori repairs this by adding an analytic cut.

Applies to. Automated theorem proving. Logic education. Model generation. Decision procedures. Interactive provers.

Limitations. Tableaux are refutation procedures: φ is proved by closing a tableau for F:φ, so there is no forward derivation of φ and nothing corresponding to stating a lemma. Being cut-free, they bear the cut-free blow-up — a fact needed on several branches must be re-derived on each, and no rule lets it be recorded once. The γ-rule may be applied unboundedly often with fresh terms and there is no computable bound on how many instances suffice, so first-order completeness holds only in the limit and fairness must be imposed by a strategy outside the calculus. Intuitionistic and modal tableaux cannot simply delete used formulas from a branch; prefixes, world labels, or Kripke-style bookkeeping are required, and logics whose frame conditions are not first-order — the Löb axiom needs converse well-foundedness — get no rule of the standard prefixed form. Termination for modal systems comes from loop checking, which is a device added on top of the rules rather than a property of them.