%%
%%
\documentclass{llncs}
%\documentclass[a4paper,11pt,twocolumn]{article}
%\documentclass[a4paper,11pt]{article}
%\usepackage{makeidx}
%\usepackage{acmnew-xref}
% \usepackage[scrtime]{prelim2e}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{exptrees}
\usepackage{url}
%\newcommand{\url}[1]{\texttt{#1}}
%\RequirePackage{mathptm}
%\RequirePackage{times}
%\RequirePackage{palatino}
\renewcommand{\today}{\number\day\
\ifcase\month\or
January\or February\or March\or April\or May\or June\or
July\or August\or September\or October\or November\or December\fi
\ \number\year}
%\setlength \parskip {1.0ex}
\setcounter{secnumdepth}2
\setcounter{tocdepth}2
%\newtheorem{theorem}{Theorem}[subsection]
% \newtheorem{theorem}{Theorem}[section]
%\newcounter{theorem}[section]
% \def\thedefinition{\thesection.\arabic{theorem}}
% \newenvironment{theorem}{
% \refstepcounter{theorem}
% \trivlist
% \item[\hskip\labelsep{\bf Theorem \thedefinition}.]}%
% {\samepage\hfill\mbox{\ $\nabla$}\endtrivlist\par}
% \newcommand{\qed}{}
% \newenvironment{proof}{
% \noindent{\bf Proof:}}{\mbox{\bf Q.E.D.}\vspace{1ex}}
% \newtheorem{definition}{Definition}[section]
% \newcounter{definition}[section]
% \def\thedefinition{\thesection.\arabic{definition}}
% \newenvironment{definition}{
% \refstepcounter{definition}
% \trivlist
% \item[\hskip\labelsep{\bf Definition \thedefinition}.]}%
% {\samepage\hfill\mbox{\ $\nabla$}\endtrivlist\par}
% \newtheorem{lemma}{Lemma}[section]
% \newcounter{lemma}[section]
% \def\thedefinition{\thesection.\arabic{lemma}}
% \newenvironment{lemma}{
% \refstepcounter{lemma}
% \trivlist
% \item[\hskip\labelsep{\bf Lemma \thedefinition}.]}%
% {\samepage\hfill\mbox{\ $\nabla$}\endtrivlist\par}
% \newtheorem{corollary}{Corollary}[section]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble
\newcommand{\mcyl}{\raisebox{0.2ex}{\bf c}}
\newcommand{\mor}{+}
\newcommand{\mand}{\circ}
\newcommand{\mnot}{\sim}
\newcommand{\mimp}{\rightarrow}
\newcommand{\mif}{\leftarrow}
\newcommand{\mtop}{\mbox{\bf 1}}
\newcommand{\mbot}{\mbox{\bf 0}}
%\newcommand{\myzero}{\mbox{\bf 0}}
\newcommand{\mstar}{\bigstar}
%\newcommand{\fiss}{+}
\newcommand{\mcal}[1]{\mbox{$\cal #1$}}
\newcommand{\btop}{\top}
\newcommand{\bbot}{\bot}
\newcommand{\bor}{\vee}
\newcommand{\band}{\wedge}
\newcommand{\bnot}{\neg}
\newcommand{\bimp}{\supset}
\newcommand{\conv}{\smallsmile}
\newcommand{\semic}{\mbox{ ; }}
\newcommand{\comma}{\raisebox{0.5ex}{ , }}
%\newcommand{\colon}{\mbox{ : }}
\newcommand{\myE}{ E }
\newcommand{\blob}{\bullet}
\newcommand\cfile{}
\newcommand\comment[1]{}
% \newcommand\cc[1]{} % for label names
\newcommand\cc[1]{#1} % for label names
% \renewcommand\footnote[1]{} % for footnotes
% \pagestyle{myheadings}
% \newcommand{\mystrut}[1]{
% \bpf \A ; "$\vphantom{X}$" \U ['] ; "$\vphantom{X}$" "#1" \epf \ %
% }
\newcommand{\idrule}[2]{
\mbox{#1 \ $\mbox{#2}$}}
\newcommand{\ds}{\displaystyle\strut}
\newcommand{\urule}[3]{
\mbox{#1 \ $\frac{\ds \mbox{#2}}{\ds \mbox{#3}}$}}
\newcommand{\brule}[4]{
\mbox{#1 \ $\frac{\ds \mbox{#2}\ \ \ \ \mbox{#3}}
{\ds \mbox{#4}}$}}
\newcommand\invrule[2]{
% for use in non-math mode, args interpreted in math mode
\begin{tabular}{@{}c@{}}
$ #1 $ \\ \hline \hline $ #2 $
\end{tabular}}
\newcommand\slrule[2]{ % similar to \frac, except
% for use in non-math mode, args interpreted in math mode
\begin{tabular}{@{}c@{}}
$ #1 $ \\ \hline $ #2 $
\end{tabular}}
\renewcommand\theenumi{(\alph{enumi})}
\renewcommand\labelenumi{\theenumi}
\renewcommand\theenumii{(\roman{enumii})}
\renewcommand\labelenumii{\theenumii}
%\newcommand\proof{\noindent\textbf{Proof.}}
\newcommand\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
%\newcommand\seesrc[1]{(see source file \texttt{#1}, \apsrc{#1})}
\newcommand\seesrc[1]{(see source file \texttt{#1})}
%\newcommand\insrc[1]{in source file \texttt{#1} (see \apsrc{#1})}
\newcommand\insrc[1]{in source file \texttt{#1}}
\newcommand\page[1]{page~\pageref{#1}}
\newcommand\fig[1]{Fig.~\ref{fig:#1}}
\newcommand\ch[1]{Chapter~\ref{ch:#1}}
\newcommand\tbl[1]{Table~\ref{tbl:#1}}
\newcommand\thrm[1]{Theorem~\ref{thrm:#1}}
\newcommand\lem[1]{Lemma~\ref{lem:#1}}
\newcommand\ttl[1]{\tti{#1}\label{#1}}
\newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}}
\newcommand\ttdef[1]{\texttt{#1}\tti{#1}}
\newcommand\tti[1]{\index{#1@\texttt{#1}}}
\newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}}
\newcommand\dRA{{\boldmath $\delta$}\textbf{RA}}
\newcommand\dKt{{\boldmath $\delta$}\textbf{Kt}}
\newcommand\NRA{\textbf{NRA}}
\newcommand\RA{\textbf{RA}}
%\newcommand\M{$\mathcal M$}
\newcommand\M{\ensuremath{\mathcal M}}
\newcommand\Mp{$\mathcal M'$}
\newcommand\up[1]{\vspace{-#1ex}}
\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree
\newcommand\1{\textbf 1}
\newcommand\0{\textbf 0}
\newcommand\cut{(\emph{cut})}
\newcommand\dt{\texttt{dt}}
\newcommand\dtn{\texttt{dtn}}
\newcommand{\pordered}[3]{#1 <_{\texttt{\scriptsize #2}} #3}
\newcommand{\Revpordered}[3]{#1 >_{\texttt{\scriptsize #2}} #3}
\newcommand{\LRPord}[2]{\pordered{#1}{LRP}{#2}}
\newcommand{\cutord}[2]{\pordered{#1}{cut}{#2}}
\newcommand{\snoneord}[2]{\pordered{#1}{sn1}{#2}}
\newcommand{\dtord}[2]{\pordered{#1}{dt}{#2}}
\newcommand{\Revdtord}[2]{\Revpordered{#1}{dt}{#2}}
% automatically defined in LLNCS style
%\newtheorem{thm}{Theorem}%[chapter]
%\newtheorem{lemma}[thm]{Lemma}
%\newtheorem{defn}[thm]{Definition}
%\newtheorem{cor}{Corollary}[thm]
%\renewcommand\thecor{\thethm(\arabic{cor})}
\pagestyle{plain}
\begin{document}
\title{Formalised Cut Admissibility for Display Logic}
\author{
Jeremy E.\ Dawson\thanks{Supported by an Australian Research
Council Large Grant}
\ \ and \ \
Rajeev Gor\'e\thanks{Supported by an Australian Research Council QEII Fellowship}
}
\institute{
Department of Computer Science and
Automated Reasoning Group
\\ Australian National University,
Canberra, ACT 0200, Australia
\\ \texttt{jeremy@discus.anu.edu.au} \ \ \texttt{rpg@discus.anu.edu.au}
}
\date{\today}
%% Title
\maketitle
\begin{abstract}
We use a deep embedding of the display calculus for relation
algebras \dRA\ in the logical framework Isabelle/HOL to formalise a
machine-checked proof of cut-admissibility for \dRA. Unlike other
``implementations'', we explicitly formalise the structural
induction in Isabelle/HOL and believe this to be the first full
formalisation of cut-admissibility in the presence of explicit
structural rules.
\end{abstract}
% \newpage
% \tableofcontents
% \newpage
\sloppy
%% Here begins the main text
\section{Introduction}
Display Logic \cite{belnap-display} is a generalised sequent framework
for non-classical logics.
%, based on Gentzen's sequent calculus \cite{szabo-gentzen}.
Since it is not really a logic, we prefer the
term display calculi and use it from now on. Display calculi extend
Gentzen's language of sequents with extra, complex, $n$-ary structural
connectives, in addition to Gentzen's sole structural connective, the
``comma''. Whereas Gentzen's comma is usually assumed to be
associative, commutative and inherently poly-valent, no such implicit
assumptions are made about the $n$-ary structural connectives in
display calculi. Properties such as associativity are explicitly
stated as structural rules.
Such explicit structural rules make display calculi as modular as
Hilbert-style calculi: the logical rules remain constant and different
logics are obtained by the addition or deletion of structural rules
only. Display calculi therefore provide an extremely elegant sequent
framework for ``logic engineering'', applicable to many (classical and
non-classical) logics in a uniform way
\cite{wansing-displaying-modal-logic,gore-sld-igpl}. The display
calculus \dRA\ \cite{gore-relalg}, for example, captures the logic for
relation algebras. The most remarkable property of display calculi is
a generic cut-elimination theorem, which applies whenever the rules
for the display calculus satisfy certain, easily checked, conditions.
Belnap \cite{belnap-display} proves that the cut rule is
\textit{admissible} in \textbf{all} such display calculi: he
transforms a derivation whose only instance of cut is at the bottom,
into a cut-free derivation of the same end-sequent. His proof does not
use the standard double induction over the cut rank and degree a
l\`{a} Gentzen.
%\cite{szabo-gentzen}.
In \cite{dawson-gore-embedding-comparing} we implemented a ``shallow''
embedding of \dRA\ which enabled us to mimic derivations in \dRA\
using Isabelle/Pure. But it was impossible to reason \textit{about}
derivations since they existed only as the trace of the particular
Isabelle session. In \cite{pfenning-structural-lics94}, Pfenning has
given a formalisation of cut-admissibility for traditional sequent
calculi for various nonclassical logics using the logical framework
Elf, which is based upon dependent type theory. Although dependent
types allow derivations to be captured as terms, they do not enable us to
formalise all aspects of a meta-theoretic proof. As Pfenning admits,
the Elf formalisation cannot be used for checking the correct use of
the induction principles used in the cut-admissibility proof, since
this requires a ``deep'' embedding \cite{pfenning-structural-lics94}.
% \begin{quote}\it
% Once the structural proof of admissibility has been found and
% implemented, it is natural to ask if it can also be encoded in
% stronger frameworks such as Coq [DFH+93] so that structural
% inductions are made explicit and the proof is fully formally
% verified.
% \end{quote}
The use of such ``deep'' embeddings to formalise meta-logical results
is rare
\cite{mikhajlova-vonwright-isomorphism,matthews-implementing-isabelle}.
To our knowledge, the only full formalisation of a proof of
cut-admissibility is that of Sch{\"u}rmann \cite{schuermann-phd}, but
the calculi used by both Pfenning and Sch{\"u}rmann contain no
explicit structural rules, and structural rules like contraction are
usually the bane of cut-elimination. Here, we use a deep embedding of
the display calculus \dRA\ into Isabelle/HOL to fully formalise the
admissibility of the cut rule in the presence of explicit (and
arbitrary) structural rules.
The paper is set out as follows. In
Section~\ref{sec:display-calculus-dra} we briefly describe the display
calculus \dRA\ for the logic of relation algebras. In
Section~\ref{sec:deep-embedding-dra} we describe an encoding of \dRA\
logical constants, logical connectives, formulae, structures,
sequents, rules, derivations and derived rules into Isabelle/HOL. In
Section~\ref{sec:an-operational-view} we describe the two main
transformations required to eliminate cut. In
Section~\ref{subsec:funct-reas-about} we describe how we mechanised
these to prove the cut-elimination theorem in Isabelle/HOL. In
Section~\ref{sec:concl-furth-work} we present conclusions and discuss
further work.
\comment{
\paragraph{Note to the reviewers:}
This paper necessarily contains a lot of background material on
display calculi, cut-elimination, the syntax of \dRA, and various
details of our deep embedding of it into Isabelle/HOL. Similar details
were necessary in a companion paper which has been submitted to
LICS-02 \cite{dawson-gore-machine-checked-strong-normalisation-lics}.
The current paper and the LICS paper therefore have much in common.
But the core of the LICS paper describes a new proof of
strong-normalisation for display calculi, which arose because we found
a bug in the published proof by Wansing. The core of the current paper
describes cut-admissibility a l\`a Belnap. Whether the contents are
different enough to warrant two papers is up to you. If both papers
are accepted we shall partition the common material to reduce the
duplicated material.
Although Belnap uses a double
induction, he does not set out the proof in the traditional way
involving a cut rank and cut degree a l\`{a} Gentzen.
%\cite{szabo-gentzen}.
For this reason, Belnap's proof has been criticised verbally by well-known
proof theorists as lacking rigour, although never in writing to our
knowledge.
To settle the question, Heinrich Wansing gave a proof of
strong-normalisation for the cut-elimination procedure for a
particular display calculus in \cite{wansing-strong}. As is
traditional in proofs of strong normalisation, Wansing first defines
certain transformations on derivations, and then shows that a
sufficiently long sequence of such transformations, beginning with
some given derivation, will terminate with a cut-free derivation of
the same end-sequent. The original derivation may contain multiple
instances of cut, but only certain instances of cut are amenable to the
transformations. The highest cuts, with no cuts above them, are always
amenable to these transformations, so strong normalisation implies the
admissibility of cut.
We found it difficult to understand Wansing's proof in its entirety so
we decided to formalise it for the display calculus \dRA\ for relation
algebras from \cite{gore-relalg}, and check it using a logical
framework. The choice of the display calculus is not important, we
just happen to be very familiar with it. In
\cite{dawson-gore-embedding-comparing} we outlined our initial
attempts and described why we finally settled on the logical framework
Isabelle/HOL. But in formalising Wansing's proof of strong
normalisation, we found a slight anomaly: at a certain point in the
proof, Wansing states that ``This construction generalises easily to
the case where $A$ is introduced \ldots at more than one point
\ldots''. We were unable to see how the generalisation would proceed.
We therefore developed our own proof of strong normalisation for the
display calculus \dRA. The work required approximately 9 man-months,
required approximately 1600 lines of Isabelle/HOL theory files and
8500 lines of ML proof files, and takes approximately 35 minutes to
fully type-check on a ZZZ machine. Here, we describe how we proved
%both the admissibility of cut and
the strong normalisation result for \dRA. As
far as we are aware, this is the first full formalisation of a strong
normalisation result using a logical framework.
}
\section{The Display Calculus \dRA}
\label{sec:display-calculus-dra}
%We assume the reader is familiar with relation algebras
% \cite{maddux-introductory}
\comment{
are extensions of Boolean algebras;
whereas Boolean algebras model subsets of a given set,
relation algebras model binary relations on a given set.
Relation algebras have operations such as
relational composition and relational converse,
and Boolean operations such as intersection
(conjunction) and complement (negation).
A display calculus for relation algebras called \dRA\ can be found in
\cite{gore-relalg}.
}
% Relation algebras form the basis of relational databases
% \cite{elmasri-navathe-database}
% and of the specification and proof of correctness of programs,
% particularly in the style of Mili \cite{mili-relational}.
The following grammar defines the syntax of relation algebras:
\begin{eqnarray*}
A & ::= &
p_i
\mid \btop
\mid \bbot
\mid \bnot A
\mid A \band A
\mid A \bor A
\mid \mtop
\mid \mbot
\mid \mnot A
\mid \conv A
\mid A \mand A
\mid A \mor A
\end{eqnarray*}
A display calculus for relation algebras called \dRA\ can be found in
\cite{gore-relalg}. Sequents of \dRA\ are expressions of the form $X
\vdash Y$ where $X$ and $Y$ are built from the nullary structural
constants $E$ and $I$ and formulae, using a binary comma, a binary
semicolon, a unary $\ast$ or a unary $\bullet$ as structural
connectives, according to the grammar below:
\[
X ::= A \mid I \mid E \mid \ast X \mid \blob X \mid X \semic X
\mid X \comma X
\]
Thus, whereas Gentzen's sequents $\Gamma \vdash \Delta$ assume that
$\Gamma$ and $\Delta$ are comma-separated lists of formulae,
\dRA-sequents $X \vdash Y$ assume that $X$ and $Y$ are complex
tree-like structures built from formulae and the constants $I$ and $E$
using comma, semicolon, $\ast$ and $\blob$.
The defining feature of display calculi is that in all logical
rules, the principal formula is always ``displayed'' as the whole of the
right-hand or left-hand side.
For example, the rule $(\mbox{\textbf{LK}-}\vdash \lor )$ below
is typical of Gentzen's sequent calculi like \textbf{LK}, while the rule
$(\mbox{\dRA-}\vdash \lor )$ below is typical of display calculi:
$$\frac {\Gamma \vdash \Delta, P \comma Q}
{\Gamma \vdash \Delta, P \lor Q}(\mbox{\textbf{LK}-}\vdash \lor )
\qquad \qquad
\frac {X \vdash P \comma Q}
{ X \vdash P \lor Q}(\mbox{\dRA-}\vdash \lor )
$$
\comment{
To use this display calculus rule downwards on a sequent $X' \vdash
Y'$ containing an occurrence of the structure $(P \comma Q)$,
everything other than $(P,Q)$ must be moved to the left of $\vdash$
creating the complex structure $X$, thereby displaying the structure
$(P \comma Q)$ as the whole of the right-hand side. There are rules
which enable any given structure to be displayed. After the rule
application we can ``undisplay'' the moved material back to its
original position (reversing the display steps used), so that the sole
purpose of this rule is to ``rewrite'' some occurrence of $(P \comma
Q)$ in $X'$ or $Y'$ to $P \lor Q$. Note that the occurrence of $(P
\comma Q)$ could come from $X'$ or from $Y'$: see \cite{gore-relalg}
for a full account.
\subsection{Isabelle and its HOL theory}
Isabelle is an automated proof assistant \cite{isabelle-ref}.
Its meta-logic is an intuitionistic typed higher-order logic,
% and typed $\lambda$-calculus,
sufficient to support the built-in inference steps of
higher-order unification and term rewriting.
Isabelle accepts inference rules of the form
``from $\alpha_1, \alpha_2, \ldots, \alpha_n, \mbox{ infer } \beta$''
where the $\alpha_i$ and $\beta$
are expressions of the Isabelle meta-logic,
or are expressions using a new syntax, defined by the user, for some
``object logic''. % $\mathcal F$.
An Isabelle user can encode a particular calculus
$\mathcal C _L$ for some logic $L$ as an ``object logic'' by using
these rule templates to encode the set of inference rules of
$\mathcal C _L$.
%This is supplemented with the user's choice of
%object logic in which to perform proofs.
For example, if $\mathcal C _L$ is a natural deduction calculus, then
the $\alpha_i$ and $\beta$ will be formulae of $L$, whereas if
$\mathcal C _L$ is a sequent calculus, then the $\alpha_i$ and $\beta$
will be sequents of $\mathcal C _L$. Such an encoding is called an
``object logic'', even though it is a (typically natural deduction or
sequent) \emph{calculus} for some particular logic $L$. In practice
most users would build on one of the comprehensive ``object logics''
already supplied \cite{isabelle-object}, such as Isabelle/HOL.
Isabelle/HOL is an Isabelle theory based on the higher-order logic of
Church \cite{church-types} and the HOL system of Gordon
\cite{HOL-introduction}. Thus it includes quantification and
abstraction over higher-order functions and predicates. The HOL
theory uses Isabelle's own type system and function application and
abstraction: that is, object-level types and functions are identified
with meta-level types and functions. Isabelle/HOL contains constructs
found in functional programming languages, such as \texttt{datatype}
and \texttt{let}, which greatly facilitates re-implementing a program
in Isabelle/HOL, and then reasoning about it. However limitations
(not found in, say, Standard ML itself) prevent defining types which
are empty or which are not sets, or functions which may not terminate.
\subsection{Related Work on Mechanised Proof Theory}
\label{sec:relat-work-mech}
We are aware of only three other attempts to formalise proof theory,
cut elimination or strong normalisation.
The first attempt is the work of Pfenning where he formalises the
admissibility of cut for classical, intuitionistic and linear logic
using the logical framework Elf, which itself is based upon the
dependent type theory LF \cite{pfenning-structural-lics94,%
pfenning-structural-lf,pfenning-structural-linear}.
Elf is based
upon logic programming and uses a Prolog-like backtracking procedure
for executing the encoded definitions. When initiating our work, we
compared various ways to encode \dRA\ and reported the results in
\cite{dawson-gore-embedding-comparing}. We found, for example, that
the Elf implementation reports success even when certain
transformations, essential to cut-elimination, are deleted from the
encoding! Our conclusion was that the Elf implementation was
essentially a program for cut-elimination, which returns a cut-free
derivation when given a derivation containing cuts, rather than a full
formalisation of cut-elimination. Pfenning essentially says the same
thing in the conclusion of \cite{pfenning-structural-lics94} where he
states:
\begin{quote}\it
Once the structural proof of admissibility has been found and
implemented, it is natural to ask if it can also be encoded in
stronger frameworks such as Coq [DFH+93] so that structural
inductions are made explicit and the proof is fully formally
verified.
\end{quote}
The second attempt is the work of Matthews \textit{et al}
\cite{matthews-smaill-basin-experience,%
basin-matthews-structuring,matthews-implementing-isabelle}
which
implements Feferman's FS$_0$ in Prolog and Isabelle, and uses it to
formalise and extend various meta-theoretical formal systems. It
should be possible to formalise cut-elimination in such an
implementation, but it does not appear to have been done.
The third attempt is the work of Mikhajlova and von Wright
\cite{mikhajlova-vonwright-isomorphism}. This is the closest to our
work since it provides a formalisation of a sequent calculus for
first-order logic in the system HOL. But this work makes no attempt to
prove a cut-elimination or strong normalisation result, and as we
point out later, actually contains an unfortunate bug.
end of comment }
\section{A Deep Embedding of \dRA\ in Isabelle/HOL}
\label{sec:deep-embedding-dra}
In \cite{dawson-gore-embedding-comparing}, we describe our initial
attempts to formalise display calculi in various logical frameworks,
and describe why we chose Isabelle/HOL for this work. To make the
current paper self-contained, we now describe the Isabelle/HOL data
structures used to represent formulae, structures, sequents and
derivations.
%Although we have tried to make the paper self-contained,
We assume that the reader is familiar with ML and logical frameworks
in general.
% This section also appears in our LICS02 submission
% \cite{dawson-gore-machine-checked-strong-normalisation-lics}.
\subsection{Representing Formulae, Structures, Sequents and Rules}
%\cc{dt.tex}
% \begin{figure}[t]
% \centering
% \begin{verbatim}
% datatype formula = Btimes formula formula ("_ && _" [68,68] 67)
% | Rtimes formula formula ("_ oo _" [68,68] 67)
% | Bplus formula formula ("_ v _" [64,64] 63)
% | Rplus formula formula ("_ ++ _" [64,64] 63)
% | Bneg formula ("--_" [70] 70)
% | Rneg formula ("_^" [75] 75)
% | Btrue ("T")
% | Bfalse("F")
% | Rtrue ("r1")
% | Rfalse("r0")
% | FV string
% | PP string
% \end{verbatim}
% \caption{Isabelle/HOL Representation of Formulae of \dRA.}
% \label{fig:isabelle-formulae}
% \end{figure}
% \begin{figure}[t]
% \centering
% \begin{verbatim}
% datatype formula = Btimes formula formula ("_ && _" [68,68] 67)
% | Rtimes formula formula ("_ oo _" [68,68] 67)
% | Bplus formula formula ("_ v _" [64,64] 63)
% | Rplus formula formula ("_ ++ _" [64,64] 63)
% | Bneg formula ("--_" [70] 70) | Rneg formula ("_^" [75] 75)
% | Btrue ("T") | Bfalse("F") | Rtrue ("r1") | Rfalse("r0")
% | FV string | PP string
% \end{verbatim}
% \caption{Isabelle/HOL Representation of Formulae of \dRA.}
% \label{fig:isabelle-formulae}
% \end{figure}
An actual derivation in a Display Calculus involves structures
containing formulae which are composed of primitive propositions
(which we typically represent by $p,q,r$). It uses rules which are
\emph{expressed} using structure and formula variables, typically
$X,Y,Z$ and $A,B,C$ respectively, to represent structures and formulae
made up from primitive propositions. Nonetheless, in deriving
theorems or derived rules we will often use a rule instance where the
original variables in the rule are replaced by other variables, rather
than actual formulae. We may, for example, have to take the cut rule
as shown below left and substitute $B \land C$ for $A$, substitute
$(Z, D)$ for $X$ and substitute $C \lor D$ for $Y$ to get the cut rule
instance shown below right, and reason about this instance.
\[
\brule{(cut)}
{$X \vdash A$}
{$A \vdash Y$}
{$X \vdash Y$}
\hspace{1cm}
\brule{}
{$Z, D \vdash B \land C$}
{$B \land C \vdash C \lor D$}
{$Z, D \vdash C \lor D$}
\]
Our Isabelle formulation must allow this since variables such as
$X,Y,Z$ and $A,B,C$ are not part of the language of a Display
Calculus, but are part of the meta-language used when reasoning about
Display Calculi.
% In our Isabelle formulation we use the terms
% \texttt{SV} \textit{name} and \texttt{FV} \textit{name} to represent
% such variables, and we set up the machinery for substituting arbitrary
% structure or formulae expressions for these variables and using the
% result in derivations.
Formulae of \dRA\ are therefore represented by the datatype
below:
% in Figure~\ref{fig:isabelle-formulae}.
\begin{verbatim}
datatype formula = Btimes formula formula ("_ && _" [68,68] 67)
| Rtimes formula formula ("_ oo _" [68,68] 67)
| Bplus formula formula ("_ v _" [64,64] 63)
| Rplus formula formula ("_ ++ _" [64,64] 63)
| Bneg formula ("--_" [70] 70) | Rneg formula ("_^" [75] 75)
| Btrue ("T") | Bfalse("F") | Rtrue ("r1") | Rfalse("r0")
| FV string | PP string
\end{verbatim}
The
constructors \texttt{FV} represents formula variables which appear in
the statement of a rule or theorem, and which are instantiated to
actual formulae of \dRA\ when constructing derivations. The
constructor \texttt{PP} represents a primitive proposition variable
$p$: once again this lives at the meta-level.
% \begin{figure}[t]
% \centering
% \begin{verbatim}
% datatype structr = Comma structr structr | SemiC structr structr
% | Star structr | Blob structr | I | E | Structform formula | SV string
% \end{verbatim}
% \caption{Isabelle/HOL Representation of Structures of \dRA.}
% \label{fig:isabelle-structures}
% \end{figure}
% \begin{figure}[t]
% \centering
% \begin{verbatim}
% datatype structr = Comma structr structr
% | SemiC structr structr
% | Star structr
% | Blob structr
% | I
% | E
% | Structform formula
% | SV string
% \end{verbatim}
% \caption{Isabelle/HOL Representation of Structures of \dRA.}
% \label{fig:isabelle-structures}
% \end{figure}
% Structures of \dRA\ are represented by the datatype declaration shown
% in Figure~\ref{fig:isabelle-structures}.
% The operator
% \texttt{Structform} causes a formula to be ``cast'' into a structure,
% since a formula is a special case of a structure (as in the premises
% of the cut rule given above). The constructor \texttt{SV} represents
% structure variables which appear in the statement of a rule or
% theorem, and which are instantiated to actual structures of \dRA\ when
% constructing derivations. Since we must reason about arbitrary
% derivations, we have to allow derivations to contain structure
% variables and we must reason about the instantiations explicitly. We
% therefore cannot use Isabelle's built-in unification facility for
% instantiating its ``scheme variables'' as explained in more detail in
% \cite{dawson-gore-embedding-comparing}.
Structures of \dRA\ are represented by the datatype below:
\begin{verbatim}
datatype structr = Comma structr structr | SemiC structr structr
| Star structr | Blob structr |I|E| Structform formula | SV string
\end{verbatim}
The operator \texttt{Structform} ``casts '' a formula into
a structure, since a formula is a special case of a structure (as in
the premises of the cut rule given above). The constructor \texttt{SV}
represents structure variables which appear in the statement of a rule
or theorem, and which are instantiated to actual structures of \dRA\
when constructing derivations. Since we must reason about arbitrary
derivations, we have to allow derivations to contain structure
variables and we must reason about the instantiations explicitly. We
therefore cannot use Isabelle's built-in unification facility for
instantiating its ``scheme variables'' as explained in more detail in
\cite{dawson-gore-embedding-comparing}. Likewise, formulae of \dRA\
are represented by a datatype which include a constructor \texttt{FV}
for formula variables which can be instantiated to actual formulae of
\dRA, and a constructor \texttt{PP} for a primitive proposition
variable $p$.
The notation in parentheses in the definition of datatype
\texttt{formula}
%Figure~\ref{fig:isabelle-formulae}
describe an alternative infix syntax, closer to the actual
syntax of \dRA. Some complex manipulation of the syntax, available
through Isabelle's ``parse translations'' and ``print translations'',
allows structure variables and constants to be prefixed by the symbol
\texttt{\$}, and the notations \texttt{FV}, \texttt{SV} and
\texttt{Structform} to be omitted. For technical reasons related to
this, a different method is used to specify the alternative infix
syntax for structures and sequents: details omitted.
Sequents and rules of \dRA\ are represented by the Isabelle/HOL
datatypes:
\begin{verbatim}
datatype sequent = Sequent structr structr
datatype rule = Rule (sequent list) sequent
| Bidi sequent sequent | InvBidi sequent sequent
\end{verbatim}
% \begin{verbatim}
% datatype sequent = Sequent structr structr
% datatype rule = Rule (sequent list) sequent
% | Bidi sequent sequent
% | InvBidi sequent sequent
% \end{verbatim}
The premises of a rule are represented using a list of sequents while
the conclusion is a single sequent. Thus \texttt{Rule prems concl}
means a rule with premises \texttt{prems} and conclusion
\texttt{concl}. Many single-premise rules of display calculi are
defined to be usable from top to bottom as well as from bottom to top:
the two constants \texttt{Bidi} and \texttt{InvBidi} allow us to cater
for these. Thus \texttt{Bidi prem concl} means an invertible, or
``bi-directional'' rule (such as the display postulates) and
\texttt{InvBidi prem concl} means the rule \texttt{Bidi prem concl}
used in the inverted sense to derive the conclusion \texttt{prem} from
the premise \texttt{concl}.
A sequent \texttt{(Sequent X Y)} can also be represented as
\texttt{\$X |- \$Y}. Thus the term \texttt{Sequent (SV ''X'')
(Structform (FV ''A''))} is printed, and may be entered, as
\texttt{(\$''X'' |- ''A'')}. Functions \texttt{premsRule} and
\texttt{conclRule} return the premise list and the conclusion of a
rule respectively. A structure expression is \emph{formula-free} if it
does not contain any formula as a sub-structure: that is, if it does
not contain any occurrence of the operator \texttt{Structform}. A
formula-free sequent is defined similarly. The constant \texttt{rls}
represents the set of rules of \dRA, encoded using the datatypes just
described: we omit the details of this code.
\subsection{Handling Substitutions Explicitly}
Since a ``deep'' embedding requires handling substitution explicitly,
we now give definitions relating to substitution for structure and
formula variables. We first give some type abbreviations, and then
the types of a sample of the functions.
% fFind :: "fSubst => string => formula"
% sFind :: "sSubst => string => structr"
% subDT :: "fsSubst => dertree => dertree"
% ruleSubst :: "fsSubst => rule => rule"
% seqSubst :: "fsSubst => sequent => sequent"
% strSubst :: "fsSubst => structr => structr"
% fmlSubst :: "fSubst => formula => formula"
%
\begin{verbatim}
fSubst = "(string * formula) list"
sSubst = "(string * structr) list"
fsSubst = "fSubst * sSubst"
sFind :: "sSubst => string => structr"
ruleSubst :: "fsSubst => rule => rule"
seqSubst :: "fsSubst => sequent => sequent"
\end{verbatim}
%
% Thus \texttt{sFind} is a function of two curried arguments, of types
% \texttt{sSubst} and \texttt{string}, and result type \texttt{structr},
% and \texttt{sSubst} is the type of lists of (\texttt{string},
% \texttt{structr}) pairs.aa
To substitute for a variable, for example
\texttt{SV ''X''}, in some object, using the substitution
\texttt{(fsubs, ssubs)}, we use \texttt{sFind} to obtain the first
pair (if any) in \texttt{ssubs} whose first component is \texttt{''X''}.
If that pair is \texttt{(''X''}, $X$\texttt{)}, then \texttt{sFind}
returns $X$, and each occurrence of \texttt{SV ''X''} in the given
object is replaced by $X$.
There are functions which substitute for every
formula or structure variable in a derivation tree (defined below),
rule, sequent, structure or formula.
\subsection{Representing Derivations as Trees}
We use the term ``derivation'' for a proof \emph{within} the sequent
calculus, reserving the term ``proof'' for a meta-theoretic proof of a
theorem \emph{about} the sequent calculus. We model a derivation tree
(type \texttt{dertree}) using the following datatype:
\begin{verbatim}
datatype dertree = Der sequent rule (dertree list) | Unf sequent
\end{verbatim}
In \texttt{Der seq rule dts} the subterm \texttt{seq} is the
sequent at the root (bottom) of the tree, and \texttt{rule} is the
rule used in the last (bottom) inference. If the tree
represents a real derivation, sequent \texttt{seq} will be an
instance of the conclusion of \texttt{rule}, and the
corresponding instances of the premises of \texttt{rule} will be
the roots of the trees in the list \texttt{dts}. We say that the root
``node'' of such a tree is \emph{well-formed}. The trees in
\texttt{dts} are the \emph{immediate} subtrees of \texttt{Der seq rule
dts}.
The leaves of a derivation tree are either axioms with no premises, or
``\texttt{Unf}inished'' sequents whose derivations are currently
unfinished. The derivation tree for a derivable sequent will therefore
have no \texttt{Unf} leaves and we call such a derivation tree
\emph{finished}. The derivation tree for a derived rule will have the
premises of the rule as its \texttt{Unf} leaf sequents.
Display calculi typically use the initial sequent $p \vdash p$, using
primitive propositions only. It is then proved that the sequent $A
\vdash A$ is derivable for all formulae $A$ by induction on the size
of $A$, where $A$ \emph{stands for} a formula composed of primitive
propositions and logical connectives. We proved this as the theorem
\texttt{idfpp}. However we also need to reason about the derivation
trees of derived rules; such trees may contain formula and structure
variables as well as primitive propositions, and may use the (derived)
rule $A \vdash A$, for arbitrary formula $A$. We therefore sometimes
must treat $A \vdash A$ (where $A$ is a formula variable) as an axiom.
Thus the derivation tree \texttt{Der (''A'' |- ''A'') idf []} stands
for a finished derivation, which uses the \texttt{idfpp} lemma that $A
\vdash A$ is derivable for all $A$, whereas the derivation tree
\texttt{Unf (''A'' |- ''A'')} stands for an unfinished derivation with
unfinished premise $A \vdash A$.
For example, the unfinished derivation tree shown below at left is
represented as the Isabelle/HOL term shown below at right where
\texttt{''A'' |- PP p \&\& ''A''} stands for $A \vdash p \land A$ and
\texttt{cA} and \texttt{ands} are the contraction and ($\vdash \land
$) rules, and
\texttt{idf} is the derived rule $A \vdash A$:\\[1em]
\begin{tabular}[c]{rr}
\begin{minipage}[c]{0.3\linewidth}
{\vpf
\bpf
\A "$A \vdash p$"
\A "$A \vdash A$"
\B [1em] "$A, A \vdash p \land A$" "($\vdash \land $)"
\U "$A \vdash p \land A$" "(\textsl{ctr})"
\epf
}
\end{minipage}
&
\begin{minipage}[c]{0.7\textwidth}
\begin{verbatim}
Der (''A'' |- PP p && ''A'') cA
[Der (''A'', ''A'' |- PP p && ''A'') ands
[Unf (''A'' |- PP p),
Der (''A'' |- ''A'') idf []]]
\end{verbatim}
\end{minipage}
\end{tabular}
\subsection{Reasoning About Derivations and Derivability}
In this section we describe various functions which allow us to reason
about derivations in \dRA. The types for these functions are shown in
Figure~\ref{fig:functions-reasoning-about-derivations}.
\begin{figure}[t]
\centering
\begin{verbatim}
allDT :: "(dertree => bool) => dertree => bool"
allNextDTs :: "(dertree => bool) => dertree => bool"
wfb :: "dertree => bool"
frb :: "rule set => dertree => bool"
premsDT :: "dertree => sequent list"
conclDT :: "dertree => sequent"
IsDerivable :: "rule set => rule => bool"
IsDerivableR :: "rule set => sequent set => sequent => bool"
\end{verbatim}
% IsDerivableB :: "rule set => sequent => sequent => bool"
\caption{Functions for reasoning about derivations}
\label{fig:functions-reasoning-about-derivations}
\end{figure}
\begin{description}
\item[\texttt{allDT f dt}] holds if property \texttt{f} holds for
% every sub-tree in the derivation tree \texttt{dt}.
every sub-tree in the tree \texttt{dt}.
\item[\texttt{allNextDTs f dt}] holds if property \texttt{f} holds for
every proper sub-tree of \texttt{dt}.
\item[\texttt{wfb (Der concl rule dts)}] holds if sequent rule
\texttt{rule} has an instantiation with conclusion instance
\texttt{concl} and premise instances which are the conclusions of the
derivation trees in the list \texttt{dts}. (``\texttt{wfb}'' stands for
\emph{well-formed}).
\item[\texttt{allDT wfb dt}] holds if every sub-tree of the derivation
tree \texttt{dt} satisfies \texttt{wfb} (ie, if every node in
\texttt{dt} is well-formed). Such a derivation is said to be
\emph{well-formed}.
\item[\texttt{frb rules (Der concl rule dts)}] holds when the lowest
rule \texttt{rule} used in a derivation tree \texttt{Der concl rule
dts} belongs to the set \texttt{rules}.
\item[\texttt{allDT (frb rules) dt}] holds when every rule used in
a derivation tree \texttt{dt} belongs to the set \texttt{rules}.
\item[\texttt{premsDT dt}] returns a list of all ``premises''
(unfinished leaves) of the derivation tree \texttt{dt}. That is, the
sequents found in nodes of \texttt{dt} of the form \texttt{Unf seq}.
\item[\texttt{conclDT dt}] returns the end-sequent of the derivation
tree \texttt{dt}. That is, the conclusion of the bottom-most rule
instance.
\end{description}
So \texttt{wfb (Der seq rule dts)} means that the bottom node of the
derivation tree \texttt{Der seq rule dts} is \emph{well-formed}. We
say a derivation tree \texttt{dt} is \emph{well-formed} if every node
in it is well-formed, and express this as \texttt{allDT wfb dt},
since \texttt{allDT f dt} means that property \texttt{f} holds for
every sub-tree in the derivation tree \texttt{dt}. Also,
\texttt{allNextDTs f dt} means that every proper sub-tree of
\texttt{dt} satisfies \texttt{f}.
The property \texttt{allDT (frb rules)} holds when every rule used in
a derivation tree belongs to the set \texttt{rules}. The function
\texttt{premsDT} returns a list of all ``premises'' (unproved
assumptions) of the derivation tree, that is, the sequents found in
nodes of the form \texttt{Unf seq}.
A tree representing a real derivation in a display calculus naturally
is well-formed and uses the rules of the calculus. Further, a tree
which derives a sequent (rather than a derived rule) is finished, that
is, it has no unfinished leaves.
The cut-elimination procedure involves transformations of derivation
trees; in discussing these we will only be interested in derivation
trees which actually derive a sequent, so we make the following
definition.
\begin{definition}
A derivation tree \texttt{dt} is \emph{valid} if
it is well-formed,
it uses rules in the set of rules \texttt{rules} of the calculus, and
it has no unfinished leaves.
% from HOL_DT.thy
\begin{verbatim}
valid_def = "valid ?rules ?dt ==
allDT wfb ?dt & allDT (frb ?rules) ?dt & premsDT ?dt = []"
\end{verbatim}
\end{definition}
We have explicitly added question marks in front of \texttt{rules} and
\texttt{dt} to flag that they are free variables, even though the
question mark would be absent in the Isabelle/HOL theory file itself:
we follow this practice throughout this paper.
\begin{definition}[\texttt{IsDerivableR}]
\texttt{IsDerivableR rules prems' concl} holds iff
there exists a derivation tree \texttt{dt} which
uses only rules contained in the set \texttt{rules},
is well-formed,
has conclusion \texttt{concl},
and
has premises from set \texttt{prems'}.
\begin{verbatim}
"IsDerivableR ?rules ?prems' ?concl == (EX dt.
allDT (frb ?rules) dt & allDT wfb dt &
conclDT dt = ?concl & set (premsDT dt) <= ?prems')"
\end{verbatim}
\end{definition}
Here, \texttt{set} is a function that allows us to treat its argument
as a set rather than a list, and \texttt{<=} is the subset relation
$\subseteq$.
Finally, \texttt{IsDerivable rules rule} holds iff \texttt{rule} may
be obtained as a derived rule, from the (unordered) set
\texttt{rules}.
% Thus, for example, if \texttt{rule} is of the form
% \texttt{Rule prems concl},
That is, if \texttt{rule} has premise list \texttt{prems} and conclusion
\texttt{concl},
then \texttt{IsDerivable rules rule} is
equivalent to \texttt{IsDerivableR rules (set prems) concl}.
\comment{
If \texttt{rule} is a bi-directional rule, say
\texttt{Bidi prem concl},
then \texttt{IsDerivable rules rule} is equivalent to
\texttt{IsDerivableB rules prem concl} defined below:
\begin{verbatim}
"IsDerivableB ?rules ?prem ?concl ==
IsDerivableR ?rules {?prem} ?concl &
IsDerivableR ?rules {?concl} ?prem"
\end{verbatim}
}
\subsection{Reasoning About Derivability}
\label{subsec:theor-about-deriv}
Among the results we have proved about the derivability relation are
the following theorems.
\comment{ Note that \texttt{IsDerivableR
rules prems concl} means that conclusion \texttt{concl} is derivable
from premises \texttt{prems} using rules \texttt{rules} (ie, except
for the type of \texttt{prems}, the same as \texttt{IsDerivable rules
(Rule prems concl)}).
end of comment }
The first is a transitivity result, relating to a derivation of a
conclusion from premises which are themselves derived.
\begin{theorem}%[\texttt{IsDerivableR\_trans}]
If \texttt{concl} is derivable from
\texttt{prems'} and each sequent
\texttt{p}
in \texttt{prems'}
is derivable from \texttt{prems} then
\texttt{concl} is derivable from \texttt{prems}.
\begin{verbatim}
IsDerivableR_trans = "[| IsDerivableR ?rules ?prems' ?concl ;
ALL p:?prems'. IsDerivableR ?rules ?prems p |] ==>
IsDerivableR ?rules ?prems ?concl" : thm
\end{verbatim}
\end{theorem}
The appellation ``\texttt{: thm}'' indicates a statement that has been
proved in Isabelle/HOL as a theorem, from previous Isabelle/HOL
definitions: we follow this practice for theorems and lemmata
throughout this paper.
The second is a a different sort of transitivity result,
relating to a derivation using rules which are themselves derived.
\begin{theorem}[\texttt{IsDerivableR\_deriv}]
If
each \texttt{rule} in \texttt{rules'} is derivable using \texttt{rules},
and
\texttt{concl} is derivable from \texttt{prems} using the set \texttt{rules'},
then
\texttt{concl} is derivable from \texttt{prems} using \texttt{rules}.
\begin{verbatim}
IsDerivableR_deriv = "[| ALL rule:?rules'.
IsDerivable ?rules rule ; IsDerivableR ?rules' ?prems ?concl |]
==> IsDerivableR ?rules ?prems ?concl" : thm
\end{verbatim}
\end{theorem}
In another reported formalisation of the notion of derivations in a
logical calculus \cite{mikhajlova-vonwright-isomorphism}, these two
properties were, in effect, stated rather than proved. The
disadvantage of proceeding that way is the possibility of stating them
incorrectly. For example, \cite{mikhajlova-vonwright-isomorphism}
defines \texttt{IsDerivable} inductively as a relation which is
transitive in both the senses of the results above; see the second and
third clauses of the definition on
\cite[page~302]{mikhajlova-vonwright-isomorphism}. However in the
third clause, which deals with the case of a result being provable
using derived rules, inappropriate use of an existential quantifier
leads to the incorrect result that $P \to Q$ could be used as a
derived rule on the grounds that one instance of it, say
$\textsl{True} \to \textsl{True}$, is provable.
\comment{
Finally we have a recursive characterisation of derivability.
\begin{theorem}[\texttt{IsDerivableR\_recur}]
A conclusion \texttt{concl} is derivable from premises \texttt{prems}
using rules \texttt{rules} if and only if either \texttt{concl} is one of
\texttt{prems}, or there exists an instantiated \texttt{rule}
obtained from \texttt{rules}
and the conclusion of \texttt{rule} is \texttt{concl}
and the premises of \texttt{rule} are themselves
derivable from \texttt{prems} using \texttt{rules}.
\begin{verbatim}
IsDerivableR_recur = "IsDerivableR ?rules ?prems ?concl = (
?concl : ?prems | (EX rule. ruleFromSet rule ?rules &
conclRule rule = ?concl & (ALL p : set (premsRule rule).
IsDerivableR ?rules ?prems p)) )" : thm
\end{verbatim}
\end{theorem}
Here, \texttt{ruleFromSet rule rules} means that \texttt{rule} is an
instantiation of a rule in \texttt{rules} (which may be the inverse
sense of a bi-directional rule), and \texttt{premsRule rule} is a list
containing the premises of rule \texttt{rule}.
}
\section{An Operational View of Cut-Elimination}
\label{sec:an-operational-view}
We now give an operational view of cut-elimination, to explain the
steps involved in the overall cut-elimination procedure a l\`a Belnap
\cite{belnap-display}. We assume familiarity with notions like
``parametric ancestors'' of a cut formula \cite{belnap-display}.
% Some subsections have \textit{analogues} in our LICS02 paper
% \cite{dawson-gore-machine-checked-strong-normalisation-lics}, but the
% results and details are different.
\subsection{Principal Cuts and Belnap's Condition C8}
\label{subsec:princ-cuts-beln}
\begin{definition}
An application of (cut) is \emph{left-principal}
[\emph{right-principal}] if the cut-formula is the principal formula
of the left [right] premise of the cut rule.
\end{definition}
\begin{figure}[t]
\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-new}
\label{fig-orcut-new}
\end{figure}
\begin{figure}[t]
\vpf
\begin{center}
\bpf
\A "$\Pi_{ZAB}$"
\U "$Z \vdash A, B$"
\U "$*A, Z \vdash B$" "($cs1$)"
\A "$\Pi_{BY}$"
\U "$B \vdash Y$"
\B [2em] "$*A, Z \vdash Y$" "($cut$)"
\U "$Z \vdash A, Y$" "($\overline{cs1}$)"
\U "$Z, *Y \vdash A$" "($cs2$)"
\A "$\Pi_{AX}$"
\U "$A \vdash X$"
\B [2em] "$Z, *Y \vdash X$" "($cut$)"
\U "$Z \vdash X, Y$" "($\overline{cs2}$)"
\epf
\end{center}
\caption{Transformed principal cut on formula $A \lor B$}
%\cc{fig-orcut'}
\label{fig-orcut'-new}
\end{figure}
Given a derivation (tree) with one principal cut, such as in
Figure~\ref{fig-orcut-new}, Belnap's condition (C8) on the rules of a
Display Calculus ensures that the given derivation can be transformed
into one whose cuts are on smaller formulae. For example, the
principal cut on $A \lor B$ shown in Figure~\ref{fig-orcut-new} can be
replaced by the derivation shown in Figure~\ref{fig-orcut'-new}, where
($cs1$), ($cs2$), ($\overline{cs1}$) and ($\overline{cs1}$) are two of
the display postulates and their inverses respectively. The
replacement derivation contains cuts only on $A$ and $B$, which are
smaller formulae than $A \lor B$.
\begin{figure}[t]
\vpf
\begin{center}
\bpf
\A "$A \vdash A$"
\A "$\Pi_{AY}$"
\U "$A \vdash Y$" "(intro-$A$)"
\B [2em] "$A \vdash Y$" "($cut$)"
\epf
%\qquad $\longrightarrow$ \qquad
\qquad becomes \qquad
\bpf
\A "$\Pi_{AY}$"
\U "$A \vdash Y$"
\epf
\end{center}
\caption{Principal cut where cut-formula is introduced by identity axiom}
%\cc{fig-idcut}
\label{fig-idcut-new}
\end{figure}
There is one such transformation for every connective and this is the
basis for a step of the cut-elimination proof which depends on
induction on the structure or size of the cut-formula. The base case
of this induction is where the cut-formula is
% a single formula variable or primitive
% proposition, when it is necessarily
introduced by the identity axiom. Such a cut, and its removal, are
shown in Figure~\ref{fig-idcut-new}. We return to the actual
mechanisation in Section~\ref{principal-cuts}.
The transformation of a principal cut on $A$ into one or more cuts on
strict subformulae of $A$ is known as a ``principal move''. We now
need a way to turn arbitrary cuts into principal ones.
\subsection{Transforming Arbitrary Cuts Into Principal Ones}
\label{s-mcp}
\begin{figure}[t]
\hfill
\bpf
\A "$\Pi[A]$"
\U "$Z[A] \vdash A $" "(intro-$A$)"
\U "$\Pi_L[A]$" "($\pi$)"
\U "$X \vdash A $" "($\rho$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [2em] "$X \vdash Y$" "($cut$)"
\epf
\hspace{0.1cm}
\bpf
\A "$\Pi'[Y]$"
\U "$Z[Y] \vdash A $" "(intro-$A$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [2em] "$Z[Y] \vdash Y$" "($cut$)"
\U "$\Pi_L[Y]$" "($\pi$)"
\U "$X \vdash Y $" "($\rho$)"
\epf
\hfill \mbox{}
\caption{Making a cut left-principal}
\label{fig-cut-p-new}
\end{figure}
In the case of a cut that is not left-principal, say we have a tree
like the one on the left in Figure~\ref{fig-cut-p-new}. 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 Figure~\ref{fig-cut-p-new} shows this in the case where $A$ is
introduced at just one point.
In Figure~\ref{fig-cut-p-new}, the notation $\Pi_L[A]$ and $Z[A]$
means that the sub-derivation $\Pi_L$ and structure $Z$ may contain
occurrences of $A$ which are parametric ancestors of the cut-formula
$A$: thus (intro-$A$) is the lowest rule where $A$ is the principal
formula on the right of $\vdash$. The notation $\Pi_L[Y]$ and $Z[Y]$
means that all such ``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 the
new sub-derivation $\Pi_L[Y]$ are the same as the rules used in
$\Pi_L$; thus it remains to be proved that $\Pi_L[Y]$ is well-formed.
The resulting cut in the diagram on the right of
Figure~\ref{fig-cut-p-new} is left-principal. Notice that the
original sub-derivation $\Pi$ may be transformed into a
\textit{different} sub-derivation $\Pi'$ during this process since the
parametric ancestors of $A$ occurring in $\Pi[A]$ will in turn need to
be ``cut away'' below where they are introduced, and replaced by $Y$.
Belnap's conditions guarantee 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 Figure~\ref{fig-cut-p-new}. Other conditions of
Belnap (\textit{e.g.} 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.
% 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
% Figure~\ref{fig-cut-id-new}. Again, the diagram is specific to the case
% where $A$ is introduced at just one point.
This construction generalises easily to the case where $A$ is
introduced (in one of the above ways) at more than one point
(\textit{e.g.} arising from use of one of the rules where a structure
variable, whose instantiation contains occurrences of $A$, appears
twice in the premises) or where $A$ is ``introduced'' by use of the
weakening rule. Our description of the procedure is very loose and
informal -- the formality and completeness of detail is reserved for
the machine proof!
% \begin{figure}[t]
% \hfill
% \bpf
% \A "$A \vdash A $"
% \U "$\Pi_L[A]$" "($\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[Y]$" "($\pi$)"
% \U "$X \vdash Y $" "($\rho$)"
% \epf
% \hfill \mbox{}
% \caption{Making a cut left-principal -- $A$ introduced by identity axiom}
% \label{fig-cut-id-new}
% \end{figure}
Subsequently, the ``mirror-image'' procedure is followed, to convert a
left-principal cut into one or more (left- and right-)principal cuts.
The process of making a cut left-principal, or of making a
left-principal cut (left and right) principal is called a ``parametric
move''.
\section{Functions for Reasoning About Cuts}
\label{subsec:funct-reas-about}
We therefore need functions, with the following types, for reasoning
about derivations which end with a cut:
%in Figure~\ref{fig:functions-reasoning-about-cuts-new}.
\begin{verbatim}
cutOnFmls :: "formula set => dertree => bool"
cutIsLP :: "formula => dertree => bool"
cutIsLRP :: "formula => dertree => bool"
\end{verbatim}
Each require the bottom node of the derivation tree to be of the form
\texttt{Der seq rule dts}, and that if \texttt{rule} is \cut, then:
for \texttt{cutOnFmls s} the cut is on a formula in the set
\texttt{s}; for \texttt{cutIsLP A} the cut is on formula \texttt{A}
and is left-principal; and for \texttt{cutIsLRP A} the cut is on
formula \texttt{A} and is (left- and right-)principal.
% \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 Figure~\ref{fig-orcut-new})
% \item[\texttt{cutIsLRP A} :]
% the cut is on formula \texttt{A} and is (left- and right-)principal.
% \end{description}
Note that it also follows from the actual definitions that a derivation tree
satisfying any of \texttt{allDT (cutOnFmls s)}, \texttt{allDT (cutIsLP A)}
and \texttt{allDT (cutIsLRP A)} has no unfinished leaves: we omit details.
\subsection{Dealing With Principal Cuts}
\label{principal-cuts}
% \begin{figure}[t]
% \centering
% \begin{verbatim}
% cutOnFmls :: "formula set => dertree => bool"
% cutIsLP :: "formula => dertree => bool"
% cutIsLRP :: "formula => dertree => bool"
% \end{verbatim}
% \caption{Functions for reasoning about cuts}
% \label{fig:functions-reasoning-about-cuts-new}
% \end{figure}
% FOLLOWING INSERTED FOR TPHOLS PAPER
For each logical connective and constant in the calculus, we prove
that a derivation ending in a (left and right) principal cut, where
the main connective of the cut formula is that connective, can be
transformed into another derivation of the same end-sequent, using
only cuts (if any) on formulae which are strict subformulae of the
original cut-formula. Some SML code is used to do part of the work of
finding these replacement derivation trees. But the proof that such a
replacement derivation tree is well-formed, for example, has to be
done using the theorem prover. Here is the resulting theorem for
$\lor$: there is an analogous theorem for every logical connective and
logical constant.
% Although Theorem~\ref{thm:orc8} assumes that
% \texttt{dt} may contain cuts on the subformulae $A$ and $B$, it is
% used when \texttt{dt} contains only one (bottom-most) cut, so such
% smaller cuts do not occur in \texttt{dt}.
% \begin{theorem}[\texttt{orC8}]
% \label{thm:orc8}
% Assume we are given a valid derivation tree \texttt{dt}. Assume that
% if the bottom rule of \dt\ is \cut, then the cut is principal and
% its cut-formula is $A \lor B$. Also assume that any cuts above the
% root of \dt\ have either $A$ or $B$ as cut-formula. Then there
% is a valid derivation tree \texttt{dtn} with the same conclusion as
% \texttt{dt}, such that \emph{all} cuts in \texttt{dtn} have either
% $A$ or $B$ as cut-formula.
% \begin{verbatim}
% orC8 = "[| allDT wfb ?dt; allDT (frb rls) ?dt;
% cutIsLRP (?A v ?B) ?dt; allNextDTs (cutOnFmls {?B, ?A}) ?dt |]
% ==> EX dtn. conclDT dtn = conclDT ?dt & allDT wfb dtn &
% allDT (frb rls) dtn & allDT (cutOnFmls {?B, ?A}) dtn" : thm
% \end{verbatim}
% \end{theorem}
\begin{theorem}[\texttt{orC8}]
\label{thm:orc8}
Assume we are given a valid derivation tree \texttt{dt} whose only
instance of cut (if any) is at the bottom, and that this cut is
principal with cut-formula $A \lor B$. Then there is a valid
derivation tree \texttt{dtn} with the same conclusion as \texttt{dt},
such that \emph{each} cut (if any) in \texttt{dtn} has $A$ or $B$ as
cut-formula.
\begin{verbatim}
orC8 = "[| allDT wfb ?dt; allDT (frb rls) ?dt;
cutIsLRP (?A v ?B) ?dt; allNextDTs (cutOnFmls {}) ?dt |]
==> EX dtn. conclDT dtn = conclDT ?dt & allDT wfb dtn &
allDT (frb rls) dtn & allDT (cutOnFmls {?B, ?A}) dtn" : thm
\end{verbatim}
\end{theorem}
\subsection{Making A Cut (Left) Principal}
\label{make-cut-lp}
%We define a relation between two sequents.
For boolean \texttt{b}, structures \texttt{X}, \texttt{Y}
and sequents \texttt{seq1} and \texttt{seq2},
the expression \texttt{seqRep b X Y seq1 seq2} is true iff
\texttt{seq1} and \texttt{seq2} are the same, except that (possibly)
one or more occurrences of \texttt{X} in \texttt{seq1} are replaced by
corresponding occurrences of \texttt{Y} in \texttt{seq2}, where,
when \texttt{b} is \texttt{True} [\texttt{False}],
such differences occur only in succedent [antecedent] positions.
For two lists \texttt{seql1} and \texttt{seql2} of sequents,
\texttt{seqReps b X Y seql1 seql2} holds if each $n$th member of
\texttt{seql1} is related to the $n$th member of \texttt{seql2}
by \texttt{seqRep b X Y}.
Next come
%The following are
the main theorems used in the mechanised
proof based on making cuts (left and right) principal. Several
% of them
use the relation \texttt{seqRep pn (Structform A) Y}, since
\texttt{seqRep pn (Structform A) Y seqa seqy} holds when \texttt{seqa}
and \texttt{seqy} are corresponding sequents in the trees $\Pi_L[A]$
and $\Pi_L[Y]$ from Figure~\ref{fig-cut-p-new}.
\begin{theorem}[\texttt{seqExSub1}]
If sequent \texttt{pat} is formula-free and does not contain any structure
variable more than once, and can be instantiated to obtain sequent
\texttt{seqa}, and \texttt{seqRep pn (Structform A) Y seqa seqy}
holds, then \texttt{pat} can be instantiated to obtain sequent \texttt{seqy}.
\end{theorem}
\begin{verbatim}
seqExSub1 = "[| ~ seqCtnsFml ?pat; noDups (seqSVs ?pat);
seqSubst (?fs, ?suba) ?pat = ?seqa;
seqRep ?pn (Structform ?A) ?Y ?seqa ?seqy |]
==> EX suby. seqSubst (?fs, suby) ?pat = ?seqy" : thm
\end{verbatim}
To see why \texttt{pat} must be formula-free, suppose that
\texttt{pat} contains \texttt{Structform (FV ''B'')}, which means that
\texttt{pat} is not formula-free. Then, this part of \texttt{pat} can
be instantiated to \texttt{Structform A}, but not to an arbitrary
structure \texttt{Y} as desired. The condition that a structure
variable may not appear more than once in the conclusion of a rule is
one of Belnap's conditions \cite{belnap-display}.
% \subsection{Definition of the transformation}
%\label{s-mlp}
% As part of an attempt to implement some of the proofs of
% Wansing \cite{wansing-displaying-modal-logic}
% (discussed later, \S \ref{s-wsn}),
% we gave (partially) a functional definition of the transformation
% used to obtain the new derivation tree.
The stronger result \texttt{seqExSub2} is similar to \texttt{seqExSub1},
except that the antecedent [succedent] of the sequent
\texttt{pat} may contain a formula,
provided that the whole of the antecedent [succedent] is that formula.
The result \texttt{seqExSub2}
is used in proceeding up the derivation tree $\Pi_L[A]$,
changing $A$ to $Y$:
if \texttt{pat} is the conclusion of a rule, which, instantiated with
\texttt{(fs, suba)}, is used in $\Pi_L[A]$, then that rule, instantiated with
\texttt{(fs, suby)}, is used in $\Pi_L[Y]$.
This is expressed in the theorem \texttt{extSub2}, which is one step in the
transformation of $\Pi_L[A]$ to $\Pi_L[Y]$.
To explain theorem \texttt{extSub2} we define
%\texttt{bprops} of rules:
\texttt{bprops rule} to hold if the rule \texttt{rule}
satisfies the following three properties, which are related
(but do not exactly correspond) to Belnap's conditions (C3), (C4) and (C5):
% -- this is discussed further in \S\ref{Bel-props}.\footnote{No it is not!}
%The three properties are
\begin{itemize}
\item the conclusion of \texttt{rule} has no repeated structure variables
\item if a structure variable in the conclusion of \texttt{rule}
is also in a premise,
then it has the same ``cedency'' (ie antecedent or succedent) there
\item if the conclusion of \texttt{rule} has formulae,
they are displayed (as the whole of one side)
\end{itemize}
\begin{theorem}[\texttt{extSub2}]
\renewcommand\theenumi{\roman{enumi}}
\renewcommand\labelenumi{(\theenumi)}
Suppose we are given a rule \texttt{rule}
and an instantiation \texttt{ruleA} of it,
and given a sequent \texttt{conclY},
such that
% \begin{enumerate}
% \item \texttt{seqRep pn (Structform A) Y (conclRule ruleA) conclY} holds,
% \item \texttt{bprops rule} holds,
% \item \label{extc}
% if the conclusion of \texttt{rule}
% has a displayed formula on one side,
% then \texttt{conclrule ruleA} and \texttt{conclY} are the same on that side
% \end{enumerate}
(i) \texttt{seqRep pn (Structform A) Y (conclRule ruleA) conclY} holds;
(ii) \texttt{bprops rule} holds;
(iii) if the conclusion of \texttt{rule}
has a displayed formula on one side
then \texttt{conclrule ruleA} and \texttt{conclY} are the same on that side.
Then there exists \texttt{ruleY}, an instantiation of \texttt{rule},
whose conclusion is \texttt{conclY} and whose premises \texttt{premsY}
are, respectively, related to \texttt{premsRule ruleA} by
\texttt{seqRep pn (Structform A) Y}.
% \begin{verbatim}
% extSub2 =
% "[| conclRule rule = Sequent pant psuc ;
% conclRule ruleA = Sequent aant asuc ;
% conclY = Sequent yant ysuc ;
% (strIsFml pant & aant = Structform A --> aant = yant) ;
% (strIsFml psuc & asuc = Structform A --> asuc = ysuc) ;
% ruleMatches ruleA rule ; bprops rule ;
% seqRep pn (Structform A) Y (conclRule ruleA) conclY |]
% ==> (EX subY. conclRule (ruleSubst subY rule) = conclY &
% seqReps pn (Structform A) Y (premsRule ruleA)
% (premsRule (ruleSubst subY rule)))" : thm
%\end{verbatim}
\begin{verbatim}
extSub2 = "[| conclRule rule = Sequent pant psuc ;
conclRule ruleA = Sequent aant asuc ; conclY = Sequent yant ysuc ;
(strIsFml pant & aant = Structform A --> aant = yant) ;
(strIsFml psuc & asuc = Structform A --> asuc = ysuc) ;
ruleMatches ruleA rule ; bprops rule ;
seqRep pn (Structform A) Y (conclRule ruleA) conclY |]
==> (EX subY. conclRule (ruleSubst subY rule) = conclY &
seqReps pn (Structform A) Y (premsRule ruleA)
(premsRule (ruleSubst subY rule)))" : thm
\end{verbatim}
\end{theorem}
This theorem is used to show that, when a node of the tree $\Pi_L[A]$
is transformed to the corresponding node of $\Pi_L[Y]$,
then the next node(s) above can be so transformed.
But this does not hold at the node whose conclusion is
$X' \vdash A$ (see Fig.\ref{fig-cut-p-new});
condition (iii)
%\ref{extc})
above reflects this limitation.
\subsection{Turning One Cut Into Several Left-Principal Cuts}
\label{turn-cut-lps}
To turn one cut into several left-principal cuts
we use the procedure described above.
This uses \texttt{extSub2} to transform $\Pi_L[A]$ to $\Pi_L[Y]$
up to each point where $A$ is introduced, and then inserting an instance
of the (cut) rule.
% (or, in the case where $A$ is introduced by the axiom
% $A \vdash A$, using the $\Pi_R$ alone, as in Fig.\ref{fig-cut-p-new}).
It is to be understood that the derivation trees have no
(unfinished) premises.
\begin{theorem}[\texttt{makeCutLP}]
Given cut-free derivation tree \texttt{dtAY}
deriving (\texttt{A} $\vdash $ \texttt{Y})
and \texttt{dtA} deriving \texttt{seqA},
and given \texttt{seqY}, where
\texttt{seqRep True (Structform A) Y seqA seqY} holds
(ie, \texttt{seqY} and \texttt{seqA}
are the same except (possibly)
that $A$ in a succedent position in \texttt{seqA} is replaced by $Y$
in \texttt{seqY}),
there is a derivation tree deriving \texttt{seqY} whose
cuts are all left-principal on $A$.
% \begin{verbatim}
% makeCutLP =
% "[| allDT (cutOnFmls {}) ?dtAY; allDT (frb rls) ?dtAY;
% allDT wfb ?dtAY; conclDT ?dtAY = (?A |- $?Y);
% allDT (frb rls) ?dtA; allDT wfb ?dtA;
% allDT (cutOnFmls {}) ?dtA;
% seqRep True (Structform ?A) ?Y (conclDT ?dtA) ?seqY |]
% ==> EX dtY.
% conclDT dtY = ?seqY & allDT (cutIsLP ?A) dtY &
% allDT (frb rls) dtY & allDT wfb dtY" : thm
% \end{verbatim}
% %$
% \end{theorem}
\begin{verbatim}
makeCutLP = "[| allDT (cutOnFmls {}) ?dtAY; allDT (frb rls) ?dtAY;
allDT wfb ?dtAY; conclDT ?dtAY = (?A |- $?Y);
allDT (frb rls) ?dtA; allDT wfb ?dtA; allDT (cutOnFmls {}) ?dtA;
seqRep True (Structform ?A) ?Y (conclDT ?dtA) ?seqY |]
==> EX dtY. conclDT dtY = ?seqY & allDT (cutIsLP ?A) dtY &
allDT (frb rls) dtY & allDT wfb dtY" : thm
\end{verbatim}
%$
\end{theorem}
Function \texttt{makeCutRP} is basically the symmetric variant of
\texttt{makeCutLP} ; so \texttt{dtAY} is a cut-free derivation tree
deriving ($Y \vdash A$). But with the extra hypothesis that $A$ is
introduced at the bottom of \texttt{dtAY}, the result is that there is
a derivation tree deriving \texttt{seqY} whose cuts are all (left- and
right-) principal on $A$.
These were the most difficult to prove in this cut-elimination proof.
The proofs proceed by structural induction on the initial derivation
tree, where the inductive step involves an application of
\texttt{extSub2}, except where the formula $A$ is introduced. If $A$
is introduced by an introduction rule, then the inductive step
involves inserting an instance of (cut) into the tree, and then
applying the inductive hypothesis. If $A$ is introduced by the axiom
(\textit{id}), then (and this is the base case of the induction) the
tree \texttt{dtAY} is substituted for $A \vdash A$.
Next we have the theorem expressing the transformation of the whole
derivation tree, as shown in the diagrams.
\begin{theorem}[\texttt{allLP}] \label{thm-allLP}
Given a valid derivation tree \texttt{dt} containing just one cut,
which is on formula $A$ and
is at the root of \texttt{dt}, there is a valid tree with
the same conclusion (root) sequent,
all of whose cuts are left-principal and are on $A$.
\begin{verbatim}
allLP = "[| cutOnFmls {?A} ?dt; allDT wfb ?dt; allDT (frb rls) ?dt;
allNextDTs (cutOnFmls {}) ?dt |]
==> EX dtn. conclDT dtn = conclDT ?dt & allDT (cutIsLP ?A) dtn &
allDT (frb rls) dtn & allDT wfb dtn" : thm
\end{verbatim}
\end{theorem}
\texttt{allLRP} is a similar theorem where we start with a single
left-principal cut, and produce a tree whose cuts are
all (left- and right-) principal.
\subsection{Putting It All Together}
% \footnote{The focus of the paper
% should be this section. Perhaps we should give the code for these?}
\label{s-pat}%\cc{s-pat}
A monolithic proof of the cut-admissibility theorem would be very
complex, involving either several nested inductions or a complex
measure function. For the transformations
above replace one arbitrary cut by many left-principal cuts, one left-principal
cut by many principal cuts and one principal cut by one or two cuts on
subformulae, whereas we need, ultimately, to replace many arbitrary cuts in a
given derivation tree. We can manage this complexity by
considering how we would write a program to perform the elimination of
cuts from a derivation tree.
One way would be to use a number of mutually recursive routines, as follows:
\begin{description}
\item[\texttt{elim}] eliminates a single arbitrary cut,
by turning it into several left-principal cuts
% (\texttt{allLP} says this is possible)
and using \texttt{elimAllLP} to eliminate them \ldots
\item[\texttt{elimAllLP}] eliminates several left-principal cuts,
by repeatedly using \texttt{elimLP} to eliminate the top-most remaining one
\ldots
\item[\texttt{elimLP}] eliminates a left-principal cut,
by turning it into several principal cuts
% (\texttt{allLRP} says this is possible)
and using \texttt{elimAllLRP} to eliminate them \ldots
\item[\texttt{elimAllLRP}] eliminates several principal cuts,
by repeatedly using \texttt{elimLRP} to eliminate the top-most remaining one
\ldots
\item[\texttt{elimLRP}] eliminates a principal cut,
by turning it into several cuts on smaller cut-formulae,
and using \texttt{elimAll} to eliminate them \ldots
\item[\texttt{elimAll}] eliminates several arbitrary cuts,
by repeatedly using \texttt{elim} to eliminate the top-most remaining one
\ldots
\end{description}
Such a program would terminate because any call to \texttt{elim} would
(indirectly) call \texttt{elim} only on smaller cut-formulae.
We turn this program outline into a proof.
Each routine listed above, of the form
``routine $P$ does \ldots and uses routine $Q$''
will correspond to a theorem which will say essentially
``if routine $Q$ completes successfully then
routine $P$ completes successfully''
(assuming they are called with appropriately related arguments).
% We imitate this procedure by defining two predicates,
We define two predicates,
\texttt{canElim} and \texttt{canElimAll},
whose types and meanings (assuming valid trees) are given below.
When we use them, the argument \texttt{f} will be one of the
functions
%in
%Figure~\ref{fig:functions-reasoning-about-cuts-new}.
\texttt{cutOnFmls}, \texttt{cutIsLP} and \texttt{cutIsLRP}.
\begin{definition}
\texttt{canElim f} holds for property \texttt{f} if, for any valid
derivation tree \texttt{dt} satisfying \texttt{f} and containing at
most one cut at the bottom, there is a valid cut-free derivation
tree which is \emph{equivalent} to (has the same conclusion as)
\texttt{dt}.
\texttt{canElimAll f} means that if every subtree of a given valid
tree \texttt{dt} satisfies \texttt{f}, then there is a valid
cut-free derivation tree \texttt{dt'} equivalent to \texttt{dt} such
that if the bottom rule of \texttt{dt} is not (\textit{cut}), then
the same rule is at the bottom of \texttt{dt'}.
% from HOL_Elim.thy
\begin{verbatim}
canElim :: "(dertree => bool) => bool"
canElimAll :: "(dertree => bool) => bool"
"canElim ?f == (ALL dt. ?f dt & allNextDTs (cutOnFmls {}) dt &
allDT wfb dt & allDT (frb rls) dt -->
(EX dtn. allDT (cutOnFmls {}) dtn & allDT wfb dtn &
allDT (frb rls) dtn & conclDT dtn = conclDT dt))"
"canElimAll ?f ==
(ALL dt. allDT ?f dt & allDT wfb dt & allDT (frb rls) dt -->
(EX dt'. (botRule dt ~= cutr --> botRule dt' = botRule dt) &
conclDT dt' = conclDT dt & allDT (cutOnFmls {}) dt' &
allDT wfb dt' & allDT (frb rls) dt'))"
\end{verbatim}
\end{definition}
\comment{
\texttt{canElim f} means that if a valid derivation tree \texttt{dt}
has no cuts other than (possibly) one at the bottom, and satisfies
\texttt{f}, then there is an equivalent valid cut-free derivation
tree.
\texttt{canElimAll f} means that if every subtree of a given valid
tree \texttt{dt} satisfies \texttt{f}, then there is a valid cut-free
derivation tree \texttt{dt'} equivalent to \texttt{dt}: we also
include as part of this definition the requirement that if the bottom
rule of \texttt{dt} is not (\textit{cut}), then the bottom rule of
\texttt{dt'} is the same.
end of comment }
\comment{
\footnote{
RAJ - you suggest making the following lemmata.
I see your point, but wonder how it would look.
Firstly, there would be thirteen of them,
\texttt{allLP'} to \texttt{canElimAll}.
I assume one lemma with 13 parts would be best.
(or did you mean just \texttt{allLP'} and \texttt{allLRP'} ?)
Secondly, the present statements in English (at present for some only)
are rather informal, ``we can eliminate \ldots''.
If neither of these are a problem, then we could state the rest in
English similarly, and make the change, and
list all the Isabelle theorems below.
Alternatively, part of what I've written is of the flavour of a proof,
so some or all of it could be made part of the proof of the ultimate result,
except for the fact that it has Isabelle theorems interspersed in it.
}
end of comment }
We restate \texttt{allLP} and \texttt{allLRP}
%from Theorem~\ref{thm-allLP}
using \texttt{canElim} and \texttt{canElimAll}.
\begin{theorem}[\texttt{allLP'}, \texttt{allLRP'}]
\begin{enumerate}
\item If we can eliminate any number of left-principal cuts on $A$ from
a valid tree \dt,
then we can eliminate a single arbitrary cut on $A$ from the bottom of \dt.
\item If we can eliminate any number of principal cuts on $A$ from
a valid tree \dt,
then we can eliminate a single left-principal
cut on $A$ from the bottom of \dt.
\end{enumerate}
\end{theorem}
\comment{
\begin{proof} ~
\begin{enumerate}
\item The theorem \texttt{allLP} says
``we can turn a tree \dt\ which has one cut, which is at the bottom
and is on $A$,
into a tree with several cuts, which are all left-principal and are on $A$'',
which is equivalent to the theorem statement.
\item This has a corresponding proof. \qed
\end{enumerate}
\end{proof}
We can now turn the theorems
\texttt{allLP}
(``we can turn a tree with one cut, at the bottom, on $A$,
into a tree with several cuts, all left-principal on $A$'')
into \texttt{allLP'}
(``if we can eliminate several cuts, all left-principal on $A$,
then we can eliminate a single arbitrary cut, at the bottom, on $A$''),
and similarly \texttt{allLRP} into \texttt{allLRP'}:
end of comment }
\begin{verbatim}
allLP' = "canElimAll (cutIsLP ?A) ==> canElim (cutOnFmls {?A})":thm
allLRP' = "canElimAll (cutIsLRP ?A) ==> canElim (cutIsLP ?A)":thm
\end{verbatim}
Now if we can eliminate one arbitrary cut (or left-principal cut, or
principal cut) then we can eliminate any number, by eliminating them
one at a time starting from the top-most cut. This is easy because
eliminating a cut affects only the proof tree above the cut. (There
is just a slight complication: we need to show that eliminating a cut
does not change a lower cut from being principal to not principal, but
this is not difficult).
%
This gives the following three results:
\begin{theorem}\label{thm:three}
If we can eliminate one arbitrary cut
(or left-principal cut, or principal cut) from any given derivation tree,
then we can eliminate any number of such cuts
from any given derivation tree.
\end{theorem}
\begin{verbatim}
elimLRP= "canElim (cutIsLRP ?A) ==> canElimAll (cutIsLRP ?A)":thm
elimLP= "canElim (cutIsLP ?A) ==> canElimAll (cutIsLP ?A)":thm
elimFmls="canElim (cutOnFmls ?s) ==> canElimAll (cutOnFmls ?s)":thm
\end{verbatim}
\comment{
We also have two results which will be combined with \texttt{elimFmls}
\begin{verbatim}
twoElim = "[| canElim (cutOnFmls {?A}); canElim (cutOnFmls {?B}) |]
==> canElim (cutOnFmls {?B, ?A})" : thm
\end{verbatim}
(``if we can eliminate a cut (at the bottom) on $A$
and if we can eliminate one on $B$
then we can eliminate one which may be either on $B$ or $A$'').
\begin{verbatim}
trivElim = "canElim (cutOnFmls {})" : thm
\end{verbatim}
(``we can eliminate cuts (if any) from a tree which has no cuts'').
}
We also have the theorems such as \texttt{orC8} (see
\S\ref{subsec:princ-cuts-beln}) dealing with a tree with a single
(left- and right-) principal cut on a given formula.
\begin{theorem}
A tree with a single (left- and right-) principal cut on a given formula
can be replaced by a tree with arbitrary cuts
on the immediate subformulae (if any) of that formula.
\end{theorem}
These theorems (one for each constructor for the type \texttt{formula})
are converted to a list of theorems \texttt{thC8Es'},
of which an example is
\begin{verbatim}
"canElimAll (cutOnFmls {?B,?A}) ==> canElim (cutIsLRP (?Av?B))":thm
\end{verbatim}
We have one such theorem for each logical connective or constant, and
one for the special formulae \texttt{FV str} and \texttt{PP str}.
These latter two arise in the trivial instance of cut-elimination when
$Y$ is $A$ and $\Pi_{AY}$ is empty in Figure~\ref{fig-idcut-new}.
% \[
% \frac {A \vdash A \qquad A \vdash A} {A \vdash A} \textit{(cut)}
% \qquad \mbox{becomes} \qquad {A \vdash A}
% \]
\comment{
% \begin{figure}[t]
\vpf
\begin{center}
\bpf
\A "$A \vdash A$"
\A "$A \vdash A$"
\B [2em] "$A \vdash A$" "($cut$)"
\epf
\qquad becomes \qquad
\bpf
\A "$A \vdash A$"
\epf
\end{center}
% \caption{When the cut-formula is ...}
%\cc{fig-idcut}
% \label{fig-base-case}
% \end{figure}
}
Together with the theorems \texttt{elimLRP}, \texttt{allLRP'},
\texttt{elimLP}, \texttt{allLP'} and \texttt{elimFmls}, we now have
theorems corresponding to the six routines described above. As noted
already, a call to \texttt{elim} would indirectly call \texttt{elim}
with a smaller cut-formula as argument, and so the program would
terminate, the base case of the recursion being the trivial instance
of Figure~\ref{fig-idcut-new} mentioned above. Correspondingly, the
theorems we now have can be combined to give the following.
\begin{theorem} \label{thm-princ_subf}
We can eliminate a cut on a formula if we can eliminate a cut on
each of the formula's immediate subformulae.
\end{theorem}
\begin{verbatim}
"canElim (cutOnFmls {?B,?A}) ==> canElim (cutOnFmls {?A v ?B})":thm
\end{verbatim}
The proof of Theorem \ref{thm-princ_subf} is by cases on the formation
of the cut-formula, and here we have shown the case for $\lor$ only.
There is one such case for each constructor for the type
\texttt{formula}. We can therefore use structural induction on the
structure of a formula to prove that we can eliminate a cut on any
given formula \texttt{fml}: that is, we can eliminate any cut.
% "[| canElim (cutOnFmls {?A}); canElim (cutOnFmls {?B}) |]
% ==> canElim (cutOnFmls {?A v ?B})" : thm
% we get the list of theorems \texttt{thC8Es}, including
% \begin{verbatim}
% "canElimAll (cutOnFmls {?B, ?A}) ==> canElim (cutOnFmls {?A v ?B})" : thm
% \end{verbatim}
%
% We then combine these with the result \texttt{elimFmls} and
% (in the case of a binary logical connective) \texttt{twoElim} to get
% the list of theorems \texttt{elimFmlRecs}, including
% \begin{verbatim}
% "[| canElim (cutOnFmls {?A}); canElim (cutOnFmls {?B}) |]
% ==> canElim (cutOnFmls {?A v ?B})" : thm
% \end{verbatim}
% The theorems \texttt{elimFmlRecs} are then used in a proof by
% Of the two encodings of this last theorem,
% the second follows easily from the first.
%We can now use these theorems in
%A proof by
% Structural
% induction on the structure of a formula is now possible.
%
%We now have the ingredients for the main theorem.
\comment{
Such theorems are then used in a proof by structural induction on the
structure of a formula to prove that we can eliminate a cut (on any
formula), and then, using \texttt{elimFmls},
that we can eliminate any number of cuts,
which is the required cut-elimination result.
\begin{verbatim}
canElimFml = "canElim (cutOnFmls {?fml})" : thm
\end{verbatim}
(``we can eliminate one cut on any given formula \texttt{fml}''),
\begin{verbatim}
canElimAny = "canElim (cutOnFmls UNIV)" : thm
\end{verbatim}
(``we can eliminate one cut whatever the cut-formula''),
and, using \texttt{elimFmls},
\begin{verbatim}
canElimAll = "canElimAll (cutOnFmls UNIV)" : thm
\end{verbatim}
Finally we convert \texttt{canElimAll} into the cut-elimination theorem
\begin{verbatim}
cutElim = "IsDerivableR rls {} ?concl ==>
IsDerivableR (rls - {cut}) {} ?concl" : thm
\end{verbatim}
}
\begin{theorem}
A sequent derivable using \textit{(cut)} is derivable without using
\textit{(cut)}.
\end{theorem}
\begin{proof}
Using \texttt{elimFmls} from
Theorem~\ref{thm:three}, it follows that we can eliminate any number
of cuts, as reflected by the following sequence of theorems.
\begin{verbatim}
canElimFml = "canElim (cutOnFmls {?fml})" : thm
canElimAny = "canElim (cutOnFmls UNIV)" : thm
canElimAll = "canElimAll (cutOnFmls UNIV)" : thm
cutElim = "IsDerivableR rls {} ?concl ==>
IsDerivableR (rls - {cut}) {} ?concl" : thm
\end{verbatim}
\end{proof}
\begin{corollary}
The rule (cut) is admissible in \dRA.
\end{corollary}
\comment{
\subsection{Use of properties of the Display Calculus}
\label{Bel-props}
Belnap's cut-elimination theorem states that any Display Calculus
satisfying his properties (C2) to (C8) satisfies the cut-elimination theorem.
Here we trace the use of these properties in the proof for the
specific case of \dRA.
We refer to the conditions in the form given by Kracht \cite{kracht-power}.
We proved properties which are satisfied by each rule of \dRA.
They use the following definitions:
\texttt{rls} is the set of rules of \dRA.
\texttt{ruleInOrInv} \texttt{rule rules} :
either \texttt{rule} or its inverse is a member of \texttt{rules}
\texttt{seqNoSSF} \texttt{seq} :
if a formula appears on one side of the $\vdash$ in
\texttt{seq} then the whole of that side is a formula.
\texttt{seqSVs} \texttt{seq} : a list of the structure variables in
\texttt{seq}.
\texttt{noDups} \texttt{list} :
\texttt{list} contains no member more than once.
\texttt{seqSVs'} \texttt{bool seq} : a list of the structure variables in
antecedent or succedent (depending on \texttt{bool}) positions in
\texttt{seq}.
The following three results are used in the proofs of
\texttt{makeCutLP} and \texttt{makeCutRP}.
In the conclusion of a rule, no structure has a sub-structure which is a
formula
\begin{verbatim}
seqNoSSF_rls =
"ruleInOrInv ?rule rls ==> seqNoSSF (conclRule ?rule)" : thm
\end{verbatim}
No structure variable appears more than once in the conclusion of a rule.
\begin{verbatim}
noDupSVs_rls =
"ruleInOrInv ?rule rls ==> noDups (seqSVs (conclRule ?rule))" : thm
\end{verbatim}
If a structure variable appears in the conclusion of a rule
in antecedent [succedent] position,
then it does not appear in a premise of that rule
in succedent [antecedent] position.
\begin{verbatim}
noSVsAS_rls =
"[| ruleInOrInv ?rule rls; ?prem : set (premsRule ?rule);
?s : set (seqSVs' ?b (conclRule ?rule)) |]
==> ?s ~: set (seqSVs' (~ ?b) ?prem)"
\end{verbatim}
\comment{
Note that an earlier version of our work used the following rule,
which is actually stronger than required, but makes the proof simpler.
If a structure variable appears in a premise of a rule,
in antecedent [succedent] position,
then it also appears in the conclusion of that rule
in antecedent [succedent] position.
\begin{verbatim}
noNewSVs_rls =
"[| ruleInOrInv ?rule rls; ?prem : set (premsRule ?rule);
?s : set (seqSVs' ?b ?prem) |]
==> ?s : set (seqSVs' ?b (conclRule ?rule))"
\end{verbatim}
}
The result \texttt{orC8}, and the corresponding results for each logical
connective, form Belnap's condition (C8).
Belnap's condition (C3) is equivalent to \texttt{noDupSVs\_rls}.
His condition (C4) says that if a
structure variable appears anywhere in a rule in an
antecedent (succedent) position, then it does not appear in a
succedent (antecedent) position.
In fact all we actually need for the proof is \texttt{noSVsAS\_rls},
which is weaker than (C4), since
\texttt{noSVsAS\_rls} permits a structure variable to appear
in both antecedent and succedent positions in the premises,
provided that it does not appear in the conclusion.
\comment{
(C4) is implied by \texttt{noDupSVs\_rls} and \texttt{noNewSVs\_rls}
(which we had used originally).
However \texttt{noNewSVs\_rls} is stronger than it needs to be for this
result, since (C4) permits structure variables to appear in the
premise(s) but not in the conclusion.
Note that Display Calculi generally do satisfy \texttt{noNewSVs\_rls}.
}
Our theorem \texttt{seqNoSSF\_rls} is equivalent to Belnap's (C5),
since, in Kracht's formulation, formula variables can never be parameters.
Under Kracht's formulation, Belnap's (C2), (C6) and (C7) are trivially
satisfied.
end of comment }
\section{Conclusion and Further Work}
\label{sec:concl-furth-work}
We have formulated the Display Calculus for Relation Algebra, \dRA, in
Isabelle/HOL as a ``deep embedding'', allowing us to model and reason
about derivations rather than just performing derivations (as in a
shallow embedding). We have proved, from the definitions,
``transitivity'' results about the composition of proofs. These are
results which were omitted -- ``due to their difficulty'' -- from
another reported mechanised formalisation of provability
\cite[p.~302]{mikhajlova-vonwright-isomorphism}.
We have proved Belnap's cut-admissibility theorem for \dRA. This was a
considerable effort, and could not have been achieved without the
complementary features (found in Isabelle) of the extensive provision
of powerful tactics, and the powerful programming language interface
available to the user.
The most important disadvantage of our approach is the inability to easily
produce a program for cut-elimination from our Isabelle/HOL proofs,
even when our proofs mimic a programming style (see \S\ref{s-pat}).
% We now discuss possible further work to address this issue.
% In \cite{dawson-gore-embedding-comparing} we described a shallow
% embedding of \dRA\ into Isabelle/Pure. We also described an
% implementation of \dRA\ in Twelf, which had the feature that deriving
% a sequent produced a term containing the derivation tree for that
% sequent. If we think of that Twelf implementation as a ``shallow
% embedding'', we may then ask whether a ``deep embedding'' in Twelf,
% and a similar proof of cut-elimination using it, would produce a term
% representing that proof. That term might then provide a function to
% perform cut-elimination. Note, however, that proof by structural
% induction on the types \verb|dertree| and \verb|formula| (types defined
% using Isabelle/HOL's \verb|datatype| facility) were crucial. To
% perform the proof in another system we would still need to reproduce
% these types.
% In fact, in further work on strong normalisation
% \cite{dawson-gore-machine-checked-strong-normalisation-lics} we needed
% to describe (in Isabelle/HOL) a function to perform the transformation
% shown in Figure~\ref{fig-cut-p-new}. Doing so was more complicated
% than proving the corresponding existence theorems of
% \S~\ref{make-cut-lp} and \S~\ref{turn-cut-lps}. Even so, the
% definition of the function was not completely implementable as it used
% the Isabelle/HOL \texttt{Eps} operator to choose an arbitrary one of
% several substitutions having the same effect on a particular sequent.
Results like \verb|IsDerivableR_trans| and \verb|IsDerivableR_deriv|
are general results about the structure of derivations, closely
resembling facilities available in Isabelle: namely, successive
refinement of subgoals, and use of a previously proved lemma. A
higher order framework allows us to reason about higher and higher
meta-levels, like the \verb|IsDerivable| relation itself, without
invoking explicit ``reflection principles''
\cite{harrison-metatheory-reflection}.
%Mechanising such meta-theoretic reasoning
This is the topic of future work.
\comment{
Belnap's theorem is expressed to apply to any Display Calculus
satisfying his conditions. To prove his theorem in that form would
require modelling an arbitrary Display Calculus, with generalised
rules for arbitrary sets of structural and logical connectives. A
theoretical framework for such generalised rules can be found in
\cite{gore-sld-igpl}. In a sense, this would require a ``deeper''
embedding still. For, in our first implementation
\cite{dawson-gore-dra-jelia98}, we set up the specific connectives and
rules of \dRA\ in Isabelle, and used Isabelle proofs as the
\dRA-derivations. In the present implementation, we again set up the
specific connectives and rules of \dRA, although we set up data
structures to model arbitrary derivations. To prove the generic Belnap
theorem, we need to set up the necessary structures to model arbitrary
sets of connectives and rules.
end of comment }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter
\begin{thebibliography}{10}
\bibitem{belnap-display}
N~D {Belnap}.
\newblock Display logic.
\newblock {\em Journal of Philosophical Logic}, 11:375--417, 1982.
\bibitem{dawson-gore-embedding-comparing}
Jeremy~E Dawson and R~Gor{\'e}.
\newblock Embedding display calculi into logical frameworks: Comparing {T}welf
and {I}sabelle.
\newblock In C~Fidge (Ed), {\em Proc.\ CATS 2001: The Australian Theory
Symposium}, ENTCS, 42: 89--103, 2001, Elsevier.
\bibitem{dawson-gore-machine-checked-strong-normalisation-lics}
J~E. Dawson and R~Gore.
\newblock A new machine-checked proof of strong normalisation for display
logic. Submitted 2001.
\bibitem{gore-relalg}
R~Gor{\'{e}}.
\newblock Cut-free display calculi for relation algebras.
\newblock In D~van Dalen and M~Bezem (Eds), {\em CSL96: Selected Papers of
the Annual Conference of the European Association for Computer Science
Logic}, LNCS 1258:198--210. Springer, 1997.
\bibitem{gore-sld-igpl}
R~Gor{\'{e}}.
\newblock Substructural logics on display.
\newblock {\em Logic Journal of the Interest Group in Pure and Applied Logic},
6(3):451--504, 1998.
\bibitem{harrison-metatheory-reflection}
J~Harrison.
\newblock Metatheory and reflection in theorem proving: A survey and critique.
\newblock Technical Report CRC-053, SRI International Cambridge Computer
Science Research Centre, 1995.
\bibitem{matthews-implementing-isabelle}
S~Matthews.
\newblock Implementing {FS$_0$} in {Isabelle}: adding structure at the
metalevel.
\newblock In J~Calmet and C~Limongelli, editors, {\em Proc.\ Disco'96}.
Springer, 1996.
\bibitem{mikhajlova-vonwright-isomorphism}
A~Mikhajlova and J~von Wright.
\newblock Proving isomorphism of first-order proof systems in {HOL}.
\newblock In J~Grundy and M~Newey, editors, {\em Theorem Proving in
Higher-Order Logics}, LNCS 1479:295--314. Springer, 1998.
\bibitem{pfenning-structural-lics94}
F~Pfenning.
\newblock Structural cut elimination.
\newblock In {\em Proc.\ LICS 94}, 1994.
\bibitem{schuermann-phd}
C~Sch{\"u}rmann.
\newblock {\em Automating the Meta Theory of Deductive Systems}.
\newblock PhD thesis, Dept.\ of Comp.\ Sci.\ , Carnegie Mellon
University, USA, CMU-CS-00-146, 2000.
% \bibitem{szabo-gentzen}
% M.~E. Szabo, editor.
% \newblock {\em The collected papers of Gerhard Gentzen}, pages 68--131.
% \newblock North-Holland, Amsterdam, 1969.
\bibitem{wansing-displaying-modal-logic}
H~Wansing.
\newblock {\em Displaying Modal Logic}, volume~3 of {\em Trends in Logic}.
\newblock Kluwer Academic Publishers, Dordrecht, August 1998.
\end{thebibliography}
%\bibliography{../ce,/home/discus/disk1/rpg/bib/fm,/home/discus/disk1/rpg/bib/modal,/home/discus/disk1/rpg/bib/mtl,/home/discus/disk1/rpg/bib/logic,/home/discus/disk1/rpg/bib/tl,/home/discus/disk1/rpg/bib/paracon,/home/discus/disk1/rpg/bib/linear,/home/discus/disk1/rpg/bib/algebra,/home/discus/disk1/rpg/bib/relevant,/home/discus/disk1/rpg/bib/dl,/home/discus/disk1/rpg/bib/atp}
%\bibliographystyle{plain}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: