Definition:Propositional Tableau/Identification

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

This article is complete as far as it goes, but it could do with expansion. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding this information. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Expand}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.