Definition:Propositional Tableau/Construction

Definition

Finite Propositional Tableau

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$ 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 $\struct {T, \mathbf H, \Phi}$ is a propositional tableau if and only if:

There exists an exhausting sequence of sets $\sequence {T_n}_{n \mathop \in \N}$ of $T$ such that for all $n \in \N$:

$\struct {T_n, \mathbf H, \Phi \restriction_{T_n} }$

is a finite propositional tableau, where $\Phi \restriction_{T_n}$ denotes the restriction of $\Phi$ to $T_n$.