Definition:Propositional Tableau/Identification

From ProofWiki
Jump to navigation Jump to search

Definition

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