Editing Method of analytic tableaux (section)

==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 [[Skolem normal form|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 <math>\forall x . \gamma(x)</math> implies all formulae <math>\gamma(t)</math> where <math>t</math> is a [[ground term]]. The following inference rule is therefore correct:

:<math>(\forall) \frac{\forall x . \gamma(x)}{\gamma(t)}</math> where <math>t</math> 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 <math>\{\neg P(a) \lor \neg P(b), \forall x . P(x)\}</math> can only be proved unsatisfiable if both <math>P(a)</math> and <math>P(b)</math> are generated from <math>\forall x . P(x)</math>.

Existential quantifiers are dealt with by means of Skolemization. In particular, a formula with a leading existential quantifier like <math>\exists x . \delta(x)</math> generates its Skolemization <math>\delta(c)</math>, where <math>c</math> is a new constant symbol.

:<math>(\exists) \frac{\exists x . \delta(x)}{\delta(c)}</math> where <math>c</math> is a new constant symbol

[[File:First-order tableau.svg|thumb|350px|A tableau without unification for {∀x.P(x),&nbsp;∃x.(¬P(x)⋁¬P(f(x)))}. For clarity, formulae are numbered on the left and the formula and rule used at each step is on the right.]]
The Skolem term <math>c</math> is a constant (a function of [[arity]] 0) because the quantification over <math>x</math> does not occur within the scope of any universal quantifier. If the original formula contained some universal quantifiers such that the quantification over <math>x</math> 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 <math>\forall y . \gamma(y)</math> can generate <math>\gamma(c)</math> even if <math>c</math> 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 <math>\{\neg P(f(c)), \forall x . P(x)\}</math> is unsatisfiable, but a closed tableau is never obtained if one unwisely keeps applying the rule for universal quantifiers to <math>\forall x . P(x)</math>, generating for example <math>P(c), P(f(c)), P(f(f(c))), \ldots</math>. 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 <math>(\forall)</math> 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 that already appear in the path of the tableau. The variant of tableaux with unification shown below aims at solving the problem of non-determinism.

===First-order tableau with unification===

The main problem of tableau without unification is how to choose a ground term <math>t</math> for the universal quantifier rule. Indeed, every possible ground term can be used, but clearly most of them might be useless for closing the tableau.

A solution to this problem is to "delay" the choice of the term to the time when the consequent of the rule allows closing at least a branch of the tableau. This can be done by using a variable instead of a term, so that <math>\forall x . \gamma(x)</math> generates <math>\gamma(x')</math>, and then allowing substitutions to later replace <math>x'</math> with a term. The rule for universal quantifiers becomes:

:<math>(\forall) \frac{\forall x . \gamma(x)}{\gamma(x')}</math> where <math>x'</math> is a variable not occurring everywhere else in the tableau

While the initial set of formulae is supposed not to contain free variables, a formula of the tableau may contain the free variables generated by this rule. These free variables are implicitly considered universally quantified.

This rule employs a variable instead of a ground term. What is gained by this change is that these variables can be then given a value when a branch of the tableau can be closed, solving the problem of generating terms that might be useless.

:{|
|-
| <math>(\sigma)</math>
| if <math>\sigma</math> is the most general unifier of two literals <math>A</math> and <math>B</math>, where <math>A</math> and the negation of <math>B</math> occur in the same branch of the tableau, <math>\sigma</math> can be applied at the same time to all formulae of the tableau
|}

As an example, <math>\{\neg P(a), \forall x . P(x)\}</math> can be proved unsatisfiable by first generating <math>P(x_1)</math>; the negation of this literal is unifiable with <math>\neg P(a)</math>, the most general unifier being the substitution that replaces <math>x_1</math> with <math>a</math>; applying this substitution results in replacing <math>P(x_1)</math> with <math>P(a)</math>, which closes the tableau.
 
This rule closes at least a branch of the tableau—the one containing the considered pair of literals. However, the substitution has to be applied to the whole tableau, not only on these two literals. This is expressed by saying that the free variables of the tableau are ''rigid'': if an occurrence of a variable is replaced by something else, all other occurrences of the same variable must be replaced in the same way. Formally, the free variables are (implicitly) universally quantified and all formulae of the tableau are within the scope of these quantifiers.

Existential quantifiers are dealt with by Skolemization. Contrary to the tableau without unification, Skolem terms may not be simple constants. Indeed, formulae in a tableau with unification may contain free variables, which are implicitly considered universally quantified. As a result, a formula like <math>\exists x . \delta(x)</math> may be within the scope of universal quantifiers; if this is the case, the [[Skolem term]] is not a simple constant but a term made of a new function symbol and the free variables of the formula.

:<math>(\exists) \frac{\exists x . \delta(x)}{\delta(f(x_1,\ldots,x_n))}</math> where <math>f</math> is a new function symbol and <math>x_1,\ldots,x_n</math> the free variables of <math>\delta</math>

[[File:First-order tableau with unification.svg|thumb|400px|A first-order tableau with unification for {∀x.P(x),&nbsp;∃x.(¬P(x)⋁¬P(f(x)))}. For clarity, formulae are numbered on the left and the formula and rule used at each step is on the right.]]
This rule incorporates a simplification over a rule where <math>x_1,\ldots,x_n</math> are the free variables of the branch, not of <math>\delta</math> alone. This rule can be further simplified by the reuse of a function symbol if it has already been used in a formula that is identical to <math>\delta</math> up to variable renaming.

The formula represented by a tableau is obtained in a way that is similar to the propositional case, with the additional assumption that free variables are considered universally quantified. As for the propositional case, formulae in each branch are conjoined and the resulting formulae are disjoined. In addition, all free variables of the resulting formula are universally quantified. All these quantifiers have the whole formula in their scope. In other words, if <math>F</math> is the formula obtained by disjoining the conjunction of the formulae in each branch, and <math>x_1,\ldots,x_n</math> are the free variables in it, then <math>\forall x_1,\ldots,x_n . F</math> is the formula represented by the tableau. The following considerations apply:

* The assumption that free variables are universally quantified is what makes the application of a most general unifier a sound rule: since <math>\gamma(x')</math> means that <math>\gamma</math> is true for every possible value of <math>x'</math>, then <math>\gamma(t)</math> is true for the term <math>t</math> that the most general unifier replaces <math>x</math> with.
* Free variables in a tableau are rigid: all occurrences of the same variable have to be replaced all with the same term. Every variable can be considered a symbol representing a term that is yet to be decided. This is a consequence of free variables being assumed universally quantified over the whole formula represented by the tableau: if the same variable occurs free in two different nodes, both occurrences are in the scope of the same quantifier. As an example, if the formulae in two nodes are <math>A(x)</math> and <math>B(x)</math>, where <math>x</math> is free in both, the formula represented by the tableau is something in the form <math>\forall x . (...A(x)...B(x)...)</math>. This formula implies that <math>(...A(x)...B(x)...)</math> is true for any value of <math>x</math>, but does not in general imply <math>(...A(t)...A(t')...)</math> for two different terms <math>t</math> and <math>t'</math>, as these two terms may in general take different values. This means that <math>x</math> cannot be replaced by two different terms in <math>A(x)</math> and <math>B(x)</math>.
* Free variables in a formula to check for validity are also considered universally quantified. However, these variables cannot be left free when building a tableau, because tableau rules works on the converse of the formula but still treats free variables as universally quantified. For example, <math>P(x) \to P(c)</math> is not valid (it is not true in the model where <math>D=\{1,2\}, P(1)=\bot, P(2)=\top, c=1</math>, and the interpretation where <math>x=2</math>). Consequently, <math>\{P(x),\neg P(c)\}</math> is satisfiable (it is satisfied by the same model and interpretation). However, a closed tableau could be generated with <math>P(x)</math> and <math>\neg P(c)</math>, and substituting <math>x</math> with <math>c</math> would generate a closure. A correct procedure is to first make universal quantifiers explicit, thus generating <math>\forall x . (P(x) \to P(c))</math>.

The following two variants are also correct.

* Applying to the whole tableau a substitution to the free variables of the tableau is a correct rule, provided that this substitution is free for the formula representing the tableau. In other worlds, applying such a substitution leads to a tableau whose formula is still a consequence of the input set.  Using most general unifiers automatically ensures that the condition of freeness for the tableau is met.
* While in general every variable has to be replaced with the same term in the whole tableau, there are some special cases in which this is not necessary.

Tableaux with unification can be proved complete: if a set of formulae is unsatisfiable, it has a tableau-with-unification proof. However, actually finding such a proof may be a difficult problem. Contrarily to the case without unification, applying a substitution can modify the existing part of a tableau; while applying a substitution closes at least a branch, it may make other branches impossible to close (even if the set is unsatisfiable).

A solution to this problem is ''delayed instantiation'': no substitution is applied until one that closes all branches at the same time is found. With this variant, a proof for an unsatisfiable set can always be found by a suitable policy of application of the other rules. This method however requires the whole tableau to be kept in memory: the general method closes branches, which can be then discarded, while this variant does not close any branch until the end.

The problem that some tableaux that can be generated are impossible to close even if the set is unsatisfiable is common to other sets of tableau expansion rules: even if some specific sequences of application of these rules allow constructing a closed tableau (if the set is unsatisfiable), some other sequences lead to tableaux that cannot be closed. General solutions for these cases are outlined in the "Searching for a tableau" section.