Editing Method of analytic tableaux (section)

=== 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 <math>\alpha </math> (alpha) or of type <math>\beta </math> (beta). Each formula of type alpha is assigned the two components <math>\alpha_1, \alpha_2</math>, and each formula of type beta is assigned the two components <math>\beta_1, \beta_2</math>. Formulae of type alpha can be thought of as being conjunctive, as both <math>\alpha_1</math> and <math>\alpha_2</math> are implied by <math>\alpha</math> being true. Formulae of type beta can be thought of as being disjunctive, as either <math>\beta_1</math> or <math>\beta_2</math> is implied by <math>\beta</math> being true. The below tables shows how to determine the type, and the components, of any given [[propositional formula]].{{sfn|Smullyan|1995|pages=21-22}}
{|
| valign="top"| <math>\begin{array}{c|c|c}
\alpha & \alpha_1 & \alpha_2 \\
\hline
\boldsymbol{\mathsf{T}}(X \land Y) & \boldsymbol{\mathsf{T}} ( X ) & \boldsymbol{\mathsf{T}} ( Y )\\
\boldsymbol{\mathsf{F}}(X \lor Y) & \boldsymbol{\mathsf{F}} ( X ) & \boldsymbol{\mathsf{F}} ( Y )\\
\boldsymbol{\mathsf{F}}(X \to Y) & \boldsymbol{\mathsf{T}} ( X ) & \boldsymbol{\mathsf{F}} ( Y )\\
\boldsymbol{\mathsf{T}}(\neg X) & \boldsymbol{\mathsf{F}} ( X ) & \boldsymbol{\mathsf{F}} ( X )\\
\boldsymbol{\mathsf{F}}(\neg X) & \boldsymbol{\mathsf{T}} ( X ) & \boldsymbol{\mathsf{T}} ( X )\\
\end{array}</math> || {{Spaces|3}} || valign="top" | <math>\begin{array}{c|c|c}
\beta & \beta_1 & \beta_2 \\
\hline
\boldsymbol{\mathsf{F}}(X \land Y) & \boldsymbol{\mathsf{F}} ( X ) & \boldsymbol{\mathsf{F}} ( Y )\\
\boldsymbol{\mathsf{T}}(X \lor Y) & \boldsymbol{\mathsf{T}} ( X ) & \boldsymbol{\mathsf{T}} ( Y )\\
\boldsymbol{\mathsf{T}}(X \to Y) & \boldsymbol{\mathsf{F}} ( X ) & \boldsymbol{\mathsf{T}} ( Y )\\
\end{array}</math>
|}
<!--
{|
| valign="top" | <math>\begin{array}{c|c|c}
\alpha & \alpha_1 & \alpha_2 \\
\hline
X \land Y & X & Y \\
\neg(X \lor Y) & \neg X & \neg Y \\
\neg(X \to Y) & X & \neg Y \\
\neg\neg X & X & X \\
\end{array}</math> || {{Spaces|3}} || valign="top" | <math>\begin{array}{c|c|c}
\beta & \beta_1 & \beta_2 \\
\hline
\neg(X \land Y) & \neg X & \neg Y \\
X \lor Y & X & Y \\
X \to Y & \neg X & Y \\
\end{array}</math>
|}
-->
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 <math>\alpha_1,\alpha_2</math> are added to the current branch that is being expanded. Whenever one encounters a formula of type beta on some branch <math>\theta </math>, one can split <math>\theta </math> into two branches, one with the set {<math>\theta </math>, <math>\beta_1</math>} of formulae, and the other with the set {<math>\theta </math>, <math>\beta_2</math>} of formulae.{{sfn|Smullyan|2014|pages=88–89}}