%% %% \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: