Definition:Propositional Tableau
Definition
Propositional tableaux are a specific subset of the labeled trees for propositional logic.
Identification
Let $\struct {T, \mathbf H, \Phi}$ be a labeled tree for propositional logic.
Then $T$ is a propositional tableau if and only if for each node $t$ of $T$ that is not a leaf node:
- There exists an ancestor WFF $\mathbf C$ of $t$ such that one of the following conditions holds:
$\boxed{\neg \neg}$ $t$ has precisely one child $s$ $\mathbf C$ is $\neg \neg \mathbf A$
$\map \Phi s = \mathbf A$
$\boxed \land$ $t$ has precisely one child $s$, and one grandchild $r$ $\mathbf C$ is $\mathbf A \land \mathbf B$
$\map \Phi s = \mathbf A$ and $\map \Phi r = \mathbf B$
$\boxed{\land'}$ The parent of $t$ satisfies $\boxed\land$ $\boxed{\neg \land}$ $t$ has precisely two children $s$ and $s'$ $\mathbf C$ is $\neg \paren {\mathbf A \land \mathbf B}$
$\map \Phi s = \mathbf A$ and $\map \Phi {s'} = \mathbf B$
$\boxed \lor$ $t$ has precisely two children $s$ and $s'$ $\mathbf C$ is $\mathbf A \lor \mathbf B$
$\map \Phi s = \mathbf A$ and $\map \Phi {s'} = \mathbf B$
$\boxed{\neg \lor}$ $t$ has precisely one child $s$, and one grandchild $r$ $\mathbf C$ is $\neg \paren {\mathbf A \lor \mathbf B}$
$\map \Phi s = \neg \mathbf A$ and $\map \Phi r = \neg \mathbf B$
$\boxed{\neg \lor'}$ The parent of $t$ satisfies $\boxed{\neg \lor}$ $\boxed \implies$ $t$ has precisely two children $s$ and $s'$ $\mathbf C$ is $\mathbf A \implies \mathbf B$
$\map \Phi s = \neg \mathbf A$ and $\map \Phi {s'} = \mathbf B$
$\boxed{\neg \implies}$ $t$ has precisely one child $s$, and one grandchild $r$ $\mathbf C$ is $\neg \paren {\mathbf A \implies \mathbf B}$
$\map \Phi s = \mathbf A$ and $\map \Phi r = \neg \mathbf B$
$\boxed \iff$ $t$ has precisely two children $s$ and $s'$ $\mathbf C$ is $\mathbf A \iff \mathbf B$
$\map \Phi s = \mathbf A \land \mathbf B$ and $\map \Phi {s'} = \neg \mathbf A \land \neg \mathbf B$
$\boxed{\neg \iff}$ $t$ has precisely two children $s$ and $s'$ $\mathbf C$ is $\neg \paren {\mathbf A \iff \mathbf B}$
$\map \Phi s = \mathbf A \land \neg \mathbf B$ and $\map \Phi {s'} = \neg \mathbf A \land \mathbf B$
Note how the boxes give an indication of the shape of the relevant ancestor WFF $\mathbf C$.
Construction
The finite propositional tableaux are precisely those labeled trees singled out by the following bottom-up grammar:
$\boxed{\mathrm{Root}}$ A labeled tree whose only node is its root node is a finite propositional tableau. For the following clauses, let $t$ be a leaf node of a finite propositional tableau $T$. $\boxed{\neg \neg}$ If $\neg \neg \mathbf A$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding: - a child $s$ to $t$, with $\Phi \left({s}\right) = \mathbf A$
$\boxed \land$ If $\mathbf A \land \mathbf B$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding: $\boxed{\neg \land}$ If $\neg \left({\mathbf A \land \mathbf B}\right)$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding: $\boxed \lor$ If $\mathbf A \lor \mathbf B$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding: $\boxed{\neg\lor}$ If $\neg \left({\mathbf A \lor \mathbf B}\right)$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding: $\boxed \implies$ If $\mathbf A \implies \mathbf B$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding: $\boxed{\neg\implies}$ If $\neg \left({\mathbf A \implies \mathbf B}\right)$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding: $\boxed \iff$ If $\mathbf A \iff \mathbf B$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding: $\boxed{\neg\iff}$ If $\neg \left({\mathbf A \iff \mathbf B}\right)$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding:
Note how the boxes give an indication of the ancestor WFF mentioned in the clause.
These clauses together are called the tableau extension rules.
Graphical Representation
The conditions by which a propositional tableau may be identified, respectively constructed, can be graphically represented like so:
$\begin{xy}\xymatrix @R=1em @C=3em{ \ar@{.}[d] & \ar@{.}[d] & \ar@{.}[d] & \ar@{.}[d] \\ *++{\neg \neg \mathbf A} \ar@{.}[d] & *++{\mathbf A \land \mathbf B} \ar@{.}[d] & *++{\neg \left({\mathbf A \lor \mathbf B}\right)} \ar@{.}[d] & *++{\neg \left({\mathbf A \implies \mathbf B}\right)} \ar@{.}[d] \\ *++{t} \ar@{-}[d] & *++{t} \ar@{-}[d] & *++{t} \ar@{-}[d] & *++{t} \ar@{-}[d] \\ \mathbf A & \mathbf A \ar@{=}[d] & \neg \mathbf A \ar@{=}[d] & \mathbf A \ar@{=}[d] \\ & \mathbf B & \neg \mathbf B & \neg \mathbf B \\ \boxed{\neg\neg} & \boxed \land & \boxed{\neg\lor} & \boxed{\neg\implies} }\end{xy}$ $\begin{xy}\xymatrix @R=1em @C=1em{ & \ar@{.}[d] & & & & & & \ar@{.}[d] & & & & & & \ar@{.}[d] \\ & *++{\mathbf A \lor \mathbf B} \ar@{.}[d] & & & & & & *++{\neg \left({\mathbf A \land \mathbf B}\right)} \ar@{.}[d] & & & & & & *++{\mathbf A \implies \mathbf B} \ar@{.}[d] \\ & *++{t} \ar@{-}[dl] \ar@{-}[dr] & & & & & & *++{t} \ar@{-}[dl] \ar@{-}[dr] & & & & & & *++{t} \ar@{-}[dl] \ar@{-}[dr] \\ \mathbf A & & \mathbf B & & & & \neg \mathbf A & & \neg \mathbf B & & & & \neg \mathbf A & & \mathbf B \\ & \boxed{\lor} & & & & & & \boxed{\neg \land} & & & & & & \boxed \implies }\end{xy}$ $\begin{xy}\xymatrix @R=1em @C=0.7em{ & \ar@{.}[d] & & & & & & \ar@{.}[d] \\ & *++{\mathbf A \iff \mathbf B} \ar@{.}[d] & & & & & & *++{\neg \left({\mathbf A \iff \mathbf B}\right)} \ar@{.}[d] \\ & *++{t} \ar@{-}[dl] \ar@{-}[dr] & & & & & & *++{t} \ar@{-}[dl] \ar@{-}[dr] \\ *++{\mathbf A \land \mathbf B} & & *++{\neg \mathbf A \land \neg \mathbf B} & & & & *++{\mathbf A \land \neg \mathbf B} & & *++{\neg \mathbf A \land \mathbf B} \\ & \boxed{\iff} & & & & & & \boxed{\neg \iff} }\end{xy}$
Also see
- Results about propositional tableaux can be found here.
Linguistic Note
The word tableau originates from the French language, where it means array, display, or table (in the sense of data presentation).
Hence the plural form of tableau is tableaux, although the US generally uses tableaus.
Tableaux is the preferred form on $\mathsf{Pr} \infty \mathsf{fWiki}$.
Sources
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.7$: Tableaus