Definition:Propositional Tableau/Identification

From ProofWiki
Jump to: navigation, search

Definition

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$.