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