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

\newtheorem{theorem}{Claim}
\newcommand{\closed}{\mathbf{\times}}
\newcommand{\arrow}{\Rightarrow}

\begin{document}
\bibliographystyle{plain}

\paragraph{CS81 Spring 2012} {\sc Gentzen's Sequent Calculus} 

\vspace{.2in}

Gentzen introduced a proof procedure called the {\bf sequent calculus} as an extension of
his earlier natural deduction proof system. We follow a survey given by Buss \cite{buss98}.

In this method, each line in a proof is a {\em sequent} where a sequent is written in the form:
\[
	A_{1},\ldots,A_{m} \arrow B_{1},\ldots,B_{n}
\]
where the symbol $\arrow$ is a new symbol called the sequent arrow (not to be confused with the
implication symbol $\to$) and where $A_{i}$ and $B_{j}$ are formulas. 
The intentional meaning of the above sequent is that the conjunction of the $A_{i}$'s implies
the disjunction of the $B_{j}$'s. So, an equivalent way to write the above sequent is as the
following implication:
\[
	\bigwedge_{i=1}^{m} A_{i} \to \bigvee_{j=1}^{n} B_{j}.
\]
A standard convention for an empty conjunction ($m=0$) is it evaluates to $\top$ (True)
while an empty disjunction ($n=0$) evaluates to $\bot$ (False).
So, $\arrow A \equiv A$, $A \arrow \equiv \lnot A$, and the empty sequent $\arrow$ is
equivalent to $\bot$. 

The sequence of formulas $A_{1},\ldots,A_{m}$ is called the {\em antecedent} while the
sequence of formulas $B_{1},\ldots,B_{n}$ is called the {\em succedent}. Both of these
sequences are called {\em cedents}.

To prove a formula $\alpha$ in sequent calculus, we build a proof tree (much like the
tableaux method) by starting with a root labeled with $\alpha$ (at the bottom) and
constructing the tree upwards. The leaves of the tree are called the initial sequents
(axioms) which are logical axioms of the form $\beta \arrow \beta$.


\paragraph{Inference Rules for Sequent Calculus}
\begin{enumerate}
\item {\em Weakening} rules:
\begin{prooftree}
\AxiomC{$\Gamma \arrow \Delta$}
\LeftLabel{weakening left:}
\UnaryInfC{$A,\Gamma \arrow \Delta$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$\Gamma \arrow \Delta$}
\LeftLabel{weakening right:}
\UnaryInfC{$\Gamma \arrow \Delta,A$}
\end{prooftree}


\item {\em Exchange} rules:
\begin{prooftree}
\AxiomC{$\Gamma_{1},A,B,\Gamma_{2} \arrow \Delta$}
\LeftLabel{exchange left:}
\UnaryInfC{$\Gamma_{1},B,A,\Gamma_{2} \arrow \Delta$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$\Gamma \arrow \Delta_{1},A,B,\Delta_{2}$}
\LeftLabel{exchange right:}
\UnaryInfC{$\Gamma \arrow \Delta_{1},B,A,\Delta_{2}$}
\end{prooftree}


\item {\em Contraction} rules:
\begin{prooftree}
\AxiomC{$\Gamma,A,A \arrow \Delta$}
\LeftLabel{contraction left:}
\UnaryInfC{$\Gamma,A \arrow \Delta$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$\Gamma \arrow \Delta,A,A$}
\LeftLabel{contraction right:}
\UnaryInfC{$\Gamma \arrow \Delta,A$}
\end{prooftree}


\item {\em Negation Introduction} rules:
\begin{prooftree}
\AxiomC{$\Gamma \arrow \Delta,A$}
\LeftLabel{negation left:}
\UnaryInfC{$\lnot A,\Gamma \arrow \Delta$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$A,\Gamma \arrow \Delta$}
\LeftLabel{negation right:}
\UnaryInfC{$\Gamma \arrow \Delta,\lnot A$}
\end{prooftree}


\item {\em Conjunction Introduction} rules:
\begin{prooftree}
\AxiomC{$A,B,\Gamma \arrow \Delta$}
\LeftLabel{conjunction left:}
\UnaryInfC{$(A \wedge B),\Gamma \arrow \Delta$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$\Gamma \arrow \Delta,A$}
\AxiomC{$\Gamma \arrow \Delta,B$}
\LeftLabel{conjunction right:}
\BinaryInfC{$\Gamma \arrow \Delta,(A \wedge B)$}
\end{prooftree}


\item {\em Disjunction Introduction} rules:
\begin{prooftree}
\AxiomC{$A,\Gamma \arrow \Delta$}
\AxiomC{$B,\Gamma \arrow \Delta$}
\LeftLabel{disjunction left:}
\BinaryInfC{$(A \vee B),\Gamma \arrow \Delta$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$\Gamma \arrow \Delta,A,B$}
\LeftLabel{disjunction right:}
\UnaryInfC{$\Gamma \arrow \Delta,(A \vee B)$}
\end{prooftree}

\item {\em Implication Introduction} rules:
\begin{prooftree}
\AxiomC{$\Gamma \arrow \Delta, A$}
\AxiomC{$B,\Gamma \arrow \Delta$}
\LeftLabel{implication left:}
\BinaryInfC{$(A \to B),\Gamma \arrow \Delta$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$A, \Gamma \arrow \Delta, B$}
\LeftLabel{implication right:}
\UnaryInfC{$\Gamma \arrow \Delta, (A \to B)$}
\end{prooftree}


\item {\em Cut} rule:
\begin{prooftree}
\AxiomC{$\Gamma \arrow \Delta,A$}
\AxiomC{$A,\Gamma \arrow \Delta$}
\LeftLabel{cut:}
\BinaryInfC{$\Gamma \arrow \Delta$}
\end{prooftree}

\item {\em Universal Introduction} rules: 
\begin{prooftree}
\AxiomC{$A(t),\Gamma \arrow \Delta$}
\LeftLabel{$\forall$ left:}
\UnaryInfC{$(\forall x)A(x), \Gamma \arrow \Delta$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$\Gamma \arrow \Delta, A(a)$}
\LeftLabel{$\forall$ right:}
\UnaryInfC{$\Gamma \arrow \Delta,(\forall x)A(x)$}
\end{prooftree}

\item {\em Existential Introduction} rules: 
\begin{prooftree}
\AxiomC{$A(a),\Gamma \arrow \Delta$}
\LeftLabel{$\exists$ left:}
\UnaryInfC{$(\exists x)A(x), \Gamma \arrow \Delta$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$\Gamma \arrow \Delta, A(t)$}
\LeftLabel{$\exists$ right:}
\UnaryInfC{$\Gamma \arrow \Delta, (\exists x)A(x)$}
\end{prooftree}

\end{enumerate}
In the quantifier rules above,
$t$ is any term and $a$ is any free variable which must not appear
in $\Gamma$ and $\Delta$ (in $\forall$-right and $\exists$-left).

\paragraph{Free and Bound Variables}
The following is an excerpt from Buss' survey \cite{buss98}:
\begin{quote}
The first-order sequent calculus has two classes of variables, called {\em free variables}
and {\em bound variables}. There are infinitely many variables of each type; free variables
are denoted by metavariables $a,b,c,\ldots$, and bound variables by the metavariables
$z,y,x,\ldots$. The essential idea is that free variables may not be quantified, while
bound variables may not occur freely in formulas. The syntactic distinction between free
and bound variables necessitates a change to the definition of terms and formulas.
Firstly, {\em terms} are now defined as being built up from free variables and function
symbols; whereas, the {\em semiterms} are defined as being built up from free and bound
variables and function symbols. Secondly, only bound variables may ever be quantified.
The set of {\em formulas} is now redefined with the additional requirement that only
free variables may occur freely in formulas. {\em Semiformulas} are like formulas, except
that bound variables amy occur freely in semiformulas. We henceforth use $r,s,t,\ldots$
as metavariables for terms, and $A,B,C,\ldots$ as metavariables for formulas.
\end{quote}

\newpage
\paragraph{Example 1} Proving the Distributive Law: 
\[
(a \vee b) \wedge (a \vee c) \vdash a \vee (b \wedge c). 
\]
The proof (in complete form) of this law in sequent calculus is as follows:
\begin{prooftree}
\AxiomC{$a \arrow a$}
\UnaryInfC{$a \arrow a, b$}
\AxiomC{$b \arrow b$}
\UnaryInfC{$b \arrow b, a$}
\UnaryInfC{$b \arrow a, b$}
\BinaryInfC{$a \vee b \arrow a, b$}
\UnaryInfC{$a \vee c, a \vee b \arrow a, b$}
\UnaryInfC{$a \vee b, a \vee c \arrow a, b$}

\AxiomC{$a \arrow a$}
\UnaryInfC{$a \arrow a, c$}
\AxiomC{$c \arrow c$}
\UnaryInfC{$c \arrow c, a$}
\UnaryInfC{$c \arrow a, c$}
\BinaryInfC{$a \vee c \arrow a, c$}
\UnaryInfC{$a \vee b, a \vee c \arrow a, c$}

\BinaryInfC{$a \vee b, a \vee c \arrow a, b \wedge c$}
\UnaryInfC{$a \vee b, a \vee c \arrow a \vee (b \wedge c)$}
\UnaryInfC{$(a \vee b) \wedge (a \vee c) \arrow a \vee (b \wedge c)$}
\end{prooftree}
A more abbreviated form of the above proof is (with some implicit exchange steps):
\begin{prooftree}
\AxiomC{$a \arrow a$}
\LeftLabel{weakening}
\UnaryInfC{$a \arrow a, b$}
\AxiomC{$b \arrow b$}
\LeftLabel{weakening}
\UnaryInfC{$b \arrow a, b$}
\LeftLabel{$\vee$ left}
\BinaryInfC{$a \vee b \arrow a, b$}
\LeftLabel{weakening}
\UnaryInfC{$a \vee b, a \vee c \arrow a, b$}

\AxiomC{$a \arrow a$}
\RightLabel{weakening}
\UnaryInfC{$a \arrow a, c$}
\AxiomC{$c \arrow c$}
\RightLabel{weakening}
\UnaryInfC{$c \arrow a, c$}
\RightLabel{$\vee$ left}
\BinaryInfC{$a \vee c \arrow a, c$}
\RightLabel{weakening}
\UnaryInfC{$a \vee b, a \vee c \arrow a, c$}

\RightLabel{$\wedge$ right}
\BinaryInfC{$a \vee b, a \vee c \arrow a, b \wedge c$}
\RightLabel{$\vee$ right}
\UnaryInfC{$a \vee b, a \vee c \arrow a \vee (b \wedge c)$}
\LeftLabel{$\wedge$ left}
\UnaryInfC{$(a \vee b) \wedge (a \vee c) \arrow a \vee (b \wedge c)$}
\end{prooftree}


\paragraph{Example 2} Proving DeMorgan's Law:
$\lnot(\exists x)\lnot A(x) \vdash (\forall x)A(x)$.
The proof of this law in sequent calculus is as follows:
\begin{prooftree}
\AxiomC{$A(a) \arrow A(a)$}
\RightLabel{$\forall$ right}
\UnaryInfC{$A(a) \arrow (\forall x)A(x)$}
\RightLabel{$\lnot$ right}
\UnaryInfC{$\arrow \lnot A(a), (\forall x)A(x)$}
\RightLabel{$\exists$ right}
\UnaryInfC{$\arrow (\exists x)\lnot A(x), (\forall x)A(x)$}
\LeftLabel{$\lnot$ left}
\UnaryInfC{$\lnot(\exists x)\lnot A(x) \arrow (\forall x)A(x)$}
\end{prooftree}

\paragraph{Example 3} Proving the sequent
$(\forall x)A(x) \vee (\forall x)B(x) \vdash (\forall x)(A(x) \vee B(x))$.
\begin{prooftree}
\AxiomC{$A(a) \arrow A(a)$}
\LeftLabel{weakening}
\UnaryInfC{$A(a) \arrow A(a),B(a)$}
\LeftLabel{$\vee$ right}
\UnaryInfC{$A(a) \arrow A(a) \vee B(a)$}
\LeftLabel{$\forall$ left}
\UnaryInfC{$(\forall x)A(x) \arrow A(a) \vee B(a)$}

\AxiomC{$B(a) \arrow B(a)$}
\RightLabel{weakening}
\UnaryInfC{$B(a) \arrow A(a),B(a)$}
\RightLabel{$\vee$ right}
\UnaryInfC{$B(a) \arrow A(a) \vee B(a)$}
\RightLabel{$\forall$ left}
\UnaryInfC{$(\forall x)B(x) \arrow A(a) \vee B(a)$}

\LeftLabel{$\vee$ left}
\BinaryInfC{$(\forall x)A(x) \vee (\forall x)B(x) \arrow A(a) \vee B(a)$}
\RightLabel{$\forall$ right}
\UnaryInfC{$(\forall x)A(x) \vee (\forall x)B(x) \arrow (\forall x)(A(x) \vee B(x))$}

\end{prooftree}

\begin{thebibliography}{99}

\bibitem{buss98}
Samuel R. Buss, 
``Introduction to Proof Theory,'' in {\em Handbook of Proof Theory}, S. Buss (editor),
{\em Elsevier}, 1998, pages 1-78.

\end{thebibliography}

\end{document}



