\cc{
TODO avoid primes in theorem (etc) names

\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' commas 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.

Due to their generality, display calculi provide an extremely elegant
sequent framework, applicable to many (classical and non-classical)
logics in a uniform way
\cite{wansing-displaying-modal-logic,gore-sld-igpl}. The most
remarkable property of display calculi is that they enjoy a generic
cut-elimination theorem, which applies whenever the rules for the
display calculus satisfy certain, easily checked, conditions
\cite{belnap-display}.

In \cite{belnap-display}, Nuel Belnap gives a proof that the cut rule
is \textit{admissible} in 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. 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 la Gentzen \cite{szabo-gentzen}.
For this reason, Belnap's proof has been criticised 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 for relation
algebra \dRA\ \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 generalizes 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. Here, we describe how we proved both the
admissibility of cut and the strong normalisation result for \dRA.

The paper is set out as follows.

\paragraph{\textsc{Acknowledgements:}}

\subsection{Relation Algebras and \dRA}

Relation algebras \cite{maddux-introductory}
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).
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 where the
elements of the top line are Boolean and the elements of the bottom
line are their relational analogues:
\begin{eqnarray*}
   A \ B & ::= &
           p_i 
           \mid \btop 
           \mid \bbot
           \mid \bnot A 
           \mid A \band B 
           \mid A \bor B 
           \mid A \bimp B 
\\
       &     &
           \mid \mtop
           \mid \mbot
           \mid \mnot A
           \mid \conv A 
           \mid A \mor B 
           \mid A \mand B 
           \mid A \mimp B 
\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, using the grammar below:
\[
   X Y ::= \varphi \mid I \mid E \mid \ast X \mid \blob X \mid X \semic Y 
           \mid X \comma Y 
\]
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 introduction
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 )$, shown below left,
is typical of Gentzen's sequent calculi like \textbf{LK}, while the rule
$(\mbox{\dRA-}\vdash \lor )$ shown on the right 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 )
$$
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 \texttt{HOL}.

\texttt{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 \texttt{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.

}

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