Editing Method of analytic tableaux (section)

===Set-labeled tableau===

A variant of tableau is to label nodes with sets of formulae rather than single formulae.{{sfn|Jarmużek|2020|pages=30-36}} 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 <math>A \land B</math> with the set containing both <math>A</math> and <math>B</math> in place of it. In particular, if a leaf is labeled with <math>X \cup \{A \land B\}</math>, a node can be appended to it with label <math>X \cup \{A, B\}</math>:

:<math>(\land) \frac{X \cup \{A \land B\}}{X \cup \{A, B\}}</math>

For disjunction, a set <math>X \cup \{A \lor B\}</math> is equivalent to the disjunction of the two sets <math>X \cup \{A\}</math> and <math>X \cup \{B\}</math>. As a result, if the first set labels a leaf, two children can be appended to it, labeled with the latter two formulae.

:<math>(\lor) \frac{X \cup \{A \lor B\}}{X \cup \{A\}|X \cup \{B\}}</math>

Finally, if a set contains both a literal and its negation, this branch can be closed:

:<math>(id) \frac{X \cup \{p, \neg p\}}{closed}</math>

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 
:<math>X = \{r \land \neg r,\; p \land ((\neg p \lor q) \land \neg q)\}</math>
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.

:<math>
\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)
</math>
and second, longer one, with the rules applied in a different order:
:<math>
\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)
</math>

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{{clarify|pre-text=all?|date=April 2025}} input sets of formulae cannot exist.{{disputed-inline|for=For a given '''finite''' set <math>X</math> of propositional formulae one can generate all {{mdash}} finitely many {{mdash}} possible tableaux and pick one with smallest height or width.|date=April 2025}}

The three rules <math>(\land)</math>, <math>(\lor)</math> and <math>(id)</math> given above are then enough to decide whether a given set <math>X'</math> of formulae in negated normal form are jointly satisfiable:
<blockquote>
Just apply all possible rules in all possible orders until we find a closed tableau for <math>X'</math> or until we exhaust all possibilities and conclude that every tableau for <math>X'</math> is open.
</blockquote>
In the first case, <math>X'</math> 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 <math>X'</math> jointly satisfiable. Classical logic actually has the rather nice property that we need to investigate only (any) one tableau completely: if it closes then <math>X'</math> is unsatisfiable and if it is open then <math>X'</math> 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 <math>X = \{\neg A\}</math> one can test whether the formula ''A'' is a [[tautology (logic)|tautology]] of classical logic: 
<blockquote>
If the tableau for <math>\{\neg A\}</math> closes then <math>\neg A</math> is unsatisfiable and so ''A'' is a tautology since no assignment of [[truth value]]s will ever make ''A'' false. Otherwise any open leaf of any open branch of any open tableau for <math>\{\neg A\}</math> gives an assignment that falsifies ''A''. 
</blockquote>