\section{Isabelle Proof of the Cut-Elimination Theorem}

In this section we describe functions for reasoning about derivations
which end with a cut. The types for these functions are shown in
Figure~\ref{fig:functions-reasoning-about-cuts}.

\begin{figure}[t]
  \centering
\begin{verbatim}
  cutOnFmls     :: "formula set => pftree => bool"
  cutIsLP       :: "formula => pftree => bool"
  cutIsLRP      :: "formula => pftree => bool"
\end{verbatim}
  \caption{Functions for reasoning about cuts}
  \label{fig:functions-reasoning-about-cuts}
\end{figure}

\subsection{Transforming a derivation tree to make a cut principal}
\cc{start of meth.tex} \cc{s-mcp} \label{s-mcp}

The method for cut-elimination depends on cuts being made \emph{principal},
that is, so that the cut-formula is introduced immediately above the cut,
on both sides.
We define a cut to be \emph{left-principal} [\emph{right-principal}]
if the cut-formula is 
introduced immediately above the cut on the left [right] side.
A principal cut on $A \lor B$ is shown in Fig.~\ref{fig-orcut}:

\begin{figure}
\vpf
\begin{center}
\bpf
\A "$\Pi_{ZAB}$"
\U "$Z \vdash A, B$"
\U "$Z \vdash A \lor B$" "($\vdash \lor $)"
\A "$\Pi_{AX}$"
\U "$A \vdash X$"
\A "$\Pi_{BY}$"
\U "$B \vdash Y$"
\B [1em] "$A \lor B \vdash X, Y$" "($\lor \vdash $)"
\B [2em] "$Z \vdash X, Y$" "($cut$)"
\epf
\end{center}
\caption{Principal cut on formula $A \lor B$}
\cc{fig-orcut}
\label{fig-orcut}
\end{figure}

With an arbitrary rule in place
of ($\lor \vdash $) [($\vdash \lor $)] it would be left- [right-] principal.

The predicates \texttt{cutOnFmls}, \texttt{cutIsLP} and \texttt{cutIsLRP}
require the bottom node of the
derivation tree to be of the form \texttt{Pr seq rule pts},
and that if \texttt{rule} is \texttt{cut}, then for:

\begin{description}
\item[\texttt{cutOnFmls s} :] the cut is on a formula in the set \texttt{s}
\item[\texttt{cutIsLP A} :]
  the cut is on formula \texttt{A} and is left-principal 
  (see \S\ref{s-mcp} and Fig.\ref{fig-orcut})
\item[\texttt{cutIsLRP A} :]
  the cut is on formula \texttt{A} and is (left- and right-)principal 
\end{description}

Note that it follows from the definitions that a derivation tree
satisfying any of 
the predicates \texttt{allPT (cutOnFmls ?s)}, \texttt{allPT (cutIsLP ?A)} and 
\texttt{allPT (cutIsLRP ?A)}
has no premises.

In the case of a cut that is not left-principal, say we have a tree
like the one on the left in Fig.~\ref{fig-cut-p}.  Then we transform
the subtree rooted at $X \vdash A$ by simply changing its root sequent
to $X \vdash Y$, and, proceeding upwards, changing all ancestor
occurrences of $A$ to $Y$.  In doing this we run into difficulty at
each point where $A$ is introduced: at such points we insert an
instance of the cut rule.  The diagram on the right hand side of
Fig.~\ref{fig-cut-p} shows this in the case where $A$ is introduced at
just one point.  The notation $\Pi_L[A \,?\!= Y]$ means that all
``appropriate'' instances of $A$ are changed to $Y$, that is,
instances of $A$ which can be traced to the instance displayed on the
right in $X \vdash A$.  The rules contained in $\Pi_L[A \,?\!= Y]$ are
the same as the rules used in $\Pi_L$; thus it remains to be proved
that $\Pi_L[A \,?\!= Y]$ is well-formed.  The resulting 
%It can be seen that the 
cut in the diagram on the right of Fig.~\ref{fig-cut-p} is left-principal.

\begin{figure}
\hfill 
\bpf
\A "$\Pi'$"
\U "$X' \vdash A $" "(intro-$A$)"
\U "$\Pi_L$" "($\pi$)"
\U "$X \vdash A $" "($\rho$)"
\A "$\Pi_R$"
\U "$A \vdash Y$" 
\B [2em] "$X \vdash Y$" "($cut$)"
\epf
\qquad \qquad
\bpf
\A "$\Pi'$"
\U "$X' \vdash A $" "(intro-$A$)"
\A "$\Pi_R$"
\U "$A \vdash Y$" 
\B [2em] "$X' \vdash Y$" "($cut$)"
\U "$\Pi_L[A \,?\!= Y]$" "($\pi$)"
\U "$X \vdash Y $" "($\rho$)"
\epf
\hfill \mbox{}
\caption{Making a cut left-principal}
\cc{fig-cut-p}
\label{fig-cut-p}
\end{figure}

It follows from Belnap's conditions that where $A$ is introduced by an
introduction rule, it is necessarily displayed in the succedent
position, as above the top of $\Pi_L$ in the left branch of the left
hand derivation in Fig.~\ref{fig-cut-p}.  Other conditions of Belnap
(eg, a formula is displayed where it is introduced, and each structure
variable appears only once in the conclusion of a rule) ensure that
a procedure can be formally defined to accord with the informal description
above; the procedure removes a cut on $A$ which is not left-principal and
creates (none, one or more) cut(s) on $A$ which are left-principal.
\footnote{was: this procedure is well-defined and works.}

Rather more trivial is where the occurrence of $A$ which we want to change to
$Y$ is introduced by the identity rule $A \vdash A$.
Then the derivation tree is transformed as shown in Fig.\ref{fig-cut-id}.
Again, the diagram is specific to the case where $A$ is introduced at just one
point.

This construction generalizes easily to the case
where $A$ is introduced (in one of the above ways)
at more than one point (eg, arising from use of
one of the rules where a structure variable appears twice in the premises),
or where $A$ is ``introduced'' by use
of the weakening rule. 
This description of the procedure is very loose and informal -- the formality
and completeness of detail is reserved for the machine proof!

\begin{figure}
\hfill
\bpf
\A "$A \vdash A $" 
\U "$\Pi_L$" "($\pi$)"
\U "$X \vdash A $" "($\rho$)"
\A "$\Pi_R$"
\U "$A \vdash Y$" 
\B [2em] "$X \vdash Y$" "($cut$)"
\epf
\qquad \qquad
\bpf
\A "$\Pi_R$"
\U "$A \vdash Y$" 
\U "$\Pi_L[A \,?\!= Y]$" "($\pi$)"
\U "$X \vdash Y $" "($\rho$)"
\epf
\hfill \mbox{}
\caption{Making a cut left-principal -- $A$ introduced by identity axiom}
\cc{fig-cut-id}
\label{fig-cut-id}
\end{figure}

Subsequently,
the ``mirror-image'' procedure is followed, to convert a left-principal
cut into one or more (left- and right-)principal cuts.

\cc{end of meth.tex} 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "ce"
%%% End: