Definition:Propositional Tableau

From ProofWiki
Jump to navigation Jump to search

Definition

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


Identification

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


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{ \ar@{.}[d] & \ar@{.}[d] & \ar@{.}[d] & \ar@{.}[d] \\ *++{\neg \neg \mathbf A} \ar@{.}[d] & *++{\mathbf A \land \mathbf B} \ar@{.}[d] & *++{\neg \left({\mathbf A \lor \mathbf B}\right)} \ar@{.}[d] & *++{\neg \left({\mathbf A \implies \mathbf B}\right)} \ar@{.}[d] \\ *++{t} \ar@{-}[d] & *++{t} \ar@{-}[d] & *++{t} \ar@{-}[d] & *++{t} \ar@{-}[d] \\ \mathbf A & \mathbf A \ar@{=}[d] & \neg \mathbf A \ar@{=}[d] & \mathbf A \ar@{=}[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{ & \ar@{.}[d] & & & & & & \ar@{.}[d] & & & & & & \ar@{.}[d] \\ & *++{\mathbf A \lor \mathbf B} \ar@{.}[d] & & & & & & *++{\neg \left({\mathbf A \land \mathbf B}\right)} \ar@{.}[d] & & & & & & *++{\mathbf A \implies \mathbf B} \ar@{.}[d] \\ & *++{t} \ar@{-}[dl] \ar@{-}[dr] & & & & & & *++{t} \ar@{-}[dl] \ar@{-}[dr] & & & & & & *++{t} \ar@{-}[dl] \ar@{-}[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{ & \ar@{.}[d] & & & & & & \ar@{.}[d] \\ & *++{\mathbf A \iff \mathbf B} \ar@{.}[d] & & & & & & *++{\neg \left({\mathbf A \iff \mathbf B}\right)} \ar@{.}[d] \\ & *++{t} \ar@{-}[dl] \ar@{-}[dr] & & & & & & *++{t} \ar@{-}[dl] \ar@{-}[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.


Sources