Definition:Propositional Tableau/Graphical Representation

Definition

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

Sources

• 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.7$: Tableaus: Figure $1.4$