\documentstyle[fullpage,11pt]{article}

\input{macros}
\newcommand{\defeq}{\buildrel \mbox{\small def} \over =}

 % zero-width inference rule markers
 % (if they have width, they throw off centering)
\newcommand{\zwb}[1]{\makebox[0cm][l]{{\scriptsize $#1$}}}

\newcommand{\mall}{\mbox{{\sc mall}}}
\newcommand{\imall}{\mbox{{\sc imall}}}
\newcommand{\mll}{\mbox{{\sc mll}}}
\newcommand{\cll}{\mbox{{\sc cll}}}
\newcommand{\imll}{\mbox{{\sc imll}}}
\newcommand{\ill}{\mbox{{\sc ill}}}
\newcommand{\cmll}{\mbox{{\sc cmll}}}

\newcommand{\la}{\mbox{$-\!\circ$}}     % Linear Arrow
\newcommand{\bla}{\mbox{$\circ\!-$}}    % Backwards Linear Arrow
%\newcommand{\Par}{\,{\parfont P}\,}    % Par (font)
\newcommand{\Par}{{\mbox{\raisebox{.4ex}{$\wp$}}}} % Par (gross)
\newcommand{\with}{\mbox{\,{\&}\,}}     % With (Additive And) (&)
\newcommand{\lplus}{\mbox{$\oplus$}}    % oplus
\newcommand{\tensor}{\mbox{$\otimes$}}  % Tensor (Multiplicative And) o*
\newcommand{\one}{\mbox{$1$}}           % 1
\newcommand{\zero}{\mbox{$0$}}          % 0
\renewcommand{\bottom}{\mbox{$\bot$}}     % bottom
\newcommand{\ltop}{\mbox{$\top$}}       % top

\newcommand{\as}{{\sc seq{}}{}} %%% Abramsky's System
\newcommand{\lm}{{\sc nat}}     %%% Our System

 % Definition
\newcommand{\define}{\mbox{${\stackrel{\Delta}{=}}$}}

\newcommand{\additives}[1]{#1}  % show additives
\newcommand{\emptyrhs}[1]{} % get rid of emptyrhs rules in int logic

\begin{document}

\title{\bf Natural Deduction and Sequent Calculus}
\author{Notes for CS 358, Spring 1995}
\date{April 10--12 Lectures}
\maketitle

\section{Natural Deduction Rules}

In natural deduction, a proof is a finite tree, with 
leaves labeled by logic formulas and internal nodes
labeled by instances of proof rules (including the
antecedent and consequent formulas).
In writing the rules, we use the notation 
\[
\begin{array}{c}
{}\\
\vdots\\
A
\end{array}
\]
to indicate a deduction of formula $A$,
i.e., a proof tree with $A$ at the root.

A leaf of a proof tree may be an \i{active} or \i{discharged}
assumption. The word \i{hypothesis} is sometimes
used for \q{active assumption.}
We have fully proved a formula $A$ only when we have constructed
a proof tree with $A$ at the root and all assumptions
discharged.

The $(\rightarrow\ \mbox{Intro})$ rule is written
\infrule{\begin{array}{c}
[A]\\
\vdots\\
B\\
\end{array}
}{A \rightarrow B}{}{(\rightarrow\ \mbox{Intro})}
where the square brackets $[\ ]$ around the hypothesis
mean that one effect of the rule is to change $A$ from an
active to discharged assumption.
In other words, while the proof 
\[
\begin{array}{c}
[A]\\
\vdots\\
B\\
\end{array}
\]
depends on active assumption $A$, the 
proof of $A \rightarrow B$ using $(\rightarrow\ \mbox{Intro})$
does not rely on the assumption of $A$.
For example, here is a complete proof of the formula
$A \rightarrow A$:
\[
\begin{array}{c}
[A]\\
\hline
A \rightarrow A
\end{array}
\]
This proof is constructed by assuming $A$. Then we discharge
the assumption to get a proof of $A \rightarrow A$.

There are various conventions that we might adopt regarding
hypotheses that do are not used in the proof (and therefore
wouldn't appear as part of a connected tree-shaped graph)
and multiple occurrences of the same formula as hypotheses.
For concreteness, let us agree that any formula could be considered
as vacuously appearing in any proof,
and that discharging an assumption $A$ means that
we may simultaneously discharge as many assumptions of $A$
as desired.
For example, we can discharge the \q{non-occurring} assumption
of $B$ as follows to get a proof of $B \rightarrow A$ depending
on the hypothesis $A$.
\[
\begin{array}{c}
A\\
\hline
B \rightarrow A
\end{array}
\]
If we then discharge the assumption $A$, we have a proof of
$A \rightarrow B \rightarrow A$.

\subsection*{Natural deduction rules for $\rightarrow, \land,\fa$}


\noindent
\begin{tabular}{rccc}
{\bf Hypothesis} &   $A $ \\[.5cm]
{\bf Introduction} &  $\begin{array}{c}
       \begin{array}{c}\vdots\\A\end{array}\quad
       \begin{array}{c}\vdots\\B\end{array}\\
            \hline
            A \land B
            \end{array}$ 
         &  $\begin{array}{c}
       \begin{array}{c}[A]\\ \vdots\\B\end{array} \\
                  \hline 
            A \rightarrow B \\
            {}
            \end{array}$ 
         &  $\begin{array}{c}
       \begin{array}{c}\vdots\\A\end{array} \\
                  \hline 
            \fa x.\, A
            \end{array}$  
\\
{\bf Elimination} &  $\begin{array}{c}
       \begin{array}{c}\vdots\\A\land B\end{array}\\
            \hline
            A 
            \end{array}$ 
      \quad  $\begin{array}{c}
       \begin{array}{c}\vdots\\A\land B\end{array}\\
            \hline
            B
            \end{array}$
       &  $\begin{array}{c}
       \begin{array}{c}\vdots\\A \rightarrow B\end{array} 
       \begin{array}{c}\vdots\\A  \end{array} \\
                  \hline 
            B 
            {}
            \end{array}$ 
         &  $\begin{array}{c}
       \begin{array}{c}\vdots\\\fa x.\, A\end{array} \\
                  \hline 
            [t/x]A
            \end{array}$  
\end{tabular}\\

\vskip 1ex
\noindent
\b{Exercise:}
Write a proof of 
$(A \rightarrow B) \rightarrow A \rightarrow A \rightarrow B$.

\newpage
\section{Sequent Calculus}

A \i{sequent} is an expression $\Gamma \ts \Sigma$, where
$\Gamma$ and $\Sigma$ are finite lists of formulas,
$\Gamma = A_1, \ldots, A_k$, $\Sigma = B_1, \ldots, B_\ell$.
Intuitively, $A_1, \ldots, A_k \ts B_1, \ldots, B_\ell$
means that the conjunction $A_1 \land \ldots \land A_k$ 
implies the disjunction $B_1 \lor \ldots \lor B_\ell$.
However, the exact form of conjunction, disjunction and
implication involved will depend on the kind of logic
we are defining. In a sequent calculus presentation of
classical logic, $\Gamma \ts \Sigma$ may be understood
using classical conjunction, disjunction and
implication, while in linear logic, we must use
\q{linear} forms of conjunction, disjunction and implication.

\subsection*{Structural and identity rules}

\begin{tabular}{rccl}
{\bf Exch. Left} &  $\begin{array}{c}
	    \Gamma_1, A, B, \Gamma_2 \vdash \Sigma \\
            \hline
            \Gamma_1, B, A, \Gamma_2 \vdash \Sigma
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma \vdash \Sigma_1, A, B, \Sigma_2 \\
            \hline
            \Gamma \vdash \Sigma_1, B, A, \Sigma_2
            \end{array}$ & {\bf Exch. Right} \\[.5cm]
{\bf Weak. Left} &  $\begin{array}{c}
	    \Gamma \vdash \Sigma \\
            \hline
            \Gamma, A \vdash \Sigma
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma \vdash \Sigma \\
            \hline
            \Gamma \vdash \Sigma, B
            \end{array}$ & {\bf Weak. Right} \\[.5cm]
{\bf Contr. Left} &  $\begin{array}{c}
	    \Gamma, A, A \vdash \Sigma \\
            \hline
            \Gamma, A \vdash \Sigma
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma \vdash \Sigma, B, B \\
            \hline
            \Gamma \vdash \Sigma, B
            \end{array}$ & {\bf Contr. Right}  \\[.5cm]
{\bf Identity} &   $\begin{array}{c}
	            \hline
		    A \vdash A
		    \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma_1 \vdash A,\Sigma_1 \hspace{1cm}
            \Gamma_2, A \vdash \Sigma_2\\
            \hline
            \Gamma_1, \Gamma_2 \vdash \Sigma_1, \Sigma_2
            \end{array}$ & {\bf Cut}
\end{tabular}

\subsection*{Intuitionistic case}

The sequent rules for intuitionistic logic are obtained from
the classical ones by restricting the list of formulas
on the right to a single formula.
This makes it impossible to apply structural rules
on the right. 

\subsection*{Logical rules for negation, conjunction and disjunction}

\noindent
\begin{tabular}{rccl}
{\bf $\lnot$ Left} &  $\begin{array}{c}
	    \Gamma \vdash \Sigma, B \\
            \hline
            \Gamma, \lnot B \vdash \Sigma
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma, A \vdash \Sigma\hspace{1cm}
            \Gamma\vdash \lnot A \Sigma_2\\
            \hline
            \Gamma_1, \Gamma_2 \vdash (A \otimes B), \Sigma_1, \Sigma_2
            \end{array}$ & {\bf $\lnot$ Right} \\[.5cm]
{\bf $\land$ Left} &  $\begin{array}{c}
	    \Gamma, A \vdash \Sigma \\
            \hline
            \Gamma, A \land B \vdash \Sigma
            \end{array}$ 
            $\begin{array}{c}
	    \Gamma, B \vdash \Sigma \\
            \hline
            \Gamma, A \land B \vdash \Sigma
            \end{array}$
         &  $\begin{array}{c}
	    \Gamma_1 \vdash A,\Sigma_1 \hspace{1cm}
            \Gamma_2 \vdash B, \Sigma_2\\
            \hline
            \Gamma_1, \Gamma_2 \vdash (A \land B), \Sigma_1, \Sigma_2
            \end{array}$ & {\bf $\land$ Right} \\[.5cm]
{\bf $\lor$ Left} &  $\begin{array}{c}
	    \Gamma_1, A \vdash \Sigma_1 \hspace{1cm}
            \Gamma_2, B \vdash \Sigma_2\\
            \hline
            \Gamma_1, \Gamma_2, (A \lor B) \vdash \Sigma_1, \Sigma_2
            \end{array}$ 
         &  $\begin{array}{c}
	    \Gamma \vdash A, \Sigma \\
            \hline
            \Gamma \vdash (A \lor B), \Sigma
            \end{array}$ \quad
           $\begin{array}{c}
	    \Gamma \vdash B, \Sigma \\
            \hline
            \Gamma \vdash (A \lor B), \Sigma
            \end{array}$  & {\bf $\lor$ Right} 
\end{tabular}\\

\noindent
In the intuitionistic case, we need to reformulate
$\lor$ Left so the rule does not produce a sequent with
more than one formula on the right.

\begin{center}
\begin{tabular}{rc}
{\bf $\lor$ Left} &  $\begin{array}{c}
	    \Gamma_1, A \vdash C \hspace{1cm}
            \Gamma_2, B \vdash C\\
            \hline
            \Gamma_1, \Gamma_2, (A \lor B) \vdash C
            \end{array}$ 
\end{tabular}
\end{center}


\subsection*{Implication}

\noindent
\begin{tabular}{rccl}
	{\bf $\rightarrow$ Left} &  $\begin{array}{c}
		    \Gamma_1 \vdash A,\Sigma_1 \hspace{1cm}
	            \Gamma_2, B \vdash \Sigma_2\\
        	    \hline
	            \Gamma_1, \Gamma_2, (A \rightarrow B) \vdash \Sigma_1,
\Sigma_2
        	    \end{array}$ 
	         &  $\begin{array}{c}
		    \Gamma, A \vdash B, \Sigma \\
	            \hline
	            \Gamma \vdash (A \rightarrow B), \Sigma
        	    \end{array}$ & {\bf $\rightarrow$ Right} 
\end{tabular}

\subsection*{Quantification}

\noindent
\begin{tabular}{rccl}
{\bf $\forall$ Left} & $\begin{array}{c}
	     \Gamma,[t/x]A \vdash \Sigma \\
             \hline
	     \Gamma,\forall x .\, A \vdash \Sigma \\
             \end{array}$
           & $\begin{array}{c}
	     \Gamma  \vdash A, \Sigma \\
             \hline
	     \Gamma  \vdash \forall x.\, A, \Sigma \\
             \end{array}$ & {\bf $\forall$ Right} \\[.5cm]
{\bf $\exists$ Left} & $\begin{array}{c}
	     \Gamma,A \vdash \Sigma \\
             \hline
	     \Gamma,\exists x.\, A \vdash \Sigma \\
             \end{array}$
           & $\begin{array}{c}
	     \Gamma \vdash [t/x]A, \Sigma \\
             \hline
	     \Gamma \vdash \exists x.\, A, \Sigma \\
             \end{array}$ & {\bf $\exists$ Right} \\[.5cm]
\end{tabular}\\
In {\bf $\forall$ Right} and {\bf $\exists$ Left},
the variable $x$ must not be free in $\Gamma$ of $\Sigma$.

\subsection*{Proof strategy}

Sequent calculus lends itself to both \q{forward-directed}
proofs, starting from axioms and deriving consequences,
and  \q{backward-directed} proof search. 
The places where \q{guessing} is involved in proof search
are (i) guessing which formula in a sequent
is to be manipulated (\i{analyzed}), (ii) guessing whether {\bf Cut}
is to be used, since this is independent of the form
of any formulas in the sequent,
(iii) guessing the cut-formula, if {\bf Cut} is assumed to
be the last rule in the proof,
(iv) guessing terms to substitute for quantified
variable in rules 
{\bf $\forall$ Left} and {\bf $\exists$ Right}.

\subsection*{Cut elimination}

There is a proof-transformation procedure
that takes any proof and successively re-orders rules so that
all occurrences of cut are eventually removed. 
This procedure may increase the size of the proof 
very exponentially. However, the increase in proof size
may be traced to the use of contraction. 



For every rule except {\bf Cut}, the formulas in the
premise are subformulas of the formulas in the conclusion
(assuming we regard $[t/x]A$ as a subformula of
$\exists x.\, A$ and $\forall x.\, A$).
Since every provable formula has a {\bf Cut}-free proof,
this \i{subformula property} gives us a way of analyzing
the set of provable formulas.
This idea was used by Gentzen in the 1930's to prove the
consistency of Peano arithmetic and other systems.

\paragraph{Example} 

Here is part of a proof of Pearce's Law,
$((A \aro B) \aro A) \aro A$,
in classical sequent calculus.


\newcommand{\pfl}[1]
{\raisebox{1ex}{\underline{$ #1 $}}}

\[
\begin{array}{cl}
\pfl{\ts A \aro B, A \quad \quad A\ts A}&(\aro\ \mbox{Left})\\
\pfl{(A \aro B) \aro A \ts A,A }&(\mbox{Contr. Right})\\
\pfl{(A \aro B) \aro A \ts A} & (\aro\ \mbox{Right})\\
 ((A \aro B) \aro A) \aro A
\end{array}
\]

\paragraph{Exercises}\hfil \\
1. Complete the proof above by proving $\ts A \aro B, A$.\hfil \\
2. Use the fact that every provable formula has a
cut-free proof to show that Pearce's Law
is not provable in the intuitionistic sequent calculus.


\end{document}
