# Definition:Propositional Tableau

## Definition

Propositional tableaus are a specific subset of the labeled trees for propositional logic.

### Identification

Let $\left({T, \mathbf H, \Phi}\right)$ be a labeled tree for propositional logic.

Then $T$ is a propositional tableau iff 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$ $\Phi \left({s}\right) = \mathbf A$ $\boxed \land$ $t$ has precisely one child $s$, and one grandchild $r$ $\mathbf C$ is $\mathbf A \land \mathbf B$ $\Phi \left({s}\right) = \mathbf A$ and $\Phi \left({r}\right) = \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 \left({\mathbf A \land \mathbf B}\right)$ $\Phi \left({s}\right) = \mathbf A$ and $\Phi \left({s'}\right) = \mathbf B$ $\boxed \lor$ $t$ has precisely two children $s$ and $s'$ $\mathbf C$ is $\mathbf A \lor \mathbf B$ $\Phi \left({s}\right) = \mathbf A$ and $\Phi \left({s'}\right) = \mathbf B$ $\boxed{\neg\lor}$ $t$ has precisely one child $s$, and one grandchild $r$ $\mathbf C$ is $\neg \left({\mathbf A \lor \mathbf B}\right)$ $\Phi \left({s}\right) = \neg\mathbf A$ and $\Phi \left({r}\right) = \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$ $\Phi \left({s}\right) = \neg\mathbf A$ and $\Phi \left({s'}\right) = \mathbf B$ $\boxed{\neg\implies}$ $t$ has precisely one child $s$, and one grandchild $r$ $\mathbf C$ is $\neg \left({\mathbf A \implies \mathbf B}\right)$ $\Phi \left({s}\right) = \mathbf A$ and $\Phi \left({r}\right) = \neg\mathbf B$ $\boxed \iff$ $t$ has precisely two children $s$ and $s'$ $\mathbf C$ is $\mathbf A \iff \mathbf B$ $\Phi \left({s}\right) = \mathbf A \land \mathbf B$ and $\Phi \left({s'}\right) = \neg\mathbf A \land \neg\mathbf B$ $\boxed{\neg\iff}$ $t$ has precisely two children $s$ and $s'$ $\mathbf C$ is $\neg \left({\mathbf A \iff \mathbf B}\right)$ $\Phi \left({s}\right) = \mathbf A \land \neg \mathbf B$ and $\Phi \left({s'}\right) = \neg\mathbf A \land \mathbf B$

Note how the boxes give an indication of the shape of the relevant ancestor WFF $\mathbf C$.

#### Finite Propositional Tableau

The finite propositional tableaus 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$ is a finite propositional tableau. $\boxed \land$ If $\mathbf A \land \mathbf B$ 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$ a child $r$ to $s$, with $\Phi \left({r}\right) = \mathbf B$ is a finite propositional tableau. $\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: a child $s$ to $t$, with $\Phi \left({s}\right) = \neg\mathbf A$ another child $s'$ to $t$, with $\Phi \left({s'}\right) = \neg\mathbf B$ is a finite propositional tableau. $\boxed \lor$ If $\mathbf A \lor \mathbf B$ 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$ another child $s'$ to $t$, with $\Phi \left({s'}\right) = \mathbf B$ is a finite propositional tableau. $\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: a child $s$ to $t$, with $\Phi \left({s}\right) = \neg\mathbf A$ a child $r$ to $s$, with $\Phi \left({r}\right) = \neg \mathbf B$ is a finite propositional tableau. $\boxed \implies$ If $\mathbf A \implies \mathbf B$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding: a child $s$ to $t$, with $\Phi \left({s}\right) = \neg\mathbf A$ another child $s'$ to $t$, with $\Phi \left({s'}\right) = \mathbf B$ is a finite propositional tableau. $\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: a child $s$ to $t$, with $\Phi \left({s}\right) = \mathbf A$ a child $r$ to $s$, with $\Phi \left({r}\right) = \neg \mathbf B$ is a finite propositional tableau. $\boxed \iff$ If $\mathbf A \iff \mathbf B$ 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 \land \mathbf B$ another child $s'$ to $t$, with $\Phi \left({s'}\right) = \neg \mathbf A \land \neg\mathbf B$ is a finite propositional tableau. $\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: a child $s$ to $t$, with $\Phi \left({s}\right) = \mathbf A \land \neg \mathbf B$ another child $s'$ to $t$, with $\Phi \left({s'}\right) = \neg \mathbf A \land \mathbf B$ is a finite propositional tableau.

Note how the boxes give an indication of the ancestor WFF mentioned in the clause.

These clauses together are called the tableau extension rules.

#### Infinite Propositional Tableau

An infinite labeled tree $\left({T, \mathbf H, \Phi}\right)$ is a propositional tableau if and only if:

There exists an exhausting sequence of sets $\left({T_n}\right)_{n \in \N}$ of $T$ such that for all $n \in \N$:
$\left({T_n, \mathbf H, \Phi \restriction_{T_n}}\right)$
is a finite propositional tableau, where $\Phi \restriction_{T_n}$ denotes the restriction of $\Phi$ to $T_n$.

## 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{ \[email protected]{.}[d] & \[email protected]{.}[d] & \[email protected]{.}[d] & \[email protected]{.}[d] \\ *++{\neg \neg \mathbf A} \[email protected]{.}[d] & *++{\mathbf A \land \mathbf B} \[email protected]{.}[d] & *++{\neg \left({\mathbf A \lor \mathbf B}\right)} \[email protected]{.}[d] & *++{\neg \left({\mathbf A \implies \mathbf B}\right)} \[email protected]{.}[d] \\ *++{t} \[email protected]{-}[d] & *++{t} \[email protected]{-}[d] & *++{t} \[email protected]{-}[d] & *++{t} \[email protected]{-}[d] \\ \mathbf A & \mathbf A \[email protected]{=}[d] & \neg \mathbf A \[email protected]{=}[d] & \mathbf A \[email protected]{=}[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{ & \[email protected]{.}[d] & & & & & & \[email protected]{.}[d] & & & & & & \[email protected]{.}[d] \\ & *++{\mathbf A \lor \mathbf B} \[email protected]{.}[d] & & & & & & *++{\neg \left({\mathbf A \land \mathbf B}\right)} \[email protected]{.}[d] & & & & & & *++{\mathbf A \implies \mathbf B} \[email protected]{.}[d] \\ & *++{t} \[email protected]{-}[dl] \[email protected]{-}[dr] & & & & & & *++{t} \[email protected]{-}[dl] \[email protected]{-}[dr] & & & & & & *++{t} \[email protected]{-}[dl] \[email protected]{-}[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{ & \[email protected]{.}[d] & & & & & & \[email protected]{.}[d] \\ & *++{\mathbf A \iff \mathbf B} \[email protected]{.}[d] & & & & & & *++{\neg \left({\mathbf A \iff \mathbf B}\right)} \[email protected]{.}[d] \\ & *++{t} \[email protected]{-}[dl] \[email protected]{-}[dr] & & & & & & *++{t} \[email protected]{-}[dl] \[email protected]{-}[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 tableaus can be found here.