\documentclass[12pt]{article}
\usepackage{fullpage}
\usepackage{times}
\usepackage{amsmath,amsfonts,amssymb,amsthm}
\usepackage{qtree}

\newcommand{\closed}{\mathbf{\times}}

\begin{document}
\bibliographystyle{plain}

\paragraph{CS81 Spring 2012} {\sc Analytic Tableaux} 

\vspace{.2in}

Smullyan \cite{smullyan} introduced an elegant proof procedure called the {\bf analytic tableaux}.
He attributed the idea of this method to earlier works by Beth and Hintikka.
With this method, to prove a formula $\alpha$, we assume $\lnot\alpha$ and derive a contradiction
from this assumption by constructing a {\em refutation} tree.

The refutation tree contains vertices which are labeled by logical formulas.
The root of the tree is labeled with the formula $\lnot\alpha$.
Given a vertex $u$ of the tree labeled with a formula $\beta$, the children of $u$
is constructed based on the form of $\beta$ by using the rules given below. 
A leaf $v$ is called {\bf closed} if,
for some formula $\psi$, both $\psi$ and $\lnot\psi$ appear along the unique path from
the root to $v$. The refutation tree is {\bf complete} if all leaves are closed.

\paragraph{Rules for Tableaux Construction}
\begin{enumerate}
\item {\em Negation} rule:
\Tree [.{$\lnot\lnot \alpha$}
	[.{$\alpha$} ]
]


\item {\em Conjunction} rule:
\Tree [.{$\alpha \wedge \beta$}
	[.{ $\alpha$ \\ $\beta$} ]
]
\Tree [.{$\lnot(\alpha \wedge \beta)$} 
	[.{$\lnot\alpha $} ] 
	[.{$\lnot\beta$} ]
]

\item {\em Disjunction} rule:
\Tree [.{$\lnot(\alpha \vee \beta)$}
	[.{$\lnot\alpha$ \\ $\lnot\beta$} ]
]
\Tree [.{$\alpha \vee \beta$} 
	[.{$\alpha $} ] 
	[.{$\beta$} ]
]

\item {\em Implication} rule:
\Tree [.{$\lnot(\alpha \to \beta)$}
	[.{$\alpha$ \\ $\lnot\beta$} ]
]
\Tree [.{$\alpha \to \beta$} 
	[.{$\lnot\alpha $} ] 
	[.{$\beta$} ]
]

\item {\em Universal} $\forall$-rule: 
\Tree [.{$(\forall x)\alpha$} 
	[.{$\alpha[a/x]$} ] 
]
\Tree [.{$\lnot(\exists x)\alpha$} 
	[.{$\lnot\alpha[a/x]$} ] 
]

\par\noindent
provided $a$ is {\em any} parameter\footnote{In \cite{smullyan}, Smullyan
used {\em parameter} to denote what may be called a {\em constant} (see page 43).}.

\item {\em Existential} $\exists$-rule: 
\Tree [.{$(\exists x)\alpha$} 
	[.{$\alpha[a/x]$} ] 
]
\Tree [.{$\lnot(\forall x)\alpha$} 
	[.{$\lnot\alpha[a/x]$} ] 
]

\par\noindent
provided $a$ is a {\em new} parameter.
In \cite{smullyan}, Smullyan mentioned that the $\exists$-rule can be {\em liberalized}
by replacing the clause ``provided $a$ is a new parameter'' by
``provided $a$ is new, or else $a$ has not been previously introduced by an $\exists$-rule,
and does not occur in $(\exists x)\alpha$, and no parameter of $(\exists x)\alpha$ has been
previously introduced by an $\exists$-rule.''

\end{enumerate}


\newpage
\paragraph{Example 1} Proving the Distributive Law: 
\[
	a \vee (b \wedge c) \vdash (a \vee b) \wedge (a \vee c).
\]
The refutation tree is given by:

\Tree
[.{
  $\lnot [a \vee (b \wedge c) \to (a \vee b) \wedge (a \vee c)]$
  }
  [.{
	$\checkmark (a \vee (b \wedge c))$ \\
	$\checkmark \lnot((a \vee b) \wedge (a \vee c))$
	}
	[.{
	  $\checkmark a$
	  }
	  [.{
		$\checkmark \lnot(a \vee b)$ \\
		$\checkmark \lnot a$ \\
		$\lnot b$ \\
		$\closed$
		}
	  ]
	  [.{
		$\checkmark \lnot(a \vee c)$ \\
		$\checkmark \lnot a$ \\
		$\lnot c$ \\
		$\closed$
		}
	  ]
	]
	[.{
	  $\checkmark (b \wedge c)$ \\
	  $\checkmark b$ \\
	  $\checkmark c$
	  }
	  [.{
		$\checkmark \lnot(a \vee b)$ \\
		$\lnot a$ \\
		$\checkmark \lnot b$ \\
		$\closed$
		}
	  ]
	  [.{
		$\checkmark \lnot(a \vee c)$ \\
		$\lnot a$ \\
		$\checkmark \lnot c$ \\
		$\closed$
		}
	  ]
	]
  ]
]

\par\noindent
The (optional) {\em checkmark}s are to denote formulas which are {\em used} 
in some step along some branch in the tree.


\paragraph{Example 2} Proving DeMorgan's Law:
\[
	\lnot(\exists x)\lnot A(x) \vdash (\forall x)A(x)
\]
The refutation tree is given by:

\Tree
[.{$\lnot[\lnot(\exists x)\lnot A(x) \to (\forall x)A(x)]$}
  [.{$\checkmark \lnot (\exists x)\lnot A(x)$ \\ $\checkmark \lnot(\forall x)A(x)$}
    [.{$\checkmark \lnot A(\hat{a})$ \\ $\checkmark A(\hat{a})$ \\ $\closed$} ]
  ] 
]


\newpage
\paragraph{Example 3} (from Smullyan \cite{smullyan}) Proving the sentence 
$(\exists y)[(\exists x)A(x) \to A(y)]$ using the strict $\exists$-rule.

\Tree
[.{$\lnot (\exists y)[(\exists x)A(x) \to A(y)]$}
  [.{$\lnot [(\exists x)A(x) \to A(a)]$}
    [.{$(\exists x)A(x)$ \\ $\lnot A(a)$}
     [.{$A(b)$}
      [.{$\lnot [(\exists x)A(x) \to A(b)]$}
       [.{$(\exists x)A(x)$ \\ $\lnot A(b)$ \\ $\closed$}
       ]
      ]
     ]
    ]
  ]
]

Now, using the liberalized $\exists$-rule:

\Tree
[.{$\lnot (\exists y)[(\exists x)A(x) \to A(y)]$}
  [.{$\lnot [(\exists x)A(x) \to A(a)]$}
   [.{$(\exists x)A(x)$ \\ $\lnot A(a)$}
    [.{$A(a)$ \\ $\closed$}
    ]
   ]
  ]
]



\begin{thebibliography}{99}

\bibitem{smullyan}
R. Smullyan, {\em First-Order Logic}, Dover, 1968.

\end{thebibliography}

\end{document}



