In proof theory, the semantic tableau (; plural: tableaux), also called an analytic tableau, truth tree, or simply tree, is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics. A method of truth trees contains a fixed set of rules for producing trees from a given logical formula, or set of logical formulas. Those trees will have more formulas at each branch, and in some cases, a branch can come to contain both a formula and its negation, which is to say, a contradiction. In that case, the branch is said to close. If every branch in a tree closes, the tree itself is said to close. In virtue of the rules for construction of tableaux, a closed tree is a proof that the original formula, or set of formulas, used to construct it was itself self-contradictory, and therefore false. Conversely, a tableau can also prove that a logical formula is tautologous: if a formula is tautologous, its negation is a contradiction, so a tableau built from its negation will close.
History In his Symbolic Logic Part II, Charles Lutwidge Dodgson (also known by his literary pseudonym, Lewis Carroll) introduced the Method of Trees, the earliest modern use of a truth tree. The method of semantic tableaux was invented independently by the Dutch logician Evert Willem Beth (Beth 1955), the Finnish logician and philosopher Jaakko Hintikka, and the Swedish philosopher Stig Kanger, and simplified, for classical logic, by Raymond Smullyan (Smullyan 1968, 1995). Smullyan's simplification, "one-sided tableaux", is described here. Smullyan's method has been generalized to arbitrary many-valued propositional and first-order logics by Walter Carnielli (Carnielli 1987). Tableaux can be intuitively seen as sequent systems upside-down. This symmetrical relation between tableaux and sequent systems was formally established in (Carnielli 1991).
Propositional logic
Definitions Assume an infinite set P V {\displaystyle PV} of propositional variables and define the set Φ {\displaystyle \Phi } of formulae by induction, represented by the following grammar:
Φ ::= P V ∣ ¬ Φ ∣ ( Φ → Φ ) ∣ ( Φ ∨ Φ ) ∣ ( Φ ∧ Φ ) {\displaystyle \Phi ::=PV\mid \neg \Phi \mid (\Phi \to \Phi )\mid (\Phi \lor \Phi )\mid (\Phi \land \Phi )} . That is, the basic connectives are: negation ¬ {\displaystyle \neg } , implication → {\displaystyle \to } , disjunction ∨ {\displaystyle \lor } , and conjunction ∧ {\displaystyle \land } . The truth or falsehood of a formula is called its truth value. A formula, or set of formulas, is said to be satisfiable if there is a possible assignment of truth-values to the propositional variables such that the entire formula, which combines the variables with connectives, is itself true as well. Such an assignment is said to satisfy the formula.
General method A tableau checks whether a given set of formulae is satisfiable or not. It can be used to check either validity or entailment: a formula is valid if its negation is unsatisfiable, and formulae A 1 , … , A n {\displaystyle A_{1},\ldots ,A_{n}} imply B {\displaystyle B} if { A 1 , … , A n , ¬ B } {\displaystyle \{A_{1},\ldots ,A_{n},\neg B\}} is unsatisfiable.
For any formulae X {\displaystyle X} , Y {\displaystyle Y} the following facts hold:
If a conjunction X ∧ Y {\displaystyle X\land Y} is true, then X {\displaystyle X} , Y {\displaystyle Y} are both true; is false, then either X {\displaystyle X} is false or Y {\displaystyle Y} is false. If a disjunction X ∨ Y {\displaystyle X\lor Y} is true, then either X {\displaystyle X} is true or Y {\displaystyle Y} is true; is false, then X {\displaystyle X} , Y {\displaystyle Y} are both false. If a conditional X → Y {\displaystyle X\to Y} is true, then either X {\displaystyle X} is false or Y {\displaystyle Y} is true; is false, then X {\displaystyle X} is true and Y {\displaystyle Y} is false. If a negation ¬ X {\displaystyle \neg X} is true, then X {\displaystyle X} is false; is false, then X {\displaystyle X} is true. The method of analytic tableaux is based on these facts. The main principle of propositional tableaux is to attempt to "break" complex formulae into smaller ones until complementary pairs of literals are produced or no further expansion is possible.
The method works on a tree whose nodes are labeled with formulae. At each step, this tree is modified; in the propositional case, the only allowed changes are additions of a node as descendant of a leaf. The procedure starts by generating the tree made of a chain of all formulae in the set to prove unsatisfiability. Then, the following procedure may be repeatedly applied nondeterministically:
Pick an open leaf node. (The leaf node in the initial chain is marked open). Pick an applicable node on the branch above the selected node. Apply the applicable node, which corresponds to expanding the tree below the selected leaf node based on some expansion rule (detailed below). For every newly created node that is both a literal/negated literal, and whose complement appears in a prior node on the same branch, mark the branch as closed. Mark all other newly created nodes as open.
If a branch of the tableau contains a formula ...
T ( X ∧ Y ) {\displaystyle {\boldsymbol {\mathsf {T}}}(X\land Y)} , add to its leaf the chain of two nodes containing the formulae T ( X ) {\displaystyle {\boldsymbol {\mathsf {T}}}(X)} and T ( Y ) {\displaystyle {\boldsymbol {\mathsf {T}}}(Y)} ;
F ( X ∧ Y ) {\displaystyle {\boldsymbol {\mathsf {F}}}(X\land Y)} , create two sibling children to its leaf, containing the formulae F ( X ) {\displaystyle {\boldsymbol {\mathsf {F}}}(X)} and F ( Y ) {\displaystyle {\boldsymbol {\mathsf {F}}}(Y)} respectively;
T ( X ∨ Y ) {\displaystyle {\boldsymbol {\mathsf {T}}}(X\lor Y)} , create two sibling children to its leaf, containing the formulae T ( X ) {\displaystyle {\boldsymbol {\mathsf {T}}}(X)} and T ( Y ) {\displaystyle {\boldsymbol {\mathsf {T}}}(Y)} respectively;
F ( X ∨ Y ) {\displaystyle {\boldsymbol {\mathsf {F}}}(X\lor Y)} , add to its leaf the chain of two nodes containing the formulae F ( X ) {\displaystyle {\boldsymbol {\mathsf {F}}}(X)} and F ( Y ) {\displaystyle {\boldsymbol {\mathsf {F}}}(Y)} ;
T ( X → Y ) {\displaystyle {\boldsymbol {\mathsf {T}}}(X\to Y)} , create two sibling children to its leaf, containing the formulae F ( X ) {\displaystyle {\boldsymbol {\mathsf {F}}}(X)} and T ( Y ) {\displaystyle {\boldsymbol {\mathsf {T}}}(Y)} respectively;
F ( X → Y ) {\displaystyle {\boldsymbol {\mathsf {F}}}(X\to Y)} , add to its leaf the chain of two nodes containing the formulae T ( X ) {\displaystyle {\boldsymbol {\mathsf {T}}}(X)} and F ( Y ) {\displaystyle {\boldsymbol {\mathsf {F}}}(Y)} ;
T ( ¬ X ) {\displaystyle {\boldsymbol {\mathsf {T}}}(\neg X)} , add to its leaf the node containing the formula F ( X ) {\displaystyle {\boldsymbol {\mathsf {F}}}(X)} ;
F ( ¬ X ) {\displaystyle {\boldsymbol {\mathsf {F}}}(\neg X)} , add to its leaf the node containing the formula T ( X ) {\displaystyle {\boldsymbol {\mathsf {T}}}(X)} . The breakdown process terminates after a finite number of steps, because each application of a rule eliminates a connective, and there are only finitely many connectives in any formula.
Note: In systems based on the grammar
Φ ::= ⊥ ∣ P V ∣ ( Φ → Φ ) ∣ ( Φ ∨ Φ ) ∣ ( Φ ∧ Φ ) {\displaystyle \Phi ::=\bot \mid PV\mid (\Phi \to \Phi )\mid (\Phi \lor \Phi )\mid (\Phi \land \Phi )} , that do not treat negation as primitive but define it in terms of implication and falsity ( ¬ Φ = def Φ → ⊥ {\displaystyle \neg \Phi \,{\overset {\text{def}}{=}}\,\Phi \to \bot } ),the tableau rules for ¬ {\displaystyle \neg } are replaced by
The principle of tableau is that formulae in nodes of the same branch are considered in conjunction while the different branches are considered to be disjuncted. As a result, a tableau is a tree-like representation of a formula that is a disjunction of conjunctions. This formula is equivalent to the set to prove unsatisfiability. The procedure modifies the tableau in such a way that the formula represented by the resulting tableau is equivalent to the original one. One of these conjunctions may contain a pair of complementary literals, in which case that conjunction is proved to be unsatisfiable. If all conjunctions are proved unsatisfiable, the original set of formulae is unsatisfiable.
Closure Every tableau can be considered as a graphical representation of a formula, which is equivalent to the set the tableau is built from. This formula is as follows: each branch of the tableau represents the conjunction of its formulae; the tableau represents the disjunction of its branches. The expansion rules transforms a tableau into one having an equivalent represented formula. Since the tableau is initialized as a single branch containing the formulae of the input set, all subsequent tableaux obtained from it represent formulae which are equivalent to that set (in the variant where the initial tableau is the single node labeled true, the formulae represented by tableaux are consequences of the original set.)
The method of tableaux works by starting with the initial set of formulae and then adding to the tableau simpler and simpler formulae until contradiction is shown in the simple form of opposite literals. Since the formula represented by a tableau is the disjunction of the formulae represented by its branches, contradiction is obtained when every branch contains a pair of opposite literals. Once a branch contains a literal and its negation, its corresponding formula is unsatisfiable. As a result, this branch can be now "closed", as there is no need to further expand it. If all branches of a tableau are closed, the formula represented by the tableau is unsatisfiable; therefore, the original set is unsatisfiable as well. Obtaining a tableau where all branches are closed is a way for proving the unsatisfiability of the original set. In the propositional case, one can also prove that satisfiability is proved by the impossibility of finding a closed tableau, provided that every expansion rule has been applied everywhere it could be applied. In particular, if a tableau contains some open (non-closed) branches and every formula that is not a literal has been used by a rule to generate a new node on every branch the formula is in, the set is satisfiable. This rule takes into account that a formula may occur in more than one branch (this is the case if there is at least a branching point "below" the node). In this case, the rule for expanding the formula has to be applied so that its conclusion(s) are appended to all of these branches that are still open, before one can conclude that the tableau cannot be further expanded and that the formula is therefore satisfiable.
Propositional tableau with unification The above rules for propositional tableau can be simplified by using uniform notation. In uniform notation, each formula is either of type α {\displaystyle \alpha } (alpha) or of type β {\displaystyle \beta } (beta). Each formula of type alpha is assigned the two components α 1 , α 2 {\displaystyle \alpha _{1},\alpha _{2}} , and each formula of type beta is assigned the two components β 1 , β 2 {\displaystyle \beta _{1},\beta _{2}} . Formulae of type alpha can be thought of as being conjunctive, as both α 1 {\displaystyle \alpha _{1}} and α 2 {\displaystyle \alpha _{2}} are implied by α {\displaystyle \alpha } being true. Formulae of type beta can be thought of as being disjunctive, as either β 1 {\displaystyle \beta _{1}} or β 2 {\displaystyle \beta _{2}} is implied by β {\displaystyle \beta } being true. The below tables shows how to determine the type, and the components, of any given propositional formula.
In each table, the left-most column shows all the possible structures for the formulae of type alpha or beta, and the right-most columns show their respective components. When constructing a propositional tableau using the above notation, whenever one encounters a formula of type alpha, its two components α 1 , α 2 {\displaystyle \alpha _{1},\alpha _{2}} are added to the current branch that is being expanded. Whenever one encounters a formula of type beta on some branch θ {\displaystyle \theta } , one can split θ {\displaystyle \theta } into two branches, one with the set { θ {\displaystyle \theta } , β 1 {\displaystyle \beta _{1}} } of formulae, and the other with the set { θ {\displaystyle \theta } , β 2 {\displaystyle \beta _{2}} } of formulae.
Set-labeled tableau A variant of tableau is to label nodes with sets of formulae rather than single formulae. In this case, the initial tableau is a single node labeled with the set to be proved satisfiable. The formulae in a set are therefore considered to be in conjunction. The rules of expansion of the tableau can now work on the leaves of the tableau, ignoring all internal nodes. For conjunction, the rule is based on the equivalence of a set containing a conjunction A ∧ B {\displaystyle A\land B} with the set containing both A {\displaystyle A} and B {\displaystyle B} in place of it. In particular, if a leaf is labeled with X ∪ { A ∧ B } {\displaystyle X\cup \{A\land B\}} , a node can be appended to it with label X ∪ { A , B } {\displaystyle X\cup \{A,B\}} :
( ∧ ) X ∪ { A ∧ B } X ∪ { A , B } {\displaystyle (\land ){\frac {X\cup \{A\land B\}}{X\cup \{A,B\}}}}
For disjunction, a set X ∪ { A ∨ B } {\displaystyle X\cup \{A\lor B\}} is equivalent to the disjunction of the two sets X ∪ { A } {\displaystyle X\cup \{A\}} and X ∪ { B } {\displaystyle X\cup \{B\}} . As a result, if the first set labels a leaf, two children can be appended to it, labeled with the latter two formulae.
( ∨ ) X ∪ { A ∨ B } X ∪ { A } | X ∪ { B } {\displaystyle (\lor ){\frac {X\cup \{A\lor B\}}{X\cup \{A\}|X\cup \{B\}}}}
Finally, if a set contains both a literal and its negation, this branch can be closed:
( i d ) X ∪ { p , ¬ p } c l o s e d {\displaystyle (id){\frac {X\cup \{p,\neg p\}}{closed}}}
A tableau for a given finite set X is a finite (upside down) tree with root X in which all child nodes are obtained by applying the tableau rules to their parents. A branch in such a tableau is closed if its leaf node contains "closed". A tableau is closed if all its branches are closed. A tableau is open if at least one branch is not closed. Below are two closed tableaux for the set
X = { r ∧ ¬ r , p ∧ ( ( ¬ p ∨ q ) ∧ ¬ q ) } {\displaystyle X=\{r\land \neg r,\;p\land ((\neg p\lor q)\land \neg q)\}}
Each rule application is marked at the right hand side. Both achieve the same effect; the first closes faster. The only difference is the order in which the reduction is performed.
r ∧ ¬ r , p ∧ ( ( ¬ p ∨ q ) ∧ ¬ q ) r , ¬ r , p ∧ ( ( ¬ p ∨ q ) ∧ ¬ q ) ( ∧ ) c l o s e d ( ∧ ) {\displaystyle {\dfrac {\quad {\dfrac {\quad r\land \neg r,\;p\land ((\neg p\lor q)\land \neg q)\quad }{r,\;\neg r,\;p\land ((\neg p\lor q)\land \neg q)}}(\land )}{closed}}(\land )}
and second, longer one, with the rules applied in a different order:
r ∧ ¬ r , p ∧ ( ( ¬ p ∨ q ) ∧ ¬ q ) r ∧ ¬ r , p , ( ( ¬ p ∨ q ) ∧ ¬ q ) ( ∧ ) r ∧ ¬ r , p , ( ¬ p ∨ q ) , ¬ q ( ∧ ) r ∧ ¬ r , p , ¬ p , ¬ q c l o s e d ( i d ) r ∧ ¬ r , p , q , ¬ q c l o s e d ( i d ) ( ∨ ) {\displaystyle {\dfrac {\quad {\dfrac {\quad {\dfrac {\quad r\land \neg r,\;p\land ((\neg p\lor q)\land \neg q)\quad }{r\land \neg r,\;p,\;((\neg p\lor q)\land \neg q)}}(\land )\quad }{r\land \neg r,\;p,\;(\neg p\lor q),\;\neg q}}(\land )}{\quad {\dfrac {\quad r\land \neg r,\;p,\;\neg p,\;\neg q\quad }{closed}}(id)\quad \quad {\dfrac {\quad r\land \neg r,\;p,\;q,\;\neg q\quad }{closed}}(id)}}(\lor )}
The first tableau closes after only one rule application while the second one misses the mark and takes much longer to close. Clearly, one would prefer to always find the shortest closed tableau but it can be shown that one single algorithm that finds the shortest closed tableau for all input sets of formulae cannot exist. The three rules ( ∧ ) {\displaystyle (\land )} , ( ∨ ) {\displaystyle (\lor )} and ( i d ) {\displaystyle (id)} given above are then enough to decide whether a given set X ′ {\displaystyle X'} of formulae in negated normal form are jointly satisfiable:
Just apply all possible rules in all possible orders until we find a closed tableau for X ′ {\displaystyle X'} or until we exhaust all possibilities and conclude that every tableau for X ′ {\displaystyle X'} is open.
In the first case, X ′ {\displaystyle X'} is jointly unsatisfiable and in the second the case the leaf node of the open branch gives an assignment to the atomic formulae and negated atomic formulae which makes X ′ {\displaystyle X'} jointly satisfiable. Classical logic actually has the rather nice property that we need to investigate only (any) one tableau completely: if it closes then X ′ {\displaystyle X'} is unsatisfiable and if it is open then X ′ {\displaystyle X'} is satisfiable. But this property is not generally enjoyed by other logics. These rules suffice for all of classical logic by taking an initial set of formulae X and replacing each member C by its logically equivalent negated normal form C' giving a set of formulae X' . We know that X is satisfiable if and only if X' is satisfiable, so it suffices to search for a closed tableau for X' using the procedure outlined above. By setting X = { ¬ A } {\displaystyle X=\{\neg A\}} one can test whether the formula A is a tautology of classical logic:
If the tableau for { ¬ A } {\displaystyle \{\neg A\}} closes then ¬ A {\displaystyle \neg A} is unsatisfiable and so A is a tautology since no assignment of truth values will ever make A false. Otherwise any open leaf of any open branch of any open tableau for { ¬ A } {\displaystyle \{\neg A\}} gives an assignment that falsifies A.
First-order logic tableau Tableaux are extended to first-order predicate logic by two rules for dealing with universal and existential quantifiers, respectively. Two different sets of rules can be used; both employ a form of Skolemization for handling existential quantifiers, but differ on the handling of universal quantifiers. The set of formulae to check for validity is here supposed to contain no free variables; this is not a limitation as free variables are implicitly universally quantified, so universal quantifiers over these variables can be added, resulting in a formula with no free variables.
First-order tableau without unification A first-order formula ∀ x . γ ( x ) {\displaystyle \forall x.\gamma (x)} implies all formulae γ ( t ) {\displaystyle \gamma (t)} where t {\displaystyle t} is a ground term. The following inference rule is therefore correct:
( ∀ ) ∀ x . γ ( x ) γ ( t ) {\displaystyle (\forall ){\frac {\forall x.\gamma (x)}{\gamma (t)}}} where t {\displaystyle t} is an arbitrary ground term Contrarily to the rules for the propositional connectives, multiple applications of this rule to the same formula may be necessary. As an example, the set { ¬ P ( a ) ∨ ¬ P ( b ) , ∀ x . P ( x ) } {\displaystyle \{\neg P(a)\lor \neg P(b),\forall x.P(x)\}} can only be proved unsatisfiable if both P ( a ) {\displaystyle P(a)} and P ( b ) {\displaystyle P(b)} are generated from ∀ x . P ( x ) {\displaystyle \forall x.P(x)} . Existential quantifiers are dealt with by means of Skolemization. In particular, a formula with a leading existential quantifier like ∃ x . δ ( x ) {\displaystyle \exists x.\delta (x)} generates its Skolemization δ ( c ) {\displaystyle \delta (c)} , where c {\displaystyle c} is a new constant symbol.
( ∃ ) ∃ x . δ ( x ) δ ( c ) {\displaystyle (\exists ){\frac {\exists x.\delta (x)}{\delta (c)}}} where c {\displaystyle c} is a new constant symbol
The Skolem term c {\displaystyle c} is a constant (a function of arity 0) because the quantification over x {\displaystyle x} does not occur within the scope of any universal quantifier. If the original formula contained some universal quantifiers such that the quantification over x {\displaystyle x} was within their scope, these quantifiers have evidently been removed by the application of the rule for universal quantifiers. The rule for existential quantifiers introduces new constant symbols. These symbols can be used by the rule for universal quantifiers, so that ∀ y . γ ( y ) {\displaystyle \forall y.\gamma (y)} can generate γ ( c ) {\displaystyle \gamma (c)} even if c {\displaystyle c} was not in the original formula but is a Skolem constant created by the rule for existential quantifiers. The above two rules for universal and existential quantifiers are correct, and so are the propositional rules: if a set of formulae generates a closed tableau, this set is unsatisfiable. Completeness can also be proved: if a set of formulae is unsatisfiable, there exists a closed tableau built from it by these rules. However, actually finding such a closed tableau requires a suitable policy of application of rules. Otherwise, an unsatisfiable set can generate an infinite-growing tableau. As an example, the set { ¬ P ( f ( c ) ) , ∀ x . P ( x ) } {\displaystyle \{\neg P(f(c)),\forall x.P(x)\}} is unsatisfiable, but a closed tableau is never obtained if one unwisely keeps applying the rule for universal quantifiers to ∀ x . P ( x ) {\displaystyle \forall x.P(x)} , generating for example P ( c ) , P ( f ( c ) ) , P ( f ( f ( c ) ) ) , … {\displaystyle P(c),P(f(c)),P(f(f(c))),\ldots } . A closed tableau can always be found by ruling out this and similar "unfair" policies of application of tableau rules. The rule for universal quantifiers ( ∀ ) {\displaystyle (\forall )} is the only non-deterministic rule, as it does not specify which term to instantiate with. Moreover, while the other rules need to be applied only once for each formula and each path the formula is in, this one may require multiple applications. Application of this rule can however be restricted by delaying the application of the rule until no other rule is applicable and by restricting the application of the rule to ground terms t