%%
\documentclass{paper}
% \documentclass[a4paper,11pt]{article}
%\documentclass[twocolumn,a4paper,11pt]{article}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
%\usepackage{exptrees}
\usepackage{url}
\usepackage{bussproofs}
\usepackage{listings}
\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}
\setcounter{secnumdepth}2
\setcounter{tocdepth}2
% \newtheorem{theorem}{Theorem}[section]
\newcommand{\qed}{\hfill$\dashv$}
\newenvironment{proof}{
\noindent{\bf Proof:}}{\mbox{\bf Q.E.D.}\vspace{1ex}}
\newtheorem{definition}{Definition}[section]
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}{Lemma}[section]
\newtheorem{corollary}{Corollary}[section]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble
\newcommand\derl{\texttt{derl}}
\newcommand\derrec{\texttt{derrec}}
\newcommand\rls{\texttt{rls}}
\newcommand\adm{\texttt{adm}}
\newcommand{\pscrel}{\mathtt{rli}}
\newcommand{\dersrec}{\mathtt{dersrec}}
\newcommand{\prems}{\mathtt{pms}}
\newcommand{\hash}{\texttt{\#}}
\newcommand{\bra}{\texttt{\{}}
\newcommand{\ket}{\texttt{\}}}
\newcommand\cfile{}
\newcommand\comment[1]{}
\newcommand\cc[1]{#1} % for label names
\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\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
\newcommand\seesrc[1]{(see source file \texttt{#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\MC{\ensuremath{\mathcal C}}
\newcommand\MD{\ensuremath{\mathcal D}}
\newcommand\MP{\ensuremath{\mathcal P}}
\newcommand\MQ{\ensuremath{\mathcal Q}}
\newcommand\MR{\ensuremath{\mathcal R}}
\newcommand\MS{\ensuremath{\mathcal S}}
\newcommand\M{\ensuremath{\mathcal M}}
\newcommand\Mp{$\mathcal M'$}
\newcommand\psl{\ensuremath\MQ_{l1} \ldots \MQ_{ln}}
\newcommand\psr{\ensuremath\MQ_{r1} \ldots \MQ_{rm}}
\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}}
\newcommand\GL{\textbf{GL}}
\newcommand\GLS{\textrm{GLS}}
\newcommand\GLR{\textit{GLR}}
\newcommand\GLRp{\ensuremath{\Box X, X, \Box B \vdash B}} % premise of GLR
\newcommand\GLRc{\ensuremath{\Box X \vdash \Box B}} % conclusion of GLR
\newcommand\lxxc{\ensuremath{\Box X, X \vdash B}} % conclusion of lem20
\newcommand\gbna{\ensuremath{\Box G, \Box B^k \vdash \Box A}}
\newcommand\GLRB{\textit{GLR}($B$)}
\newcommand\GLRXB{\textit{GLR}($X,B$)}
\newcommand\pmz{\texttt{pm0}}
\newcommand\pmgez{\texttt{pm\_ge0}}
\newcommand\delz{\texttt{del0}}
\newcommand\delzs{\ensuremath{\partial^0}}
\newcommand\muxbn{\texttt{muxbn}}
\newcommand\lgp{\mathrm{S4C}}
\newcommand\wbx{\Box}
\newcommand\wdi{\lozenge}
\newcommand\nxt{\bigcirc}
\newcommand\limp{\rightarrow}
\newcommand\leqv{\leftrightarrow}
\newcommand{\Boxes}{\ensuremath{\vec{\Phi}}}
\newcommand{\Boxesi}[1]{\ensuremath{\vec{\Phi}_{-#1}}}
\newcommand{\cute}{cut-elimination}
\newcommand{\cuta}{cut-admissibility}
\newcommand{\ctra}{contraction-admissibility}
\newcommand{\weaka}{weakening-admissibility}
\newcommand{\ds}{\displaystyle\strut}
\newcommand{\idrule}[2]{
\mbox{#1 \ $\ds$ #2}
}
\newcommand{\urule}[4]{
\AxiomC{#2}
\LeftLabel{#1}
\RightLabel{#4}
\UnaryInfC{#3}
\DisplayProof
}
\newcommand{\brule}[4]{
\AxiomC{#2}
\AxiomC{#3}
\LeftLabel{#1}
\BinaryInfC{#4}
\DisplayProof
}
\hyphenation{
non-classical
conn-ection
typi-cally
tradi-tional
frame-works
con-clusion
deriv-ation
}
\pagestyle{plain}
\begin{document}
\title{Machine-checked Proof-Theory for Propositional Modal Logics}
\author{
Jeremy E.\ Dawson,\thanks{Supported by Australian Research Council
Grant DP120101244.}
Rajeev Gor\'e and
Jesse Wu
\\
Logic and Computation Group,
School of Computer Science
\\ The Australian National University,
Canberra ACT 0200, Australia
}
\date{}
%% Title
\maketitle
\begin{abstract}
We describe how we machine-checked the admissibility of the standard
structural rules of weakening, contraction and cut for
multiset-based sequent calculi for the unimodal logics K4D, S4 and
S4.3 as well as for the bimodal logic $\lgp$ recently investigated
by Mints. Our proofs for both S4 and S4.3 appear to be new while our
proof for $\lgp$ is different from that originally presented by Mints.
\end{abstract}
%% Here begins the main text
\section{Introduction} \label{s-intro}
Sequent calculi provide a rigorous basis for meta-theoretic studies of
various logics. The central theorem is cut-elimination/admissibility,
which states that detours through lemmata can be avoided, since it can
help to show many important logical properties like consistency,
interpolation, and Beth definability. Cut-free sequent calculi are
also used for automated deduction, for nonclassical extensions of
logic programming, and for studying the connection between normalising
lambda calculi and functional programming. Sequent calculi, and their
extensions, therefore play an important role in logic and computation.
Meta-theoretic reasoning about sequent calculi is error-prone because
it involves checking many combinatorial cases,
with some being very difficult, but many being very
similar. Invariably, authors resort to expressions like ``the other
cases are similar'', or ``we omit details''. The literature contains
many examples of meta-theoretic proofs containing serious and subtle
errors in the original pencil-and-paper proofs. For example, the
cut-elimination theorem for the modal ``provability logic'' \GL{},
where $\Box \varphi$ can be read as ``$\varphi$ is provable in Peano
Arithmetic'', has a long and chequered history which has only recently
been resolved~\cite{gr-valentini}.
Here, we describe how we formalised cut-elimination for traditional,
propositional, multiset-based sequent calculi without explicit
structural rules for the modal logics KD, S4, S4.3 and $\lgp$ using
\marginpar{KD here, K4D in abstract, K4De in \S3 ?}
the interactive proof-assistant Isabelle/HOL. As far as we know, the
proofs for S4 and S4.3 are new, and avoid the complexities of previous
proofs for these logics. Our results also confirm the recent proof of
cut-elimination for $\lgp$ due to Mints, although our proof is different.
In Section~\ref{sec:preliminaries}, we briefly describe traditional
sequent calculi, discuss the need for multisets, and describe ???
In Section~\ref{s-deriv} we describe techniques and functions we have
defined for reasoning about derivations, and show how we formalise
formulae, sequents and rules, showing some of the sequent rules
as examples.
%
In Section~\ref{s-caglr} we describe the cut-admissibility proof for
???.
We assume the reader is familiar with basic
proof-theory, ML and Isabelle/HOL.
%
Our Isabelle code can be found at
\url{http://users.rsise.anu.edu.au/~jeremy/isabelle/2005/seqms/}.
Some of this work was reported informally in \cite{gore-india}.
%TO DO - include explanation of Isabelle notation
\section{Sequents Built From Multisets Verssus Sets}
\label{sec:preliminaries}
Proof-theorists typically work with sequents $\Gamma
\vdash \Delta$ where $\Gamma$ and $\Delta$ are ``collections'' of
formulae. The ``collections'' found in the literature increase in
complexity from simple sets for classical logic, to multisets for
linear logic, to ordered lists for substructural logics, to complex
tree structures for display logics.
%
A sequent rule typically has a rule name, a (finite) number of premises,
a side-condition and a conclusion.
% \begin{prooftree}
% \AxiomC{$\Gamma_1 \vdash \Delta_1
% \qquad\cdots\qquad
% \Gamma_n \vdash \Delta_n$}
% \LeftLabel{RuleName}
% \RightLabel{Condition}
% \UnaryInfC{$\Gamma_0 \vdash \Delta_0$}
% \end{prooftree}
Rules are read top-down as ``if all the premises hold then the
conclusion holds''. A derivation of the judgement $\Gamma \vdash
\Delta$ is typically a finite tree of judgements with root $\Gamma
\vdash \Delta$ where parents are obtained from children by ``applying
a rule''. We use ``derivation'' to refer to a
proof \emph{within} a calculus, reserving ``proof'' for a
meta-theoretic proof of a theorem \emph{about} the calculus.
Sequent calculi typically contain three structural rules called
weakening, contraction and cut. These rules are bad for automated
reasoning using backward proof-search since they can be applied at any
time. Thus for backward proof-search, we are interested in sequent
calculi which do not contain explicit rules for weakening, contraction
and cut. The traditional way to design such calculi is to assume that
sequents are built out of multisets, omit these rules from the
calculus itself, and prove that each of these rules is
admissible. That is, for each rule, we have to prove that the
conclusion sequent is derivable if each of its premises are derivable.
For example, our formalisation does not
regard the cut rules shown below as being part of the
system:
\[
\AxiomC{$\Gamma \vdash A, \Delta$}
\AxiomC{$\Gamma, A \vdash \Delta$}
\LeftLabel{(cut)}
\BinaryInfC{$\Gamma \vdash \Delta$}
\DisplayProof
\qquad
\AxiomC{$\Gamma_1 \vdash A, \Delta_1$}
\AxiomC{$\Gamma_2, A \vdash \Delta_2$}
\LeftLabel{(cut)}
\BinaryInfC{$\Gamma_1, \Gamma_2 \vdash \Delta_1, \Delta_2$}
\DisplayProof
\]
Thus our results will be lemmata of the form:
if $\Gamma \vdash A, \Delta$ is (cut-free) derivable
and $\Gamma, A \vdash \Delta$ is (cut-free) derivable
then $\Gamma \vdash \Delta$ is (cut-free) derivable.
\section{Basic Modal Logics}
\label{s-modal}
The sequent calculi we study are designed to reason about the
meta-theory of the basic modal logics S4, S4.3, K4De (called GTD by
Mints) and $\lgp$. Semantically, the first three are mono-modal logics
characterised by Kripke frames having reflexive and transitive;
reflexive, transitive and linear frames; and transitive and dense
frames respectively. The logic $\lgp$, called dynamic topological
logic, is a bimodal logic where $\wbx$ is captured by a reflexive and
transitive binary relation $R_\wbx$ and where $\nxt$ is captured by a
\marginpar{why $\bigcirc$ not $\circ$?}
serial and discrete linear relation $R_\nxt$ with an interaction of
``confluency'':
\begin{eqnarray}
\label{eq:1}
\forall x \forall y \forall z \exists u.
R_\wbx(x,y) \;\&\; R_\nxt(x, z) \Rightarrow R_\nxt(y,u) \;\&\;
R_\wbx(z, u)
\end{eqnarray}
The Hilbert-calculi for these logics are obtained by extending a
traditional Hilbert-calculus for classical propositional logic with
the following axioms and inference rules using the naming conventions
given in the rightmost column:
\begin{tabular}[c]{lllll}
Axiom/Rule Name & Schema & Logic & Axioms & Rules
\\
K
& $\wbx (\varphi\limp\psi) \limp (\wbx\varphi \limp \wbx\psi)$
& S4 & K,4,T & RN$\wbx$
\\
De
& $\wbx\wbx\varphi \limp \wbx\varphi $
& S4.3 & K,4,T,.3 & RN$\wbx$
\\
T
& $\wbx\varphi \limp \varphi $
& K4De & K,4,De & RN$\wbx$
\\
4
& $\wbx\varphi \limp \wbx\wbx\varphi $
\\
.3
& $\wbx (\wbx\varphi\limp\psi) \lor (\wbx\varphi \limp \psi)$
& &
\\
RN$\wbx$
& $\varphi$/$\wbx\varphi$
\end{tabular}
The logic $\lgp$ is obtained from S4 by adding the following axioms
and rule:
\begin{tabular}[c]{ll}
Axiom/Rule Name & Schema
\\
K$_\nxt$
& $\nxt (\varphi\limp\psi) \leqv (\nxt\varphi \limp \nxt\psi)$
\\
$\nxt\bot$
& $\nxt \bot \leqv \bot$
\\
C
& $\nxt\wbx\varphi \limp \wbx\nxt\varphi$
\\
RN$\nxt$
& $\varphi$/$\nxt\varphi$
\end{tabular}
The modal logic $\lgp$ is designed to capture the basic logic for
hybrid systems where equation~(\ref{eq:1}) captures the continuity of
the linear discrete relation with respect to the topological
interpretation of the $\wbx$-connective.
\section{Interactive Proof Assistants}
Interactive proof-assistants are now a mature technology for
``formalising mathematics''. They come in many different flavours as
indicated by the names of some of the most popular ones
{\tt Mizar, HOL, Coq, LEGO, NuPrl, NqThm, Isabelle,
$\lambda$-Prolog, HOL-Lite, LF, ELF, Twelf} $\cdots$
with apologies to those whose favourite proof-assistant I have
omitted.
Most of the modern proof-assistants are implemented using a modern
functional programming language such as ML, which was specifically
designed for the implementation of, and interaction with, such proof-assistants.
The lowest levels typically implement a typed lambda-calculus with
hooks provided to allow the encoding of further logical notions such as
equality of terms on top of this base implementation. The base
implementation is usually very small, comprising of a few hundred
lines of code, so that this code can be scrutinised by experts to
ensure its correctness.
Almost all aspects of proof-checking eventually compile down to a
type-checking problem using this small core, so that trust rests on
strong typing and a well-scrutinised small core of (ML) code.
Most proof-assistants also allow the user to create a proof-transcript
which can be cross-checked using other proof-assistants to guarantee
correctness.
\begin{figure}[t]
\centering
\begin{tabular}[c]{lr}
$[ \beta_1 \ ; \ \beta_2 \ ; \ \cdots \ ; \ \beta_n ] \Longrightarrow \alpha$
& $\beta$
\\[2em]
$\theta = match(\beta, \alpha)$
& $\beta_1\theta \ ; \ \beta_2\theta \ ; \ \cdots
\ ; \ \beta_n\theta$
\end{tabular}
\label{fig:backward-chaining}
\caption{Backward Chaining in Logical Frameworks}
\end{figure}
Figure~\ref{fig:backward-chaining} shows how these logical
frameworks typically work. Thus given some goal $\beta$ and an
inference step which claims that $\alpha$ is implied by $\beta_1$ up
to $\beta_n$, we pattern-match $\alpha$ and $\beta$ to find their most
general unifier $\theta$, and then reduce the original goal $\beta$ to
the $n$ subgoals $\beta_1\theta \cdots \beta_n\theta$.
The pattern matching required is usually (associative-commutative)
\marginpar{?? what does associative-commutative mean here?}
higher order unification.
The important point is that the logical framework keeps track of
sub-goals and the current proof state.
The syntax of the ``basic propositions'' such as $\alpha$, $\beta$ is
defined via an ``object logic'', which is a parameter. Different
``object logics'' can be invoked using the same logical-framework for
the task at hand.
The logical properties of ``$;$'' such as associativity or commutativity,
and properties of the ``$\Longrightarrow$'' such as classicality or
linearity are determined by the ``meta-logic'', which is usually fixed
for the logical framework in question.
For example, the meta-logic of Isabelle is higher-order intuitionistic
logic. Higher order simply means that functions can accept other
functions as arguments and can produce functions as results.
\section{A Deeper Embedding: Change Object Logic} \label{s-eol}
Recall that the meta-logic provides us with a method for backward
chaining via expressions of the form:
$$\beta_1 \ ; \cdots \ ; \ \beta_n \Longrightarrow \alpha$$
The usual method for obtaining the power for reasoning about sequent
derivations is to use the full power of higher-order classical logic
(HOL) to build the basic propositions $\beta_i$.
Isabelle's incarnation of HOL provides the usual connectives of logic
such as conjunction, disjunction, implication, negation and the higher
order quantifiers. But it also provides many powerful facilities
allowing us to define new types, define functions which accept and
return other functions as arguments, and even define infinite sets
using inductive definitions.
For example, the following HOL expressions capture the usual inductive
definition of the natural numbers by encoding the facts that ``zero is
a natural number, and if $n$ is a natural number then so is its
successor $s(n)$'':
\begin{center}
\begin{tabular}[c]{l}
$\mathtt{0 \in nat}$
\\
$\mathtt{n \in nat \Longrightarrow s(n) \in nat}$
\end{tabular}
\end{center}
Most proof-assistants will automatically generate an induction
principle from a given inductive definition. For example, Isabelle
will automatically generate the usual induction principle which states
that we can prove a property $P$ holds of all natural numbers if we
can show that $P(0)$ holds and we can show that $P(n)$ implies
$P(s(n))$. An implicit assumption which facilitates such induction
principles is that the inductive definitions are the only way to
construct its members. Thus, if $n$ is a natural number, then it is
either $0$, or is of the form $s(m)$ for some natural number $m$.
\begin{samepage}
To encode sequent calculus into HOL we first encode the grammar for
recognising formulae as below:
\begin{verbatim}
datatype fml = FC string (fml list) (* fml connective *)
| FV string (* fml variable *)
| PP string (* prim prop *)
\end{verbatim}
\end{samepage}
There are three type constructors \verb!FC!, \verb!FV! and \verb!PP!
which encode formula connectives, formula variables, and atomic
formulae (primitive propositions). Each of them takes one string
argument which is simply the string we want to use for that
construction. The formula connective constructor also accepts a list
of formulae, which constitute its subformulae.
For example, \verb!FC "&&" [FV "A", PP "q"]! encodes $A\; \land \; q$
where we use \verb!&&! as the symbol for conjunction.
Since we want to encode modal logics, we require only
the classical connectives, plus two unary modalities
\verb!FC "Box" [.]! for $\wbx .$ and \verb!FC "Dia" [.]! for
$\wdi .$ and \verb!FC "Circ" [.]! for $\nxt$.
Isabelle's HOL allows us to form sets and multisets of objects of an
arbitrary type, so the HOL expressions \verb!fml set! and
\verb!fml multiset! capture the types of formula sets and formula
multisets.
Using these types we can build a sequent type using an infix constructor
\begin{verbatim}
datatype 'a sequent = Sequent "'a multiset" "'a multiset"
\end{verbatim}
An alternative notation for the constructor \texttt{Sequent} is
$\vdash$ or \texttt{|-} (used infix).
We define the rule type by the type definitions
\begin{verbatim}
'a psc = "'a list * 'a" (* single step inference *)
'a rule = 'a sequent psc
\end{verbatim}
so a rule is a pair of a list of sequents (the premises) and a single sequent
(the conclusion).
Note that in common parlance we may say that (eg)
$A \Rightarrow B \Rightarrow A \land B$ is a ``rule'',
in the usage of our Isabelle implementation we would call ths a pattern
which can be instantiated to give infinitely many rules.
So all our rule sets are in fact the sets of instances of a finite number
of ``rule patterns''.
% Isabelle's HOL allows us to form lists of objects of an arbitrary
% but fixed type, so we define the type of a rule as a pair with the
% first component being a list of sequent premises and the second
% component being the conclusion sequent:
% $$\mathtt{datatype ~inf ~=~ (seq ~list ~,~ seq)}$$
Thus, we can use the HOL type declaration $\mathtt{\pscrel ~::~rule~set}$ to
declare that $\pscrel$ is a set of inferences, each a pair of the form
$(seq\ list , seq)$, and inductively define the set
$\pscrel$ by giving a finite collection of rule instances which belong
to this set. For example, the traditional rule $(\vdash\land)$ for
introducing a conjunction into the right hand side of a
sequent, as shown below, is given by the encoding below it where we
use the string \verb|&&| to encode $\land$:
$$
\brule{$(\vdash\land)$}
{$\Gamma \vdash A, \Delta$}
{$\Gamma \vdash B, \Delta$}
{$\Gamma \vdash A \land B, \Delta$}
$$
$$
\mathtt{(\;[\; G \vdash \bra\hash A \hash\ket + D
\ , \
G \vdash \bra\hash B \hash\ket + D \;],
\ \ G \vdash \bra\hash A \;\&\& \; B\hash\ket + D \;\; ) \in \pscrel}
$$
The encoding uses HOL's notation ``\texttt{+}'' for multiset union, and
uses \verb!{#! and \verb!#}! to encode the braces for multisets.
Thus each element of $\pscrel$ is a pair whose first
component is a list of its premises, and whose second
component is its conclusion.
% \begin{figure}[t]
% \centering
% \begin{tabular}[c]{ll}
% $c \in \prems \Longrightarrow c \in \derrec~\pscrel~\prems$
% &
% $[\ \ ] \in \dersrec~\pscrel~\prems$
% \\[1em]
% \AxiomC{$p_1 \cdots p_k$}
% \LeftLabel{$\pscrel$}
% \UnaryInfC{$c$}
% \DisplayProof
% &
% \AxiomC{$\{ pms_1 , \cdots , pms_n \}$}
% \dottedLine
% \LeftLabel{$\dersrec~\pscrel$}
% \UnaryInfC{$[\ p_1, \cdots , p_k \ ]$}
% \DisplayProof
% \\[1em]
% \multicolumn{2}{l}{
% $(ps, c) \in \pscrel \ ; \ ps \in \dersrec~\pscrel~\prems
% \Longrightarrow c \in \derrec~\pscrel~\prems$}
% \\[1em]
% \multicolumn{2}{c}{
% \AxiomC{$\{ pms_1, \cdots , pms_n \}$}
% \LeftLabel{$\derrec~\pscrel$}
% \dottedLine
% \UnaryInfC{$c$}
% \DisplayProof}
% \\[2em]
% \AxiomC{$\{ pms_1 , \cdots , pms_n \}$}
% \LeftLabel{$\derrec~\pscrel$}
% \dottedLine
% \UnaryInfC{$c$}
% \DisplayProof
% &
% \AxiomC{$\{ pms_1 , \cdots , pms_n \}$}
% \dottedLine
% \LeftLabel{$\dersrec~\pscrel$}
% \UnaryInfC{$[\ c_1, \cdots , c_m \ ]$}
% \DisplayProof
% \\[1em]
% \multicolumn{2}{l}{
% $c \in \derrec~\pscrel~\prems \ ; \ cs \in \dersrec~\pscrel~\prems$}
% \\
% \multicolumn{2}{c}{
% $\Longrightarrow c\# cs \in \dersrec~\pscrel~\prems$}
% \\[1em]
% \multicolumn{2}{c}{
% \AxiomC{$\{ pms_1 , \cdots , pms_n \}$}
% \dottedLine
% \LeftLabel{$\dersrec~\pscrel$}
% \UnaryInfC{$[\ c, c_1, \cdots , c_m \ ]$}
% \DisplayProof}
% \end{tabular}
% \caption{Inductively Definining Derivable Sequents}
% \label{fig:derrec}
% \end{figure}
We are now in a position to encode the set $\derrec$ of ``recursively
derivable sequents'' given an initial set $\prems$ of premise sequents
and an initial set $\pscrel$ of inference rules. The set $\derrec$
could be defined inductively as shown below:
\begin{tabular}[c]{l@{\extracolsep{1cm}}l}
\\
1 & $\mathtt{\derrec ~::~ (seq ~list~ * ~seq) ~set
~\Rightarrow ~seq ~set
~\Rightarrow ~seq ~set }$
\\
2 & $\mathtt{c \in \prems \Longrightarrow c \in \derrec~\pscrel~\prems}$
\\
3 & $[ \;\; \mathtt{(ps, c) \in \pscrel \ ; }$
\\
4 & $\mathtt{\;\;\;\; \forall ~p . ~p \in (set ~ps)
\Longrightarrow ~p ~\in ~\derrec~\pscrel~\prems \;\; ]}$
\\
5 & $\mathtt{\Longrightarrow ~c ~\in ~\derrec~\pscrel~\prems}$
\end{tabular}
\bigskip
The explanation is as below:
\begin{description}
\item[\rm 1:] A type declaration which tells the proof-assistant that
$\derrec$ accepts a set of inference rules and a set
of sequents, and produces a set of sequents;
\item[\rm 2] The base case of the inductive definition of $\derrec$
captures that ``each premise is itself (vacuously) derivable
from the premises using the rules''. Note that there is an implicit
outermost universal quantifier which is not shown explicitly, but
which binds free variables such as $\mathtt{c, ps}, \pscrel, \prems$.
\item[\rm 3] The first conjunct of an inductive clause
stating that $ps/c$ is a rule instance;
\item[\rm 4:] The second conjunct of the inductive clause which
captures that ``each premise $p$ in the set obtained from sequent
list $ps$ is derivable from the premises $\prems$ using the rules
$\pscrel$''. Here we use a function \verb!set! to convert a list
into the set of its members;
\item[\rm 5:] The ``then'' part of the inductive clause which
concludes that sequent ``$c$ is derivable from $\prems$ using
$\pscrel$''.
\end{description}
\section{Inductive Proofs via Automated Inductive Principles}
Induction principles are generated automatically by Isabelle from the
inductive definition of $\derrec$. A heavily simplified
version for proving an arbitrary property $\mathtt{P}$ is shown below:
\bigskip
\begin{tabular}[c]{l@{\extracolsep{1cm}}l}
1 & $\mathtt{\forall x. \forall P.}$
\\
2 & $[ \mathtt{\;\;\; x~ \in ~\derrec ~\pscrel ~\prems ~;}$
\\
3 & $\mathtt{\;\;\; \forall c . c \in ~\prems \Longrightarrow ~P(c) ~;}$
\\
4 & $\mathtt{\;\;\; \forall c . \forall ps.
[\;\; (ps, c) \in ~\pscrel \;\; ;
~\forall y \in (set ~ps). ~P(y)~]
\Longrightarrow ~P(c)}$
\\
5 & $] \;\;\; \mathtt{ \Longrightarrow ~P(x)}$
\end{tabular}
\bigskip
An explanation is:
\begin{description}
\item[\rm 1:] for all sequents $x$ and all properties $P$
\item[\rm 2 :] if $x$ is derivable from premises $\prems$ using rules
$\pscrel$, and
\item[\rm 3 :] $P$ holds for every premise $c$ in $\prems$, and
\item[\rm 4 :] for each rule, $P$ of its premises implies $P$ of
its conclusion,
\item[\rm 5 :] then $P$ holds of $x$
\end{description}
If you look closely, you will see that this is an induction principle
which we use often in proof-theory: prove that some property holds of
the leaves of a derivation, and prove that the property is preserved
from the premises to the conclusion of each rule. For example,
consider the standard translation from sequents of LK to formulae
given by $\tau(A_1, \cdots , A_n \vdash B_1, \cdots , B_m) = A_1 \land
\cdots \land A_n \limp B_1 \lor \cdots \lor B_m$. We typically use
this translation to argue that all derivable sequents are valid in the
semantics of first-order logic. The proof proceeds by showing that the
translation of the leaves of a derivation are all valid, and showing
that if the translations of the premises are valid then the
translations of the conclusion are valid, for every rule.
\marginpar{NB derrec introduced in previous section}
Thus we have the lemma:
\marginpar{make uniform with text at start of section}
\begin{lemma}
For a property \verb!P1.0!, if
\begin{itemize}
\item if every premise in \verb!prems! obeys \verb!P1.0!,
\item for every rule \verb!(ps, concl)! in \verb!rls!,
if each premise in \verb!ps! being derivable from leaves
\verb!prems! using rules in \verb!rls! and
obeying \verb!P1.0! implies that \verb!concl! obeys
\verb!P1.0!, and
\item the sequent \verb!xb! is derivable from leaves
\verb!prems! using the rules in \verb!rls!,
\end{itemize}
then \verb!xb! obeys \verb!P1.0!:
\end{lemma}
\begin{proof}
Isabelle automatically generates an induction principle from the definition of
\texttt{derrec}.
Since the definition also involves defining \texttt{dersrec} (which expresses
that a list of items are all derivable), the automatically generated principle
involves a property $P_1$ of derivable sequents and a property $P_2$ of lists
of derivable sequents.
Naturally we choose property $P_2$ of a list to be that all members of the
list satisfy $P_1$. That instantiation gives us the lemma.
\end{proof}
\begin{verbatim}
standard drs.inductr:
"[| ?xb : derrec ?rls ?prems ;
!!concl. concl : ?prems ==> ?P1.0 concl ;
!!concl ps. [| (ps, concl) : ?rls; ps : dersrec ?rls ?prems;
Ball (set ps) ?P1.0 |] ==> ?P1.0 concl |] ==> ?P1.0 ?xb"
\end{verbatim}
Using these inductive principles we proved the following lemma about
derivability using Isabelle, where the question marks indicate
free-variables which are implicitly universally quantified:
\begin{lemma}
$$\mathtt{?ps \subseteq \derrec~?\pscrel~?\prems
\ ; \
?c \in \derrec~?\pscrel~?ps
\ \Longrightarrow \
?c \in \derrec~?\pscrel~?\prems
}
$$
% Isabelle derrec_trans;
\noindent
If each premise in $ps$ is derivable from
premises $\prems$ using rules $\pscrel$,
and $c$ is derivable from $ps$ using $\pscrel$,
then $c$ is derivable from $\prems$ using $\pscrel$.
\end{lemma}
\section{An Even Deeper Embedding: Derivation Trees As Objects}
\label{s-dtobj}
The main advantage of the method outlined in the previous section
was that there was no concrete representation of a derivation. That
is, we relied on the proof-assistant to perform pattern-matching and
rule instantiations in an appropriate way, so that all we needed was
to capture the idea that derivations began with premises and ended
with a single sequent.
When we reason about cut-elimination, often we are required to
perform transformations on explicit derivations. We therefore need a
representation of such trees inside our encoding.
In previous work~\cite{DG02}, we described such an encoding using the
following datatype:
\begin{verbatim}
datatype seq dertree = Der seq (seq dertree list)
| Unf seq
\end{verbatim}
The declaration states that a derivation tree can either be an
\verb!Unf!inished (unproved)
leaf sequent built using the constructor \verb!Unf!,
or it can be a pair consisting of a conclusion sequent and a list of
sub-derivation-trees bound together using the constructor \verb!Der!.
In that work, we also described how we maintained substitutions as lists of
pairs of the form $(x, t)$ representing the substitution $x := t$. We
also described how we manipulated substitutions and instantiation
directly to obtain rule instances.
We required such low-level aspects to be made explicit so that we
could reason about display logic which required us to check conditions
on rules such as ``a rule is closed under substitution of arbitrary
structures for variables''.
Our use of \verb!dertee! can be seen as an even deeper embedding of
proof-theory into Isabelle/HOL since it utilises the proof-assistant
to describe a ``proof object'' rather than to specify directly
the provable sequents.
Omitting details now, suppose we define \verb!valid rli dt! to hold
when derivation tree \verb!dt! uses rules from \verb!rli! only and
has no \verb!Unf!inished leaves. We linked these two approaches to specifying
the provable sequents by proving:
\begin{lemma}
$$\mathtt{valid~?\pscrel~?dt~\Longrightarrow (conclDT~?dt)
\in \derrec ~?rls~\{\}}$$
\noindent
If derivation tree $dt$ is valid wrt the rules $\pscrel$ then its
conclusion is derivable from the empty set of premises using $\pscrel$.
\end{lemma}
\begin{lemma}
$$\mathtt{?c \in \derrec ~?\pscrel ~\{\}
\Longrightarrow ~EX ~dt. ~valid ~?\pscrel ~dt
~\& ~conclDT ~dt ~= ~?c}$$
\noindent
If the sequent $c$ is derivable from the empty set of premises using
rules $\pscrel$ then there exists a derivation tree $dt$ which is
valid wrt $\pscrel$, whose conclusion is $c$.
\end{lemma}
Thus we now know that our ``deep embedding'' of derivability using
$\derrec$ can be faithfully captured using the ``even deeper''
embedding using explicit derivation trees. Indeed, the lemmas allow us
to move freely between the two embeddings at will to omit or include
details as required.
\section{Our General Derivability Predicates} \label{s-dp}
SOME OF THIS IS COVERED IN \S5
We now briefly describe the functions we used to describe
derivability. A fuller account is given in \cite{gore-india}. This
framework is general in that a rule merely consists of ``premises''
and a ``conclusion'', and is independent of whether the things derived
are formulae, sequents, or other constructs, but we will refer to them
as formulae.
\begin{verbatim}
types 'a psc = "'a list * 'a" (* single step inference *)
consts
derl, adm :: "'a psc set => 'a psc set"
dersl :: "'a psc set => ('a list * 'a list) set"
dercsl :: "'a psc set => ('a list list * 'a list) set"
derrec :: "'a psc set => 'a set => 'a set"
dersrec :: "'a psc set => 'a set => 'a list set"
\end{verbatim}
An inference rule \texttt{'a psc} is a list of premises \texttt{ps}
and a conclusion \texttt{c}. Then, \texttt{derl rls} is the set of
rules derivable from the rule set \texttt{rls}, and \texttt{derrec rls
prems} is the set of formulae derivable using rules \texttt{rls}
from the set \texttt{prems} of premises. These were defined as
inductive sets, using also the functions \texttt{dersl} and
\texttt{dersrec}. So $\mathtt{(ps, c) \in \derl\ \rls}$ reflects the
shape of a derivation tree: \texttt{ps} is a list of exactly the
premises used, in the correct order, whereas $\mathtt{c \in \derrec\
\rls\ prems}$ holds even if the set of premises \texttt{prems}
contains extra formulae.
The auxiliary function \texttt{dersrec} represents several formulae,
all derivable from the premises. The auxiliary function
\texttt{dersl} represents several derivation trees side by side;
$\mathtt{(ps, cs) \in dersl~rls}$ when \texttt{ps} is the
concatenation of their lists of premises, and \texttt{cs} is the list
of their conclusions. The function \texttt{dercsl} is similar, but it
shows which premises are part of which tree. That is, $\mathtt{(pss, cs) \in
\texttt{dercsl}\ rls}$ implies $\mathtt{(concat\ pss, cs) \in \texttt{dersl}\
rls}$. Curiously, we have used this framework for several years, and
only recently we found the need to redefine \derl\ using
\texttt{dercsl} rather than \texttt{dersl} as the auxiliary function.
The key clauses for these functions are shown below:
\begin{verbatim}
dtderI : "[| (ps, concl) : pscrel ; (pss, ps) : dersl pscrel |]
==> (pss, concl) : derl pscrel"
derI : "[| (ps, concl) : pscrel ; ps : dersrec pscrel prems |]
==> concl : derrec pscrel prems"
\end{verbatim}
We obtained the expected results linking \texttt{derl} and \texttt{derrec},
and a number of results expressing transitivity of derivation and the
results of derivation using derived rules, for example:
\begin{verbatim}
derl_trans : "[| (?ps, ?c) : derl ?rls; (?x, ?ps) : dersl ?rls |]
==> (?x, ?c) : derl ?rls"
derl_deriv_eq : "derl (derl ?rls) = derl ?rls"
derrec_trans_eq : "derrec ?rls (derrec ?rls ?prems) = derrec ?rls ?prems"
\end{verbatim}
A simplified version of the induction principle
generated by the definition of the inductive set \derrec\ is as follows:
$$
\frac {x \in derrec\ rls\ prems \quad
\forall c \in prems. P\ c \quad
\forall (ps, c) \in rls. (\forall p\ in\ ps. P\ p) \Rightarrow P\ c}
{P\ x}
$$
We may contrast use of this principle with induction on the height of a
derivation tree.
Using induction on the height, it is possible, and in some proofs necessary,
to transform a sub-tree in some height-preserving (or height-reducing) way, and
use the assumption that the transformed tree has property $P$.
That approach is not available when using the induction principle above,
and was not needed for our earlier proofs.
Where we have a property of two derivations, such as cut-admissibility,
we need a more complex induction principle, which we derived
(limited to the case where the set \textit{prems} of ultimate assumptions is
empty) :
$$
\begin{array}{c}
cl \in derrec\ rlsl\ \{\} \quad cr \in derrec\ rlsr\ \{\} \\
\forall (lps, lc) \in rlsl, (rps, rc) \in rlsr.\
(\forall lp\ in\ lps. P\ lp\ rc) \land (\forall rp\ in\ rps. P\ lc\ rp)
\Rightarrow P\ lc\ rc \\
\hline { P\ cl\ cr}
\end{array}
$$
Finally, $(ps, c)$ is an admissible rule iff: if all premises in $ps$
are derivable, then $c$ is derivable:\\
$(ps, c) \in \adm\ \rls \iff
(set\ ps \subseteq \derrec\ \rls \ \ \Rightarrow \ \ c \in \derrec\
\rls)
$.
We obtained the following four results, which were surprisingly tricky
since \adm\ is not monotonic:
\begin{verbatim}
"derl ?rls <= adm ?rls" "adm (adm ?rls) = adm ?rls"
"adm (derl ?rls) = adm ?rls" "derl (adm ?rls) = adm ?rls"
\end{verbatim}
\section{Subformula Relation and Rule Extensions with Arbitrary Contexts} \label{s-gls}
Our generalised definition of formulae allows a single definition of
the immediate (proper) subformula relation, \texttt{ipsubfml}, which
will not need to be changed when new connectives are added.
\begin{verbatim}
consts ipsubfml :: "(formula * formula) set"
inductive "ipsubfml" (* proper immediate subformula relation *)
intros ipsI : "P : set Ps ==> (P, FC conn Ps) : ipsubfml"
\end{verbatim}
%
As noted in \S\ref{s-eol}
a sequent is a pair of multisets of formulae, written $\Gamma \vdash \Delta$.
% \begin{verbatim}
% datatype 'a sequent =
% Sequent "'a multiset" "'a multiset" ("((_)/ |- (_))" [6,6] 5)
% \end{verbatim}
Given a rule such as $(\vdash \land)$ in the form on the left,
$$
\MR_s = \frac{\vdash A \quad \vdash B} {\vdash A \land B}
\qquad
\MR_e = \frac{X \vdash Y, A \quad X \vdash Y, B} {X \vdash Y, A \land B}
$$
we define functions \texttt{extend} and \texttt{pscmap}, such that
(for example)
\begin{gather*}
\texttt{extend}\ (X \vdash Y)\ (U \vdash V) = (X + U) \vdash (Y + V) \\
\MR_e = \texttt{pscmap}\ (\texttt{extend}\ (X \vdash Y))\ \MR_s
\end{gather*}
Thus \texttt{pscmap} uniformly extends the skeleton provided by
$\MR_s$ with arbitrary contexts $X$ and $Y$ on respective sides to
encode $\MR_e$ using multiset addition $+$.
Then \texttt{extrs} $S$ means the set of all such extensions of all rules in the set
$S$.
\begin{verbatim}
consts
extend :: "'a sequent => 'a sequent => 'a sequent"
extrs :: "'a sequent psc set => 'a sequent psc set"
defs
extend_def : "extend fmls seq == seq + fmls"
pscmap_def : "pscmap f (ps, c) = (map f ps, f c)"
\end{verbatim}
Then we define \texttt{lksss}, the set of rules for Gentzen's LK; we
show just a selection. The rules below are the traditional invertible
logical introduction rules from LK (without any context):
$$
\frac{A, B \vdash}{A \land B \vdash}
\qquad
\frac{\vdash A \quad \vdash B}{\vdash A \land B }
\qquad
\frac{A \vdash \quad B \vdash}{A \lor B \vdash}
\qquad
\frac{\vdash A, B}{\vdash A \lor B }
\qquad
\frac{A \vdash B}{\vdash A \to B }
\qquad
\frac{B \vdash \quad \vdash A}{A \to B \vdash}
$$
\begin{verbatim}
inductive "lksir" (* LK right introduction rules *)
intros
andr : "([{#} |- {#A#}, {#} |- {#B#}], {#} |- {#A && B#}) : lksir"
orr : "([{#} |- {#A#} + {#B#}], {#} |- {#A v B#}) : lksir"
...
\end{verbatim}
Similar rules \texttt{lksil} give the
traditional invertible rules for left-introduction. By adding the
initial rule ``axiom'' below we obtain the set of ``unextended'' rules
\texttt{lksne} for LK:
\begin{verbatim}
inductive "lksne" (* LK rules before being extended *)
intros
axiom : "([], {#A#} |- {#A#}) : lksne"
ilI : "(ps, c) : lksil ==> (ps, c) : lksne"
irI : "(ps, c) : lksir ==> (ps, c) : lksne"
...
\end{verbatim}
We can now form the full extended set of rules \texttt{lksss} for LK,
where \texttt{flr} is an arbitrary pair of contexts $X, Y$
(regarded as a sequent, $X \vdash Y$).
\begin{verbatim}
inductive "lksss"
intros
extI : "psc : lksne ==> pscmap (extend flr) psc : lksss"
\end{verbatim}
The traditional K-rule below at left may be encoded as shown below by
extending the skeleton shown at right, in its conclusion only:
\[
\AxiomC{$\Gamma \vdash A$}
\RightLabel{$(K)$}
\UnaryInfC{$\Sigma, \wbx\Gamma \vdash \wbx A, \Delta$}
\DisplayProof
\qquad
\AxiomC{$ \Gamma \vdash A$}
\UnaryInfC{$\wbx\Gamma \vdash \wbx A$}
\DisplayProof
\]
\begin{verbatim}
inductive "K"
intros
I : "([X |- {#B#}], mset_map Box X |- {#Box B#}) : K"
\end{verbatim}
Note that $X$ is a multiset, and $\Box X$ is informal notation for applying
$\Box$ to each member of $X$; this is formalised as \texttt{mset\_map},
used in the formalised \texttt{K} rule.
Using a similar notation we write $\Box B^k$ for $(\Box B)^k$,
the multiset containing $n$ copies of $\Box B$.
Development of \texttt{mset\_map} and relevant lemmas is in the source files
\texttt{Multiset\_no\_le.\{thy,ML\}}.
By extending the skeleton of the LK calculus and adding the new
$K$ rule above, we could obtain an encoding of the
traditional sequent calculus for the modal logic K:
\marginpar{We don't actually do this - the closest is Jesse's
definition of \texttt{gs4\_rls}}
\begin{verbatim}
inductive "lksK"
intros
extI : "psc : lksne ==> pscmap (extend flr) psc : lksK"
K : "psc : K ==> psc : lksK"
\end{verbatim}
\section{Generalising Cut-Admissibility Proofs} \label{s-cagen}
We now show how our previous work on multicut admissibility for LK
can be formulated to make it as general as possible.
%
For proofs of \ctra{}, without height-preservation, a stronger
induction principle is required. The axioms of our systems will be
allowed to apply to arbitrary formula, not only atoms, and this
excludes the possibility of proving height-preserving invertibility
and \ctra{} results. To compensate for the lack of an explicit height,
a double induction on premises (instead of explicit derivation height)
and formula size (as measured by any well-founded subformula relation)
is used. The implementation of this first encodes an inductive step
condition:
\begin{definition}[\texttt{gen\_step}] \label{d-gen-step} ~\\
%isabelle gen_step.simps
For a formula $A$, a property $P$,
a subformula relation \texttt{sub},
a set of sequents \texttt{derivs},
% a set of rules \texttt{rls},
% a set of \texttt{rls}-derivable sequents \texttt{derivs}
% (e.g. \texttt{derrec rls prems}),
and a particular rule \texttt{r = $(ps, c)$},
\texttt{gen\_step $P\ A$ sub derivs r} means:
\noindent If
\begin{itemize}
\item forall $A'$ such that \texttt{$(A', A) \in$ sub}
and all sequents $D \in$ \texttt{derivs} the property
$P\ A'\ D$ holds,
\item for every premise $p \in ps$ both \texttt{$p \in$ derivs}
and $P\ A\ p$ holds, and
\item $c \in$ \texttt{derivs}
\end{itemize}
then $P\ A\ c$ holds.
\end{definition}
Typically \texttt{derivs} will be the set of sequents derivable using
a given set \texttt{rls} of rules, \texttt{derivs} = \texttt{derrec rls prems}.
In English, this step condition states that if a property $P$ is true
generally for formulae of lower rank $A'$, and for the (derivable)
premises of a particular rule then the property holds for the conclusion
of that rule. The main theorem, named \texttt{gen\_step\_lem} and given
as Theorem~\ref{genstep:lem} below, states that if this step case can
be proved for all possible rule instances then $P$ holds for all cases.
\begin{theorem}[\texttt{gen\_step\_lem}]\label{genstep:lem}~
%isabelle gen_step_lem
If
\begin{itemize}
\item $A$ is in the well-founded part of the subformula relation \texttt{sub},
\item sequent \texttt{S} is \texttt{rls}-derivable and
\item for all formulae $A'$ and all possible rules \texttt{r} in \texttt{rls},
% and all \texttt{rls}-derivable sequents \texttt{derrec rls \{\}},
the induction step condition
\texttt{gen\_step $P\ A'$ sub (derrec rls \{\}) r}
holds
\end{itemize}
then \texttt{P\ A\ S} holds.
\end{theorem}
In \S\ref{s-deriv} we mentioned the induction principle used for
deriving cut-admissibility, or indeed any property $P$ of two-premise
subtrees. In the diagram below, to prove $P (\MR_{l}, \MR_{r})$, the
induction assumption is that $P (\MQ_{li}, \MR_{r})$ and $P (\MR_{l},
\MQ_{rj})$ hold for all $i$ and $j$:
% \begin{center}
% \bpf
% \A "$\MQ_{l1} \ldots \MQ_{ln}$"
% \U "$\MR_{l}$" "$\rho_l$"
% \A "$\MQ_{r1} \ldots \MQ_{rm}$"
% \U "$\MR_{r}$" "$\rho_r$"
% \B "?" "(\textit{cut ?})"
% \epf
% \end{center}
\begin{center}
\begin{prooftree}
\AxiomC{$\MQ_{l1} \ldots \MQ_{ln}$}
\RightLabel{$\rho_l$}
\UnaryInfC{$\MR_{l}$}
\AxiomC{$\MQ_{r1} \ldots \MQ_{rm}$}
\RightLabel{$\rho_r$}
\UnaryInfC{$\MR_{r}$}
\RightLabel{(\textit{cut ?})}
\dottedLine
\BinaryInfC{?}
\end{prooftree}
\end{center}
A proof of $P (\MR_{l}, \MR_{r})$ using this induction assumption
inevitably proceeds according to what the rules $\rho_l$ and $\rho_r$
are, and further, for a cut-formula $A$, whether it is principal in
either or both of $\rho_l$ and $\rho_r$. But our proofs also use
induction on the size of the cut-formula, or, more generally, on some
well-founded relation on formulae.
% Since the $\MQ_{li}$, etc, above are sequents,
So we actually consider a property $P\ A\ (cl, cr)$
where $psl$ are the premises $\MQ_{l1} \ldots \MQ_{ln}$ of rule
$\rho_l$, and $cl$ is its conclusion $\MR_{l}$, and analogously for
$\rho_r$, and $A$ is the cut-formula. In proving $P\ A\ (\MR_{l},
\MR_{r})$, in addition to the inductive assumption above, we assume
that $P\ A' \ (da, db)$ holds generally for $A'$ smaller than $A$ and
all sequents $da$ and $db$ which are ``\texttt{rls}-derivable'',
ie, derivable from the empty set of premises using rules from $rls$.
These intuitions give the following definition \texttt{gen\_step2sr} of
a condition which permits one step of the inductive proof:
% where we shorten ``derivable from the empty set of premises using rule
% from \texttt{rls}'' to ``\texttt{rls}-derivable'':
\begin{definition}[\texttt{gen\_step2sr}]
For a formula \texttt{A},
a property \texttt{P},
a subformula relation \texttt{sub},
a set of rules \texttt{rls},
inference rules \texttt{(psl, cl)}, and
\texttt{(psr, cr)},
the property \texttt{gen\_step2sr} holds iff:
\noindent If
\begin{itemize}
\item
\texttt{P~A'~(da,~db)} holds
for all subformulae \texttt{A'} of \texttt{A}
and all \texttt{rls}-derivable sequents
\texttt{da} and \texttt{db};
\item for each \texttt{pa} in \texttt{psl}, \texttt{pa} is
\texttt{rls}-derivable and \texttt{P A (pa, cr)} holds;
\item for each \texttt{pb} in \texttt{psr},
\texttt{pb} is \texttt{rls}-derivable and
\texttt{P A (cl, pb)} holds;
\item \texttt{cl} and \texttt{cr} are \texttt{rls}-derivable,
\end{itemize}
then \texttt{P A (cl, cr)} holds.
\begin{verbatim}
gen_step2sr_simp :
"gen_step2sr ?P ?A ?sub ?rls ((?psl, ?cl), (?psr, ?cr)) =
( (ALL A'. (A', ?A) : ?sub -->
(ALL da:derrec ?rls {}. ALL db:derrec ?rls {}. ?P A' (da, db)))
-->
(ALL pa:set ?psl. pa : derrec ?rls {} & ?P ?A (pa, ?cr)) -->
(ALL pb:set ?psr. pb : derrec ?rls {} & ?P ?A (?cl, pb)) -->
?cl : derrec ?rls {} --> ?cr : derrec ?rls {}
--> ?P ?A (?cl, ?cr) )"
\end{verbatim}
\end{definition}
The main theorem \texttt{gen\_step2sr\_lem} below for proving an
arbitrary property $P$ states that if the step of the inductive proof
is possible for all cases of final rule instances $(psl, cl)$ and
$(psr, cr)$ on each side, then $P$ holds in all cases.
\begin{theorem}[\texttt{gen\_step2sr\_lem}]
If \texttt{A} is in the well-founded part of the subformula relation;
sequents \texttt{seql} and \texttt{seqr} are \texttt{rls}-derivable ;
and for all formulae \texttt{A}, and all rules \texttt{(psl, cl)} and
\texttt{(psr, cr)}, our induction step condition
\texttt{gen\_step2sr P A sub rls ((psl, cl), (psr, cr))}
holds, then
\texttt{P A (seql, seqr)} holds.
\begin{verbatim}
gen_step2sr_lem :
"[| ?A : wfp ?sub ;
?seql : derrec ?rls {} ; ?seqr : derrec ?rls {} ;
ALL A. ALL (psl, cl):?rls. ALL (psr, cr):?rls.
gen_step2sr ?P A ?sub rls ((psl, cl), (psr, cr)) |]
==> ?P ?A (?seql, ?seqr)"
\end{verbatim}
\end{theorem}
This enables us to split up an inductive proof, by showing,
separately, that \texttt{gen\_step2sr} holds for particular cases of
the final rules $(psl, cl)$ and $(psr, cr)$ on each side. In some
cases these results apply generally to different calculi. For
example, the inductive step for the case where the cut-formula $A$ is
parametric, not principal, on the left is encapsulated in the
following theorem where \texttt{prop2 mar ?erls ?A (?cl, ?cr)} means
that the conclusion of a multicut on \texttt{A} with premises
\texttt{cl} and \texttt{cr} is derivable using rules \texttt{erls}.
\begin{theorem}
If weakening is admissible for the rule set \texttt{erls}, all
extensions of some rule \texttt{(ps, c)} are in the rule set
\texttt{erls}, and the final rule instance of the left hand subtree
is an extension of \texttt{(ps, c)} where the cut-formula \texttt{A}
is not in the succedent of \texttt{c} (meaning that \texttt{A} is
parametric on the left), then
\verb!gen_step2sr (prop2 mar ?erls) ?A ?sub ?rls (?pscl, ?pscr)!
holds.
\begin{verbatim}
mk_sr1 lmg_gen_step' :
"[| wk_adm ?erls; extrs {(?ps, ?c)} <= ?erls; ~ ?A :# succ ?c;
?pscl = pscmap (extend ?flr) (?ps, ?c) |]
==> gen_step2sr (prop2 mar ?erls) ?A ?sub ?rls (?pscl, ?pscr)"
\end{verbatim}
\end{theorem}
Of course, for a system containing explicit weakening rules,
weakening is {\it a fortiori} admissible.
% NEED TO ADJUST THIS - NOT INCLUDING GLS IN THIS PAPER
% This result codifies parametric proof steps, and is quite general
% enough to apply in the proof for \GLS. As we note later, the proof
% for \GLS\ involves one really difficult case and a lot of fairly
% routine cases. In dealing with the routine cases, automated theorem
% proving has the benefit of ensuring that no detail is overlooked; in
% addition we have the fact that, as in this example, we often have more
% general theorems that apply directly to a set of rules such as \GLS.
Notice that all of this section deals with a shallow embedding of
derivations; it does not apply to proofs which require
derivation trees to be represented explicitly.
As noted in \S\ref{s-dtobj}, the derivability of a sequent is equivalent fo
the existence of a valid derivation tree for it, and in \S\ref{s-main-lemmas}
we describe the similar approach for explicit derivation trees.
\section{Statements of the Main Lemmas in Isabelle}\label{s-main-lemmas}
We now describe how we encoded the statements of the main lemmas
regarding the admissibility of weakening, contraction and cut, along
with the encoding of the invertibility lemmas required for contraction
admissibility.
A set \texttt{rls} of rules satisfies the weakening admissibility property if,
whenever a sequent $X \vdash Y$ is derivable, any larger sequent
$(X \vdash Y) + (U \vdash V) = (X, U \vdash Y, V)$ is derivable:
\begin{verbatim}
wk_adm :: "'a sequent psc set => bool"
wk_adm_def : "wk_adm rls ==
ALL XY. XY : derrec rls {} --> (ALL UV. XY + UV : derrec rls {})"
\end{verbatim}
Here, the variable \texttt{rls} is forced to be a set of sequent rules
by the type of \texttt{wk\_adm}, and thence
the variables \texttt{XY} and \texttt{UV} will be forced to be
of type \texttt{sequent} by the typing restrictions on the inputs to
\texttt{derrec}.
\begin{definition}
A rule \verb|(ps, c)| is \emph{invertible} with respect to a set
\verb|rls| of rules if, whenever \verb|c| is derivable using
\verb!rls!, then every member of \verb|ps| is derivable using
\verb!rls!.
\end{definition}
Here, the definition of \verb|dersrec| hides a universal
quantifier over the members of the list \verb|ps|:
\begin{verbatim}
inv_rl.simps: "inv_rl ?rls (?ps, ?c)
= (?c : derrec ?rls {} --> ?ps : dersrec ?rls {})"
\end{verbatim}
To encode contraction, we utilise an axiomatic type class for
sequents, described in more detail
elsewhere~\cite{dawson-gore-generalised}.
Thus we can write
$(A \vdash 0) + (A \vdash 0) \leq (X \vdash Y)$ to mean that
the multiset $X$ contains at least two copies of $A$
and write
$(X \vdash Y) - (A \vdash 0)$
for the sequent obtained by deleting one of these copies from $X$.
A set \texttt{rls} of rules satisfies the contraction admissibility property
for the formula $A$ if,
whenever a derivable sequent $X \vdash Y$ satisfies
$(A \vdash 0) + (A \vdash 0) \leq (X \vdash Y)$,
the sequent $(X \vdash Y) - (A \vdash 0)$ is derivable,
and likewise for $0 \vdash A$.
The first condition \verb|ms_of_seq As = {#?A#}|
says that the multiset of formulae on both sides of the sequent $UV$
is the singleton multiset \verb|{#?A#}|, thus capturing that the
contraction can happen on either side of the turnstile:
\begin{verbatim}
ctr_adm_def :
"ctr_adm ?rls ?A == ALL UV. ms_of_seq UV = {#?A#} -->
(ALL XY. XY : derrec ?rls {} --> UV + UV <= XY -->
XY - UV : derrec ?rls {})"
\end{verbatim}
A pair of sequents satisfies the properties \texttt{cas} and \texttt{car} if
cut-admissibility is available (in different senses)
for that pair of sequents.
Precisely,
$(X_l \vdash Y_l, X_r \vdash Y_r) \in \texttt{car}\ \texttt{rls}\ A$ iff
$(X_l, (X_r - A) \vdash (Y_l - A), Y_r)$ is derivable using \verb!rls!,
whereas \texttt{cas} means that this holds, conditionally on
$X_l \vdash Y_l$ and $X_r \vdash Y_r$ being themselves derivable.
\begin{verbatim}
car_eq: "((?Xl |- ?Yl, ?Xr |- ?Yr) : car ?rls ?A) =
((?Xl + (?Xr - {#?A#}) |- ?Yl - {#?A#} + ?Yr) : derrec ?rls {})"
cas_eq: "((?seql, ?seqr) : cas ?rls ?A) =
(?seql : derrec ?rls {} & ?seqr : derrec ?rls {} -->
(?seql, ?seqr) : car ?rls ?A)"
\end{verbatim}
% "([| ?seql : derrec ?rls {}; ?seqr : derrec ?rls {} |]
% ==> (?seql, ?seqr) : car ?rls ?A) ==> (?seql, ?seqr) : cas ?rls ?A"
When we are talking about proving these by induction on the derivation
of the two sequents, that is, we are talking about two sequents which
are derivable, then these two concepts become equivalent.
\begin{verbatim}
prop2_def : "prop2 f rls A seqs == seqs : f rls A"
gs2_cas_eq_car: "gen_step2sr (prop2 cas ?rls) ?A ?sub ?rls =
gen_step2sr (prop2 car ?rls) ?A ?sub ?rls"
\end{verbatim}
Sometimes we need to proceed by induction on (for example) the length of a
derivation by which a sequent can be ontained, rather than by the fact of a
sequent having been obtained earlier in the same derivation.
So to compare (say) the heights of derivations, we must be able to define them
and for this we need to look at explicit derivation trees.
Firstly we define \texttt{casdt}: two \emph{valid} (ie. no unproved
leaves, and all steps are rules of \texttt{rls}) derivation trees
satisfy \texttt{casdt rls A} if their
conclusions satisfy \texttt{car}
\begin{verbatim}
casdt.I: "valid rls dtl & valid rls dtr -->
(conclDT dtl, conclDT dtr) : car rls A ==> (dtl, dtr) : casdt rls A"
\end{verbatim}
The step of the induction proof based on explicit derivation trees is
expressed using the following definitions and lemmas.
THIS STUFF BASICALLY COMBINES THE APPROACHES OF SECTIONS 6 and 7 - SHOULD IT
GO EARLIER?
\begin{definition}[\texttt{gen\_step\_tr}]
For all properties \verb!P!, all formulae \verb!B!,
all ``sub-formula'' relations \verb!sub! and all derivation trees \verb!dta!,
\texttt{gen\_step\_tr P B sub dta} holds iff:\\
if
\begin{itemize}
\item \verb!P C dtb! holds for all subformulae \verb!C! of \verb!B!
and all derivation trees \verb!dtb!, and
\item
\verb!P B dtp! holds for all the immediate subtrees \verb!dtp! of
\verb!dta!
\end{itemize}
then \verb!P B dta! holds.
\end{definition}
\begin{verbatim}
gen_step_tr_def: "gen_step_tr ?P ?B ?sub ?dta ==
(ALL C. (C, ?B) : ?sub --> (ALL dtb. P C dtb)) -->
(ALL dtp:set (nextUp ?dta). ?P ?B dtp) --> ?P ?B ?dta"
\end{verbatim}
\begin{lemma}[\texttt{gen\_step\_tr\_lem}]
For all properties \verb!P!,
for all formulae \verb!A!,
for all relations \verb!sub!,
for all derivations \verb!dt!,
if \verb!A! is in the well-founded part of \verb!sub!,
and \verb!gen_step_tr P B sub dtb! holds for all formulae \verb!B! and
all derivations \verb!dtb!, then
\verb!P A dt! holds.
\end{lemma}
\begin{verbatim}
gen_step_tr_lem: "[| ?A : wfp ?sub ;
ALL B dtb. (gen_step_tr ?P B ?sub dtb) |] ==> ?P ?A ?dt"
\end{verbatim}
\begin{definition}[\texttt{gen\_step2\_tr}]
For all properties \verb!P!,
for all formulae \verb!B!,
for all ``sub-formula'' relations \verb!sub!,
for all pairs \verb!(dta, dtb)! of derivation trees,
\texttt{gen\_step2\_tr P B sub (dta, dtb)} holds iff:\\
if
\begin{itemize}
\item \verb!P C (dtaa, dtbb)! holds for sub-formulae \verb!C! of \verb!B!
and all derivation trees \verb!dtaa! and \verb!dtbb!,
and
\item \verb!P B (dtp, dtb)! holds for all immediate subtrees \verb!dtp! of
\verb!dta!,
and
\item \verb!P B (dta, dtq)! holds for all immediate subtrees \verb!dtq!
of \verb!dtb!
\end{itemize}
then \verb!P B (dta, dtb)! holds:
\end{definition}
\begin{verbatim}
gen_step2_tr.simps: "gen_step2_tr ?P ?B ?sub (?dta, ?dtb) =
((ALL C. (C, ?B) : ?sub --> (ALL dtaa dtbb. P C (dtaa, dtbb))) -->
(ALL dtp:set (nextUp ?dta). ?P ?B (dtp, ?dtb)) -->
(ALL dtq:set (nextUp ?dtb). ?P ?B (?dta, dtq)) --> ?P ?B (?dta, ?dtb))"
\end{verbatim}
\begin{lemma}[\texttt{gen\_step2\_tr\_lem}]
For all properties \verb!P!,
for all formulae \verb!A!,
for all relations \verb!sub!,
for all derivation trees \verb!dta! and \verb!dtb!,
if \verb!A! is in the well-founded part of \verb!sub!,
and \verb!gen_step2_tr P B sub (dtaa, dtbb)! holds for all formulae \verb!B! and
all derivations \verb!dtaa! and \verb!dtbb!, then
\verb!P A (dta, dtb)! holds:
\end{lemma}
\begin{verbatim}
gen_step2_tr_lem: "[| ?A : wfp ?sub ;
ALL B dtaa dtbb. gen_step2_tr ?P B ?sub (dtaa, dtbb) |]
==> ?P ?A (?dta, ?dtb)"
\end{verbatim}
These properties are exact analogues, for explicit derivation trees,
of the properties
\texttt{gen\_step} and \texttt{gen\_step2sr}
and lemmas \texttt{gen\_step\_lem} and \texttt{gen\_step2sr\_lem},
with the following theorem linking them.
\begin{lemma}
\end{lemma}
\begin{verbatim}
gs2_tr_casdt_sr:
"gen_step2sr (prop2 cas ?rls) ?A ?ipsubfml ?rls (botRule ?dta, botRule ?dtb)
==> gen_step2_tr (prop2 casdt ?rls) ?A ?ipsubfml (?dta, ?dtb)"
\end{verbatim}
However, the purpose of using explicit derivation trees is to define different
induction patterns.
For example, we defined an induction pattern which depends on the inductive
assumption that the property $P$ holds for the given tree on one side, and any
smaller tree on the other side.
\begin{definition}
For all \verb!a!,
all \verb!b!,
and all functions \verb!f!,
the pair \verb!(a, b)! is in \verb!measure f!
iff \verb!f a < f b!.
For all properties \verb!P!,
for all formulae \verb!A!,
for all subformula relations \verb!sub!,
for all pairs \verb!(dta, dtb)! of derivations,
\texttt{height\_step2\_tr P A sub (dta, dtb)} holds iff: \\
if
\begin{itemize}
\item \verb!P B (a, b)! holds for all subformulae \verb!B! of \verb!A! and
for all derivation trees \verb!a! and \verb!b!,
\item for all derivation trees \verb!dtp! of smaller height than \verb!dta!,
\verb!P A (dtp, dtb)!, and
\item for all derivation trees \verb!dtq! of smaller height than \verb!dtb!,
\verb!P A (dta, dtq)!,
\end{itemize}
then \verb!P A (dta, dtb)! holds.
\end{definition}
\begin{verbatim}
measure_eq: "((?a, ?b) : measure ?f) = (?f ?a < ?f ?b)"
"height_step2_tr ?P ?A ?sub (?dta, ?dtb) =
((ALL A'. (A', ?A) : ?sub --> (ALL a b. ?P A' (a, b))) -->
(ALL dtp. heightDT dtp < heightDT ?dta --> ?P ?A (dtp, ?dtb)) -->
(ALL dtq. heightDT dtq < heightDT ?dtb --> ?P ?A (?dta, dtq)) -->
?P ?A (?dta, ?dtb))"
\end{verbatim}
In some cases we found that this wasn't enough, and defined a more
general pattern, where the inductive assumption applies where the sum
of heights of the two trees is smaller.
\begin{definition}
For a property \verb!P!,
a formula \verb!A!,
a subformula relation \verb!sub!,
and a pair of derivations \verb!(dta, dtb)!,
\texttt{sumh\_step2\_tr P A sub (dta, dtb)} holds iff: \\
if
\begin{itemize}
\item \verb!P B (a, b)!
holds for all subformulae \verb!B! of \verb!A!
and all derivation trees \verb!a! and \verb!b!, and
\item for all derivation trees \verb!dta'! and \verb!dtb'! such that
$\texttt{heightDT dta'} + \texttt{heightDT dtb'} <
\texttt{heightDT dta} + \texttt{heightDT dtb}$,
\verb!P A (dta', dtb')! holds
\end{itemize}
then \verb!P A (dta, dtb)! holds
\end{definition}
\begin{verbatim}
sumh_step2_tr_eq: "sumh_step2_tr ?P ?A ?sub (?dta, ?dtb) =
((ALL B. (B, ?A) : ?sub --> (ALL a b. ?P B (a, b))) -->
(ALL dtaa dtbb.
heightDT dtaa + heightDT dtbb < heightDT ?dta + heightDT ?dtb -->
?P ?A (dtaa, dtbb)) -->
?P ?A (?dta, ?dtb))"
\end{verbatim}
We could of course generalise this by replacing \texttt{heightDT} by any
natural number function, which may be differrent for trees on the
left and right sides.
Indeed it could be further generalised to any well-founded relation on pairs
of derivation trees.
Each of these properties is successively weaker since the
corresponding inductive assumption is stronger, hence $P$ applies to a
correspondingly wider class of derivations: as formalised next.
\begin{lemma}
For a property \verb!P!,
a formula \verb!A!,
a relation \verb!sub!,
and for a pair \verb!(dta, dtb)! of derivations:
\begin{enumerate}
\item \verb!gen_step2_tr! implies \verb!height_step2_tr!
\item \verb!height_step2_tr! implies \verb!sumh_step2_tr!
\end{enumerate}
\end{lemma}
\begin{verbatim}
gs2_tr_height: "gen_step2_tr ?P ?A ?sub (?dta, ?dtb) ==>
height_step2_tr ?P ?A ?sub (?dta, ?dtb)"
hs2_sumh: "height_step2_tr ?P ?A ?sub (?dta, ?dtb) ==>
sumh_step2_tr ?P ?A ?sub (?dta, ?dtb)"
\end{verbatim}
Accordingly we need the lemma that proving these step results is sufficient
for only the weakest of them.
\begin{lemma}[\texttt{sumh\_step2\_tr\_lem}]
For a property \verb!P! and
a formula \verb!A! in the well-founded part of a relation
\verb!sub!,
if
\verb!sumh_step2_tr P A sub (dta, dtb)!
holds for all derivations \verb!dta! and \verb!dtb!
then
\verb!P A (dtaa, dtbb)! holds for all derivations \verb!dtaa! and \verb!dtbb!:
\end{lemma}
\begin{verbatim}
sumh_step2_tr_lem: "[| ?A : wfp ?sub ;
ALL A dta dtb. sumh_step2_tr ?P A ?sub (dta, dtb) |] ==>
?P ?A (?dtaa, ?dtbb)"
\end{verbatim}
% \subsection{Weakening, Invertibility and Contraction}
% Weakening admissibility, invertibility, and \ctra{} are stated using \texttt{wk\_adm}, \texttt{inv\_rl} and \texttt{ctr\_adm} respectively:
%
% MOST DUPLICATED EARLIER in \S11
% \begin{description}
% \item[\texttt{wk\_adm rls}]~\\
% This states that Weakening is admissible for \texttt{rls}. In particular, for any \texttt{rls}-derivable sequent $S$, the addition of any other sequent $As$ to this is also \texttt{rls}-derivable. Formally, given \texttt{$S \in$ derrec rls \{\}} then \texttt{$S + As \in$ derrec rls \{\}}. This is part of the base formalisation.
% \item[\texttt{inv\_rl rls (ps, c)}]~\\
% Given a rule instance \texttt{(ps, c)}, within a particular calculus \texttt{rls}, \texttt{inv\_rl} holds if whenever \texttt{c} is \texttt{rls}-derivable, then all the premises \texttt{ps} are also \texttt{rls}-derivable.
%
% \item[\texttt{ctr\_adm rls A}]~\\
% Contraction-admissibility is given as a property for a set of rules \texttt{rls}, and a single contraction-formula \texttt{A}: for all sequents \texttt{As}, if the only formula in \texttt{As} is equal to \texttt{A} then for all \texttt{rls}-derivable sequents $S$ where \texttt{As + As} is a sub-sequent of $S$, it holds that $S -$\texttt{As} is also \texttt{rls}-derivable.
% \end{description}
%The rather strange definition for \texttt{ctr\_adm} is used so that
% proving \ctra{} is possible using \texttt{gen\_step\_lem}, while also
% allowing the contraction-formula to be present as part of either the
% antecedent or the succedent.
%It should also be noted that the base formalisation only states
% admissibility for a single contraction-formula. However, a simple
% induction on multisets is sufficient to transform this result into an
% admissibility result for multiple formulae.
%Like \texttt{wk\_adm\_ext\_concl}, the proof of inversion lemmas
% only uses the simpler induction principle \texttt{drs.inductr} from
% Lemma~\ref{inductr:lem}. Proving \texttt{ctr\_adm} uses the induction
% principle \texttt{gen\_step\_lem} as in Lemma~\ref{genstep:lem}, which
% allows a double induction over both height and rank. Like the pen and
% paper proofs, the Isabelle proofs of \texttt{ctr\_adm} within this text
% make heavy use of inversion results.
%It is also interesting to note that when using \ctra{} within a \cuta{}
% proof, instead of picking a number of formula to contract on, it is
% simpler in Isabelle to show that the original sequent is a sub-sequent
% of the result after duplicating all formulae within the desired
% endsequent. As an example, consider a derivation of a sequent $\Gamma_C,
% \Gamma_C, \Gamma \vdash \Delta$ where we wish to use \ctra{} to derive
% $\Gamma_C, \Gamma \vdash \Delta$. In Isabelle, this is done by showing
% that the given sequent $\Gamma_C, \Gamma_C, \Gamma \vdash \Delta$ is a
% sub-sequent of $\Gamma_C, \Gamma_C, \Gamma, \Gamma \vdash \Delta, \Delta$.
% In addition to the \texttt{height\_step2\_tr\_lem} lemma,
% we also use the following induction principle, named \texttt{sum\_step2\_tr}.
% The assumption now is that the inductive property holds for two new
% derivations, where some well-founded measure on the new derivations is
% strictly less than the same measure on the derivations leading to $\MC_l$
% and $\MC_r$. For Cut, this measure will be derivation height. Essentially,
% \cuta{} of new derivations can be assumed, as long as their combined
% height is less than the level of the original cut-sequents $\MC_l$
% and $\MC_r$.
% \begin{definition}[\texttt{sum\_step2\_tr}]~\\
% For a formula $A$, a property $P$,
% a subformula relation \texttt{sub},
% measures on derivation trees \texttt{gsl} and \texttt{gsr},
% %a corresponding set of \texttt{rls}-derivable sequents \texttt{derivs} (e.g. \texttt{derrec rls prems}),
% and explicit derivation trees \texttt{dta} and \texttt{dtb},
%
% \smallskip
%
% \texttt{sum\_step2\_tr $P\ A$ sub gsl gsr (dta, dtb)} means: \\
% if
% \begin{itemize}
% \item forall $B$ such that \texttt{$(B, A) \in$ sub}\\
% the property $P\ B\ (a, b)$ holds for all derivation trees
% \texttt{a} and \texttt{b}, and
% \item for all derivation trees \texttt{dtaa} and \texttt{dtbb} where\\
% \texttt{gsl dtaa + gsr dtbb < gsl dta + gsr dtb}\\
% the property $P\ A (dtaa, dtbb)$ holds
% \end{itemize}
% then $P\ A\ (dta, dtb)$ holds.
% \end{definition}
% Instantiating the measures in \texttt{sum\_step2\_tr} with measures
% of derivation height results in the final principle used to prove \cuta{}:
%
% ALREADY HAVE THIS AS LEMMA 11.5
% \begin{theorem}[\texttt{sumh\_step2\_tr\_lem}]~\\
% Where \texttt{heightDT dt} gives the height of
% an explicit derivation tree \texttt{dt}.
% \begin{description}
% \item[if]
% \texttt{A} is in the well-founded part
% of the subformula relation \texttt{sub}\\
% and for all formulae \texttt{B},
% and derivation trees \texttt{dta} and \texttt{dtb}\\
% the induction step condition
% \texttt{sum\_step2\_tr P B sub heightDT heightDT (dta, dtb)} holds
% \item[then]
% \texttt{P A (dta, dtb)} holds
% \end{description}
% \end{theorem}
\section{Weakening, Contraction and Cut Admissibility for S4}
% \subsection{Motivation andRelated Work}
% \label{background:S4}
There exist both pen and paper \cite{ohnishi1957,Troelstra} and a
formalised proof~\cite{dawson14} of mix-elimination for sequent
calculi describing S4 which include explicit Weakening and Contraction
rules. As stated previously, the inclusion of structural rules is
detrimental for automated reasoning and so provides a practical
motivation for proving admissibility results for a calculus free of
such rules. This is our goal.
Troelstra and Schwichtenberg also state \cute{} for a sequent calculus
G3s that no longer uses explicit structural rules. Unfortunately, the
``proof'' of their theorem only discusses one actual transformation,
and in particular overlooks one non-trivial case -- when Cut is
applied on a formula $\Box A$, with both premises being an instance of
the G3s R$\Box$ rule (shown below). In this case, the deduction cannot
be transformed by simply permuting the Cut, or introducing a new Cut
of smaller rank, on the sequents in the original deduction. Greater
detail is given later in this section.
\begin{center}
\AxiomC{$\Box \Gamma \vdash A, \Delta$}
\LeftLabel{R$\Box$}
\UnaryInfC{$\Gamma', \Box \Gamma \vdash \Box A, \Delta, \Delta'$}
\DisplayProof
\end{center}
Goubault~\cite{Goubault96} acknowledges the problem posed by absorbing
Weakening into the R$\Box$ rule. However, his solutions are
given in the context of typed $\lambda$-calculi for a minimal version
of S4, interpreted as a sequent calculus through a version of the
Curry-Howard correspondence. Based on a proposal from
\cite{bierman96}, Goubault-Larrecq replaces the R$\Box$ rule by a
different rule with multiple premises (for subformula within the
principal formula), along with both re-write and garbage collection
rules for the $\lambda$ terms involved. While this solution could
possibly be extended to sequent calculi, the creation of new premises
and hence branching is detrimental to backward proof search. The
solution presented in this section also has the advantage of being
significantly simpler.
Negri~\cite{Negri05} proves various admissibility theorems for S4, but the calculus involved is labelled. These labels include elements of the Kripke semantics within the calculus, and so the resulting theorems are thus not entirely syntactical proofs. Furthermore, there are rules in the calculus which deal only with reachability between worlds. While perhaps not as inefficient as the standard structural rules, these rules nevertheless do not operate on logical connectives. In particular to S4, from the perspective of automated reasoning, applying all possible instances of the transitivity rule (shown below) or checking whether the transitivity rule has been saturated can be a very time-consuming process.
\begin{center}
\AxiomC{$xRz, xRy, yRz, \Gamma \vdash \Delta$}
\LeftLabel{Transitivity}
\UnaryInfC{$xRy, yRz, \Gamma \vdash \Delta$}
\DisplayProof{}
\medskip
$R$ is the accessibility relation. $x, y, z$ are worlds.
\end{center}
\subsection{Calculus}
The sequent calculus we use for S4 is based on the calculus G3cp, with
the addition of two modal rules. Note that the initial sequents do
not require atoms, and that there are only rules for $\wbx$ formulae
with $\wdi\varphi$ interpreted as $\lnot\wbx\lnot\varphi$. The rules
of the calculus are shown in Figure \ref{S4:rules}. Note that the
clause \verb!boxI! in the inductive definition for \verb!gs4_rls!
applies \verb!extend! only to the conclusion, corresponding to the
appearance of the two sets $\Sigma$ and $\Delta$ in the conclusion of
the rule $S4\wbx$.
\begin{figure}[h!]
\centering
\begin{tabular}{ll}
\textit{Initial Sequents}\\[12px]
\multicolumn{2}{c}{
\AxiomC{}
\LeftLabel{id}
\UnaryInfC{$\Gamma, \varphi \vdash \varphi, \Delta$}
\DisplayProof
}
\\[16px]
\textit{Classical rules}\\[12px]
\AxiomC{$\Gamma, \varphi , \psi \vdash \Delta$}
\LeftLabel{L$\land$}
\UnaryInfC{$\Gamma, \varphi \land \psi \vdash \Delta$}
\DisplayProof
&
\AxiomC{$\Gamma \vdash \varphi, \Delta$}
\AxiomC{$\Gamma \vdash \psi, \Delta$}
\LeftLabel{R$\land$}
\BinaryInfC{$\Gamma \vdash \varphi \land \psi , \Delta$}
\DisplayProof
\\[12px]
\AxiomC{$\Gamma , \varphi \vdash \Delta$}
\AxiomC{$\Gamma , \psi \vdash \Delta$}
\LeftLabel{L$\lor$}
\BinaryInfC{$\Gamma, \varphi \lor \psi \vdash \Delta$}
\DisplayProof
&
\AxiomC{$\Gamma \vdash \varphi , \psi, \Delta$}
\LeftLabel{R$\lor$}
\UnaryInfC{$\Gamma \vdash \varphi \lor \psi, \Delta$}
\DisplayProof
\\[12px]
\AxiomC{$\Gamma \vdash \varphi, \Delta$}
\AxiomC{$\Gamma, \psi \vdash \Delta$}
\LeftLabel{L$\to$}
\BinaryInfC{$\Gamma , \varphi \to \psi \vdash \Delta$}
\DisplayProof
&
\AxiomC{$\Gamma , \varphi \vdash \psi, \Delta$}
\LeftLabel{R$\to$}
\UnaryInfC{$\Gamma \vdash \varphi \to \psi, \Delta$}
\DisplayProof
\\[12px]
\AxiomC{$\Gamma \vdash \varphi, \Delta$}
\LeftLabel{L$\lnot$}
\UnaryInfC{$\Gamma , \lnot \varphi \vdash \Delta$}
\DisplayProof
&
\AxiomC{$\Gamma , \varphi \vdash \Delta $}
\LeftLabel{R$\lnot$}
\UnaryInfC{$\Gamma \vdash \lnot \varphi, \Delta$}
\DisplayProof
\\[16px]
\textit{Modal rules}\\[12px]
\AxiomC{$\Gamma , \varphi, \wbx \varphi \vdash \Delta$}
\LeftLabel{Refl}
\UnaryInfC{$\Gamma , \wbx \varphi \vdash \Delta$}
\DisplayProof
&
\AxiomC{$\Gamma , \wbx \Gamma \vdash \varphi$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx \Gamma \vdash \wbx \varphi, \Delta$}
\DisplayProof
\end{tabular}
\begin{verbatim}
inductive "lksne" intros
axiom : "([], {#A#} |- {#A#}) : lksne"
ilI : "psc : lksil ==> psc : lksne"
irI : "psc : lksir ==> psc : lksne"
inductive "lksss" intros
extI : "psc : lksne ==> pscmap (extend flr) psc : lksss"
inductive "lkrefl" intros
I : "([{#A#} + {#Box A#} |- {#}], {#Box A#} |- {#}) : lkrefl"
inductive "lkbox" intros
I : "([gamma + mset_map Box gamma |- {#A#}],
mset_map Box gamma |- {#Box A#}) : lkbox"
inductive "gs4_rls" intros
lksI : "psc : lksss ==> psc : gs4_rls"
reflI : "psc : lkrefl ==> pscmap (extend flr) psc : gs4_rls"
(* Note Box rule allows extra formulae in conclusion only *)
boxI : "(prem, conc) : lkbox ==> (prem, extend flr conc) : gs4_rls"
\end{verbatim}
\caption{\label{S4:rules}Sequent calculus GS4 for S4.}
\end{figure}
In Isabelle, the calculus is encoded in a modular manner. With the
overall calculus, called \texttt{gs4\_rls}, built up from separate
declarations of the id rule, the classical rules acting on antecedents
and succedents, and the two modal rules.
\subsection{Weakening for S4}
\begin{definition}
For all sets \verb!A! and all unary predicates \verb!P!, the property
\verb!Ball A P! holds iff every member of \verb!A! satisfies \verb!P!:
\end{definition}
\begin{verbatim}
Ball_def: "Ball ?A ?P == ALL x. x : ?A --> ?P x"
\end{verbatim}
\begin{definition}
A set of rules \verb!rls! satisfies \verb!ext_concl! iff: for every
list of premises \verb!ps! and conclusion \verb!c! that form an
extended rule instance of some rule in \verb!rls!, and all possible
sequents \verb!UV!, there exists a list of premises \verb!ps'! such
that the premises \verb!ps'! and the extended conclusion \verb!c + UV!
also form an instance of some rule in \verb!rls! and
for every premise \verb!p! from \verb!ps! there is a corresponding
premise \verb!p'! in \verb!ps'! such that \verb!p'! is either \verb!p!
itself or is an extension of \verb!p!:
\end{definition}
\begin{verbatim}
ext_concl_def: "ext_concl ?rls ==
ALL (ps, c):?rls. ALL UV. EX ps'.
(ps', c + UV) : ?rls & (ps, ps') : allrel {(p, p'). p <= p'}"
\end{verbatim}
\begin{lemma} \label{l-ext-concl-wk}
If a set of rules \verb!rls! obeys \verb!ext_concl! then \verb!rls!
admits weakening:
\end{lemma}
\begin{verbatim}
wk_adm_ext_concl: "ext_concl ?rls ==> wk_adm ?rls"
\end{verbatim}
\begin{lemma}
The set of rule \verb!gs4_rls! satisfies \verb!ext_concl!.
\end{lemma}
\begin{verbatim}
gs4_ext_concl: "ext_concl gs4_rls"
\end{verbatim}
\begin{lemma}
The rules of S4 satisfy weakening admissibility.
\end{lemma}
\begin{verbatim}
gs4_wk_adm: "wk_adm gs4_rls"
\end{verbatim}
\begin{proof}
\marginpar{MOVE TO proof of Lemma 12.1}
The lemma \verb!wk_adm_ext_concl! is simple enough to prove simply
by the induction principle shown above for \verb!derrec!. Use of
lemmas like \verb!gen_step_lem! is really only for the purpose of
breaking up the proofs, so that various different cases of
\verb!gen_step! (ie various final rules of the derivation) can be
put into separate lemmas.
\end{proof}
\begin{theorem}[weakening for GS4]
\marginpar{Same as Lemma 11.4. Have I misunderstood something? DELETE}
Weakening is admissible for GS4:
\\
\verb!wk_adm gs4_rls!
\end{theorem}
\begin{proof}
This follows from the fact that all rules in \verb!gs4_rls! allow
arbitrary contexts in their conclusion. That is, from the fact that
\verb!gs4_rls! satisfies \verb!ext_concl!.
\end{proof}
\subsection{Invertibility for S4}\label{s-s4-inv}
We now describe how we captured the traditional proof of
invertibility.
Suppose that we are given a calculus consisting of the rule set
\verb!drls! and suppose that we want to reason about the derivability
predicate \verb!derrec! defined earlier. Let \verb!derivs! be the set
\verb!derrec drls {}! of all sequents that are derivable from the
empty set of leaves using the rules of \verb!drls!. Suppose that we
wish to prove that every rule in \verb!irls! is invertible wrt
\verb!drls! (where \verb!irls! is usually a subset of \verb!drls!).
Without describing it in detail, the function
\verb!invs_of irls c! returns the set of sequents obtainable by
applying each rule of \verb!irls! to the sequent \verb!c!
\textit{backwards} once. That is, a sequent \verb!seq! is in
\verb!invs_of irls c! if applying some rule $\rho$ of \verb!irls!
to \verb!c! backwards, once, will give \verb!seq! as one of
the premises of $\rho$.
To prove that a rule \verb!(ps, concl)! is invertible wrt \verb!drls!
requires us to prove that each sequent \verb!seq! from the list
\verb!ps! of premises is in \verb!derivs! if \verb!concl! is in
\verb!derivs!. To prove that each rule in a set of rules \verb!irls!
is invertible wrt \verb!drls! requires us to prove that the above
property holds for each rule \verb!(ps, concl)! from \verb!irls!: that
is, \verb!invs_of irls concl <= derivs! where \verb!<=! encodes the
subset relation.
Traditional proofs of invertibility proceed by an induction on
the structure of a given derivation of a sequent
\verb!concl! from \verb!derivs!. Assuming that the final rule in this
derivation is \verb!(ps, concl)!, the induction hypothesis is to
assume that the invertibility lemma holds for each premise in
\verb!ps!. That is, we assume that every sequent \verb!seq! obtained
by applying any rule from \verb!irls! \textit{backwards}, once, to any
premise \verb!p! in \verb!ps! is itself in \verb!derivs!:
\begin{verbatim}
ALL p:set ps. invs_of irls p <= derivs
\end{verbatim}
Use of the induction hypothesis stated above can then be encoded in
\texttt{inv\_step}.
Let an ``\texttt{irls}-inverse'' of a sequent $s$ be a sequent $s'$
obtained from $s$ by applying a rule from \verb!irls! backwards once.
\begin{definition}[\texttt{inv\_step}]
Then for a given set \verb!derivs! of derivable sequents,
for a rule set \verb!irls!,
and for every rule instance \verb!(ps, concl)!,
the property \verb!inv_step derivs irls (ps, concl)! holds iff:
if, assuming that every premise in \verb!ps! is in \verb!derivs!,
every ``\texttt{irls}-invert'' of premises in \verb!ps! is in \verb!derivs!,
then every ``\texttt{irls}-invert'' of the conclusion \texttt{concl}
is in \verb!derivs!.
\end{definition}
\begin{verbatim}
inv_step.simps =
"inv_step ?derivs ?irls (?ps, ?concl) =
(set ?ps <= ?derivs -->
(ALL p:set ?ps. invs_of ?irls p <= ?derivs) -->
invs_of ?irls ?concl <= ?derivs)"
\end{verbatim}
This is the key result for doing invertibility by stating various cases of the induction step as separate lemmas.
The expression \verb!UNION (set ?ps) (invs_of ?irls)! represents the
set $X$ of all sequents which can be obtained by applying some rule from
\verb!irls! backwards once to every sequent \verb!p! from a list of
sequents \verb!ps! viewed as a set:
\[
X := \bigcup_{\verb!p!~\in~\verb!set ps!} \verb!(invs_of ?irls p)!
\]
Then, the expression
\verb!(set ?ps Un UNION (set ?ps) (invs_of ?irls))!
represents the union of $X$ and the list of sequents \verb!ps! treated
as a set: $\verb!(set ps)! \cup X$.
The property \verb!inv_stepm! is weaker than \verb!inv_step! but is
monotonic in its first argument, which makes reusing lemmas such as
\verb!lks_inv_stepm! possible as follows.
\begin{definition}
For all rule sets \verb!rls!,
for all rule sets \verb!irls!,
for all rules \verb!(ps, concl)!,
\verb!inv_stepm drls irls (ps, concl)!
holds iff:
\texttt{irls}-inverses of \verb!concl!
are derivable using \verb!derrec! from
\verb!(set ps)! and the \texttt{irls}-inverses
of every \verb!p! from \verb!set ps!:
\end{definition}
\begin{verbatim}
inv_stepm.simps ;
val it =
"inv_stepm ?drls ?irls (?ps, ?concl) =
(invs_of ?irls ?concl
<= derrec ?drls (set ?ps Un UNION (set ?ps) (invs_of ?irls)))"
\end{verbatim}
\begin{lemma}\label{lemma:inv-stepm-monotonic}
\verb!inv_stepm! is monotonic in its first argument:
\end{lemma}
\begin{verbatim}
inv_step_mono:
"[| inv_stepm ?drlsa ?irls ?psc ; ?drlsa <= ?drlsb |]
==> inv_stepm ?drlsb ?irls ?psc"
\end{verbatim}
\begin{lemma}\label{lemma:inv-step-from-inv-stepm}
For every set \verb!drls! of rules and every
set \verb!prems! of sequents, the function
\verb!(derrec drls prems)! returns the set of sequents derivable
from \verb!prems! using the rules of \verb!drls!. Let us call this
set of derivable sequents \verb!derivs!.
For every set \verb!drls! of rules used for derivations,
for every rule set \verb!irls!,
for every rule \verb!psc!,
if
\verb!inv_stepm drls irls psc!
holds then do does
\verb!inv_step derivs irls psc!
for any set of leaf premises \verb!prems!:
\end{lemma}
\begin{verbatim}
inv_step_m:
val it =
"inv_stepm ?drls ?irls ?psc
==> inv_step (derrec ?drls ?prems) ?irls ?psc"
\end{verbatim}
\begin{lemma}[\texttt{gen\_inv\_by\_step}]\label{lemma:inv-from-inv-step}
For every rule set \verb!rls! which is used to construct a set
\verb!derrec rls {}! of derivations from the empty set of leaves
using \verb!derrec!, for every rule set \verb!irls!, every rule
\verb!psc! from \verb!irls! is invertible wrt \verb!rls! if every
rule instance \verb!(ps, concl)! from \verb!rls! obeys
\verb!inv_step (derrec rls {}) irls (ps, concl)!:
\end{lemma}
\begin{verbatim}
gen_inv_by_step:
"[| Ball ?rls (inv_step (derrec ?rls {}) ?irls) ; ?psc : ?irls |]
==> inv_rl ?rls ?psc"
\end{verbatim}
\begin{lemma}
Every instance of the rule Refl, extended with
arbitrary contexts, is invertible in the rule set \verb!gs4_rls!:
\end{lemma}
\begin{verbatim}
Ball (extrs lkrefl) (inv_rl gs4_rls)
\end{verbatim}
\begin{proof}
Suppose that $\Gamma , \wbx \varphi \vdash \Delta$ is derivable.
We can show that the premise
$\Gamma , \varphi, \wbx \varphi \vdash \Delta$ is derivable by
applying weakening, which has already been shown to be admissible in
\verb!gs4_rls!.
\end{proof}
\begin{lemma}
Every instance of the rule set \verb!lksss! (of classical
propositional logic) is invertible in the rule set
\verb!gs4_rls!:
\end{lemma}
\begin{verbatim}
Ball lksss (inv_rl gs4_rls)
\end{verbatim}
\begin{proof}
By Lemma~\ref{lemma:inv-from-inv-step}, it suffices to prove
\verb!(inv_step (derrec gs4_rls {}) lksss) psc!
for every rule \verb!psc! from \verb!gs4_rls!.
By Lemma~\ref{lemma:inv-step-from-inv-stepm}, it suffices to prove
\verb!inv_stepm gs4_rls lksss psc!
for every rule \verb!psc! from \verb!gs4_rls!:
%
We proceed by cases on the rule \verb!psc! from \verb!gs4_rls!,
noting that \verb!lksss == extrs lksne!: the rule set \verb!lksne!
extended with arbitrary contexts.
Where the rule \verb!psc! is Refl:
\begin{verbatim}
"?psc : extrs lkrefl ==> inv_stepm gs4_rls (extrs lksne) ?psc"
\end{verbatim}
Where the rule \verb!psc! is a classical rule, we first prove that
the set of classical rules is invertible wrt itself:
\begin{verbatim}
"?psc : extrs lksne ==> inv_stepm (extrs lksne) (extrs lksne) ?psc"
\end{verbatim}
Since the rules \verb!lksss! are a subset of the rules
\verb!gs4_rls!,
we can use (the monotonicity) Lemma~\ref{lemma:inv-stepm-monotonic}
to obtain
\begin{verbatim}
"?psc : extrs lksne ==> inv_stepm gs4_rls (extrs lksne) ?psc"
\end{verbatim}
Where last rule is $S4\wbx$ ( with arbitrary contexts in conclusion
only), to make weakening admissible, we prove a very general result.
If the rule set \verb!rls! contains exactly one rule
\verb!extcs {(?ps, ?c)}! which is the rule (skeleton) \verb!(ps, c)!
with only the conclusion extended by an arbitrary context,
then \verb!inv_stepm rls (extrs {(ips, ic)}) ?rl! holds for any
rule \verb!(ips, ic)! extended with arbitrary contexts if
the (skeletons of the) conclusion \verb!ic! and the
the (skeletons of the) conclusion \verb!c! are disjoint:
\begin{verbatim}
inv_stepm_disj_cs:
"[| seq_meet ?c ?ic = 0; extcs {(?ps, ?c)} = ?rls; ?rl : ?rls |]
==> inv_stepm ?rl (extrs {(?ips, ?ic)}) ?rl"
\end{verbatim}
In particular, we can put \verb!extcs {(?ps, ?c)}! to be the rule
$S4\wbx$ and put \verb!(extrs {(?ips, ?ic)})! to be any rule from
\verb!lksss! since the skeletons of the conclusions of the
\verb!lksss! rules contain only the principal formula of the
respective rule and none of these is a $\wbx$-formula.
\end{proof}
\begin{theorem}[\texttt{inv\_rl\_gs4\_refl} and \texttt{inv\_rl\_gs4\_lks}]
The Refl (\texttt{lkrefl}) rule and all Classical (\texttt{lksss}) rules are invertible within \texttt{gs4\_rls}.
\end{theorem}
\begin{proof}
TODO: remove this? Takes up too much space.
As an example, consider invertibility for the R$\lor$ rule. The proof
proceeds by an induction on height.\marginpar{Which of the gen-step
lemmas does it actually use ? It uses \texttt{gen\_inv\_by\_step}}
\begin{description}
\item[Case 1. Axiom]~\\
If $\Gamma \vdash \varphi \lor \psi, \Delta$ is an axiom, and $\varphi \lor \psi$ is principal, then $\Gamma = \Gamma', \varphi \lor \psi$. The derivation for $\Gamma \vdash \varphi, \phi, \Delta$ is then:
\begin{center}
\AxiomC{}
\LeftLabel{id}
\UnaryInfC{$\Gamma', \varphi \vdash \varphi, \phi, \Delta$}
\AxiomC{}
\LeftLabel{id}
\UnaryInfC{$\Gamma', \psi \vdash \varphi, \phi, \Delta$}
\LeftLabel{L$\lor$}
\BinaryInfC{$\Gamma', \varphi \lor \psi \vdash \varphi, \phi, \Delta$}
\DisplayProof{}
\end{center}
If $\varphi \lor \psi$ is parametric in the axiom, then $\Gamma \vdash \Delta$ is an axiom, and so is $\Gamma \vdash \varphi, \phi, \Delta$.
\item[Case 2. Principal]~\\
If $\Gamma \vdash \varphi \lor \psi, \Delta$ is not an axiom, but $\varphi \lor \psi$ is principal, then R$\lor$ must have been the last rule applied. Invertibility follows immediately from the premises of the R$\lor$ rule.
\item[Case 3. Parametric]~\\
If $\Gamma \vdash \varphi \lor \psi, \Delta$ is not an axiom, and $\varphi \lor \psi$ is parametric, then an application of a new instance of that last rule (perhaps using the induction hypothesis) obtains the necessary endsequent. This is because all rules allow arbitrary contexts in their conclusion (and premises when the premises contain context). To illustrate, consider the two cases when the last rule used to originally derive $\Gamma \vdash \varphi \lor \psi, \Delta$ is either the Refl or the S4$\wbx$ rule.
\begin{itemize}
\item
If the last rule was Refl then $\Gamma = \Gamma', \wbx A$ and the original derivation is:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma', A, \wbx A \vdash \Delta, \varphi \lor \psi$}
\LeftLabel{Refl}
\UnaryInfC{$\Gamma', \wbx A \vdash \Delta, \varphi \lor \psi$}
\DisplayProof{}
\end{center}
Applying the inductive hypothesis on the premises gives a derivation of $\Gamma', A, \wbx A \vdash \Delta, \varphi, \psi$. Apply Refl to this gives the required $\Gamma', \wbx A \vdash \varphi, \phi, \Delta$.
\item
If the last rule was S4$\wbx$ then $\Gamma = \Sigma, \wbx \Gamma'$ and $\Delta = \wbx A, \Delta'$ and the original derivation looks like:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma', \wbx \Gamma' \vdash A$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx \Gamma' \vdash \wbx A, \Delta', \varphi \lor \psi$}
\DisplayProof{}
\end{center}
To derive $\Gamma \vdash \varphi, \psi, \Delta$, simply apply a new instance of S4$\wbx$ to the original premises, this time with $\varphi, \psi$ as the context instead of $\varphi \lor \psi$:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma', \wbx \Gamma' \vdash A$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx \Gamma' \vdash \wbx A, \Delta', \varphi, \psi$}
\DisplayProof{}
\end{center}
\end{itemize}
\end{description}
\end{proof}
\begin{theorem}[\texttt{gs4\_ctr\_adm}]
Contraction is admissible for the calculus \texttt{gs4\_rls}.
\end{theorem}
\begin{proof}
The cases for the G3cp
\marginpar{what is G3cp?}
and Refl rules are handled in the standard manner as in
the literature (see \cite{Troelstra} and \cite{Negri01}) using the invertibility results above.
The formalisation performs the necessary transformations using the induction principle \texttt{gen\_step\_lem} of Theorem~\ref{genstep:lem}.
\marginpar{actually uses theorem \texttt{gen\_ctr\_adm\_step}
which involves the predicate \texttt{ctr\_adm\_step},
but these are simple instantiations of \texttt{gen\_step} and
\texttt{gen\_step\_lem}}
When the rule above the contraction is an instance of the S4$\wbx$ rule, there are two possible cases. Either one or both copies of the contraction-formula exist within the context of the S4$\wbx$ rule, or both copies are principal.
In the first case, deleting one copy still leaves an instance of the
rule. That is, if the contraction-formula is $A$, with $A$ in the
succedent, then the original rule instance is as shown below where
either $\wbx \varphi = A$ or $A \in \Delta$:
\begin{center}
\AxiomC{$\Gamma, \wbx \Gamma \vdash \varphi$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx \Gamma \vdash \wbx \varphi, A, \Delta$}
\DisplayProof{}
\end{center}
Applying the S4$\wbx$ rule without introducing the shown second copy
of $A$ in the conclusion above gives a proof of $\Sigma, \wbx \Gamma
\vdash \wbx \varphi, \Delta$ as required since an occurrence of $A$ is
still in the succedent as $\wbx \varphi = A$ or $A \in
\Delta$. Similarly, if $A$ is in the context $\Sigma$ the new
S4$\wbx$ rule instance is then:
\marginpar{Was just $\varphi$ in succedent of conclusion. (DON'T UNDERSTAND!)}
\begin{center}
\AxiomC{$\Gamma, \wbx \Gamma \vdash \varphi$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma - A, \wbx \Gamma \vdash \wbx\varphi, A, \Delta$}
\DisplayProof{}
\end{center}
The harder case occurs when both instances of the contraction-formula
$A$ are principal. Due to the nature of the S4$\wbx$ rule this
requires $A$ to occur in the antecedent only, as there cannot be two
principal formulae in the succedent. As only boxed formulae are
principal, $A$ has form $\wbx B$. The original rule instance is thus
represented by:
\marginpar{Was just $\varphi$ in succedent of conclusion.}
\begin{center}
\AxiomC{$B, B, \wbx B, \wbx B,\Gamma, \wbx \Gamma \vdash \varphi$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx B, \wbx B, \wbx \Gamma \vdash \wbx\varphi, \Delta$}
\DisplayProof{}
\end{center}
The copies of $\wbx B$ and $B$ can be contracted upon, first using the induction hypothesis on height, and then on rank.
\marginpar{Doesn't need height, just induction on the derivation, ie,
assuming ctr-adm applies to premises of last rule.
Given the discussion in \S11 we should be precise on this}
The S4$\wbx$ rule can then be applied to give the required conclusion.\marginpar{Was just $\varphi$ in succedent of conclusion.}
\begin{center}
\AxiomC{$B, \wbx B,\Gamma, \wbx \Gamma \vdash \varphi$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx B, \wbx \Gamma \vdash \wbx\varphi, \Delta$}
\DisplayProof{}
\end{center}
In the Isabelle proof, this step is unfortunately rather more tedious. A significant number of proof steps in the formalisation are dedicated to manipulating the ordering of formulae to convince the proof assistant that the S4$\wbx$ can be applied after applying the induction hypotheses, and that the resulting sequent is indeed what is required.
\end{proof}
\begin{theorem}[\texttt{gs4\_cas}]
Cut is admissible in the calculus \texttt{gs4\_rls}.
\end{theorem}
\begin{proof}
The two most difficult cases to consider correspond to when the cut-formula is principal below an application of the S4$\wbx$ rule on the left, and also principal in either the Refl or the S4$\wbx$ rule on the right. As these are all modal rules, the Cut in question must be on a boxed formula, $\wbx A$.
%%%%%%%%%% S4 left, refl right %%%%%%%%%%
In the former case, the original Cut has form:
\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx \Gamma_L \vdash \Delta_L, \wbx A$}
\AxiomC{$\Pi_r$}
\noLine
\UnaryInfC{$ A, \wbx A, \Gamma_R \vdash \Delta_R$}
\LeftLabel{Refl}
\UnaryInfC{$\wbx A, \Gamma_R \vdash \Delta_R$}
\LeftLabel{Cut on $\wbx A$}
\BinaryInfC{$\Sigma, \wbx \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
\DisplayProof
\end{center}
This is transformed as follows:
\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma, \wbx \Gamma_L \vdash \Delta_L, \wbx A$}
\AxiomC{$\Pi_r$}
\noLine
\UnaryInfC{$A, \wbx A, \Gamma_R \vdash \Delta_R$}
\RightLabel{Cut on $\wbx A$}
\BinaryInfC{$A, \Sigma, \wbx \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
\RightLabel{Cut on $A$}
\BinaryInfC{$\Sigma, \Gamma_L, \wbx \Gamma_L, \wbx \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
\dashedLine
\RightLabel{Contraction-admissibility}
\UnaryInfC{$\Sigma, \Gamma_L, \wbx \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
\LeftLabel{Refl}
\UnaryInfC{$\Sigma, \wbx \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
\DisplayProof
\end{center}
Importantly, the new Cut on $\wbx A$ has lower level, and the Cut on $A$ is of smaller rank. Thus both can be eliminated by the induction hypotheses.
%%%%%%%%%% S4 both sides %%%%%%%%%%
For the latter case, when S4$\wbx$ is principal on both sides, the original Cut has form:
\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma_L, \wbx \Gamma_L \vdash \Delta_L, \wbx A$}
\AxiomC{$\Pi_r$}
\noLine
\UnaryInfC{$A, \wbx A, \Gamma_R, \wbx \Gamma_R \vdash B$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\wbx A, \Sigma_R, \wbx \Gamma_R \vdash \wbx B, \Delta_R$}
\LeftLabel{Cut on $\wbx A$}
\BinaryInfC{$\Sigma_L, \Sigma_R, \wbx \Gamma_L, \wbx \Gamma_R \vdash \wbx B, \Delta_L, \Delta_R$}
\DisplayProof
\end{center}
The normal process of reducing Cut level would apply Cut on the left cut-sequent and the premise of the right cut-sequent, as follows:
\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma_L, \wbx \Gamma_L \vdash \Delta_L, \wbx A$}
\AxiomC{$\Pi_r$}
\noLine
\UnaryInfC{$A, \wbx A, \Gamma_R, \wbx \Gamma_R \vdash B$}
\LeftLabel{Cut on $\wbx A$}
\BinaryInfC{$A, \Sigma_L, \wbx \Gamma_L, \Gamma_R, \wbx \Gamma_R \vdash B, \Delta_L$}
\DisplayProof
\end{center}
Unfortunately, this results in a deduction where we can no longer recover the
$\wbx B$ present in the conclusion of the original Cut. The nature of the
calculus and the S4$\wbx$ rule means that new box formulae cannot be introduced
in any succedent which contains some context $\Delta$ (or where there are
additional formula $\Sigma$ in the antecedent). As stated earlier, this case is
omitted in the \cute{} theorem of Troesltra and Schwichtenberg~\cite{Troelstra}.
To overcome this issue, without introducing the complications and new
branching rule in the solution of Goubault~\cite{Goubault96}, we
modify the original derivation of the left premise, to produce one of
equal height upon which we can still apply the induction hypothesis on
level. The new application of the S4$\wbx$ rule differs from the
original by simply not adding any context in the conclusion. Formally,
the $\Sigma$ and $\Delta$ of the generic S4$\wbx$ rule in Figure
\ref{S4:rules} are $\emptyset$ in the new S4$\wbx$ instance below:
\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L \vdash A$}
\LeftLabel{S4$\wbx$ (new)}
\UnaryInfC{$\wbx \Gamma_L \vdash \wbx A$}
\AxiomC{$\Pi_r$}
\noLine
\UnaryInfC{$A, \wbx A, \Gamma_R, \wbx \Gamma_R \vdash B$}
\RightLabel{Cut on $\wbx A$}
\BinaryInfC{$A, \wbx \Gamma_L, \Gamma_R, \wbx \Gamma_R \vdash B$}
\RightLabel{Cut on $A$}
\BinaryInfC{$\Gamma_L, \wbx \Gamma_L, \wbx \Gamma_L, \Gamma_R, \wbx \Gamma_R \vdash B$}
\dashedLine
\RightLabel{Contraction-admissibility}
\UnaryInfC{$\Gamma_L, \wbx \Gamma_L, \Gamma_R, \wbx \Gamma_R \vdash B$}
\LeftLabel{S4$\wbx$}
\UnaryInfC{$\Sigma_L, \Sigma_R, \wbx \Gamma_L, \wbx \Gamma_R \vdash \wbx B, \Delta_L, \Delta_R$}
\DisplayProof
\end{center}
In the formalised proof, this instance is the only case where the
inductive principle \texttt{sumh\_step2\_tr\_lem} is actually
\marginpar{Surely we have to use the same principle throughout?
In all the other cases \texttt{gen\_step2sr\_lem} would have sufficed.
So in fact all the other cases prove \texttt{gen\_step2sr}, and use
the theorem \texttt{gs2\_car\_sumhs\_tr}
}
required. As the combined height of the derivations leading to $\wbx
\Gamma_L \vdash \wbx A$ and $A, \wbx A, \Gamma_R, \wbx \Gamma_R \vdash
B$ is lower than the level of the original Cut, the induction
hypothesis on level can be applied.
\end{proof}
\begin{verbatim}
THEOREM referred to in marginal note
(combines Lemmas 11.3 and 11.4)
gs2_car_sumhs_tr:
"gen_step2sr (prop2 car ?rls) ?A ?sub ?rls (botRule ?dta, botRule ?dtb)
==> sumh_step2_tr (prop2 casdt ?rls) ?A ?sub (?dta, ?dtb)"
\end{verbatim}
\section{Weakening, Contraction and Cut Admissibility for S4.3}
There exists a syntactic pen and paper proof for S4.3 in the
literature~\cite{Shimura91}, however the calculus involved contains
Weakening and Contraction as explicit rules, and mix-elimination is
proved rather than cut. There also exist published semantic proofs of
closure under Cut for both sequent and hypersequent calculi for
S4.3~\cite{gore94,indrzejczak12}. But, there are no syntactic pen and
paper proofs of \cuta{} in the literature, nor any machine checked
proofs.
To our knowledge, there are also no published papers for S4.3
explicitly providing a sequent calculus containing only logical
rules. The labelled calculi of Negri~\cite{Negri05} and
Castellini~\cite{castellini06} are perhaps the closest representatives
in the literature. As noted previously, while these calculi do not use
Weakening or Contraction, they explicitly include the semantics of the
logic in the calculi, along with corresponding operations on world
accessibility rather than logical operators.
\subsection{Calculus}
The rules of the sequent calculus for S4.3 are listed in
Figure~\ref{S43:rules}. The calculus is based on the structural
version of Gor\'e~\cite{gore94}, but with Weakening absorbed into the
modal rules. Note, in the S4.3$\Box$ rule of Figure~\ref{S43:rules},
that $\Boxes = \{\varphi_1, \dots, \varphi_n \}$ and $\Boxesi{i} =
\{\varphi_1, \dots, \varphi_{i-1}, \varphi_{i+1}, \dots, \varphi_n \}$
for $1 \leq i \leq n$.
\begin{figure}[ht]
\centering
\begin{tabular}{ll}
\textit{Axioms}\\[12px]
\AxiomC{}
\LeftLabel{id}
\UnaryInfC{$\Gamma, \varphi \vdash \varphi, \Delta$}
\DisplayProof
\\[16px]
\textit{Classical rules}\\[12px]
\AxiomC{$\Gamma, \varphi , \psi \vdash \Delta$}
\LeftLabel{L$\land$}
\UnaryInfC{$\Gamma, \varphi \land \psi \vdash \Delta$}
\DisplayProof
&
\AxiomC{$\Gamma \vdash \varphi, \Delta$}
\AxiomC{$\Gamma \vdash \psi, \Delta$}
\LeftLabel{R$\land$}
\BinaryInfC{$\Gamma \vdash \varphi \land \psi , \Delta$}
\DisplayProof
\\[12px]
\AxiomC{$\Gamma , \varphi \vdash \Delta$}
\AxiomC{$\Gamma , \psi \vdash \Delta$}
\LeftLabel{L$\lor$}
\BinaryInfC{$\Gamma, \varphi \lor \psi \vdash \Delta$}
\DisplayProof
&
\AxiomC{$\Gamma \vdash \varphi , \psi, \Delta$}
\LeftLabel{R$\lor$}
\UnaryInfC{$\Gamma \vdash \varphi \lor \psi, \Delta$}
\DisplayProof
\\[12px]
\AxiomC{$\Gamma \vdash \varphi, \Delta$}
\AxiomC{$\Gamma, \psi \vdash \Delta$}
\LeftLabel{L$\to$}
\BinaryInfC{$\Gamma , \varphi \to \psi \vdash \Delta$}
\DisplayProof
&
\AxiomC{$\Gamma , \varphi \vdash \psi, \Delta$}
\LeftLabel{R$\to$}
\UnaryInfC{$\Gamma \vdash \varphi \to \psi, \Delta$}
\DisplayProof
\\[12px]
\AxiomC{$\Gamma \vdash \varphi, \Delta$}
\LeftLabel{L$\lnot$}
\UnaryInfC{$\Gamma , \lnot \varphi \vdash \Delta$}
\DisplayProof
&
\AxiomC{$\Gamma , \varphi \vdash \Delta $}
\LeftLabel{R$\lnot$}
\UnaryInfC{$\Gamma \vdash \lnot \varphi, \Delta$}
\DisplayProof
\\[16px]
\textit{Modal rules}\\[12px]
\AxiomC{$\Gamma , \varphi, \Box \varphi \vdash \Delta$}
\LeftLabel{Refl}
\UnaryInfC{$\Gamma , \Box \varphi \vdash \Delta$}
\DisplayProof
\\[16px]
\end{tabular}
\AxiomC{$\Gamma , \Box \Gamma \vdash \varphi_1, \Box \Boxesi{1} \; \cdots \;
\Gamma , \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i} \; \cdots \;
\Gamma , \Box \Gamma \vdash \varphi_n, \Box \Boxesi{n}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof
\caption{\label{S43:rules}Sequent calculus for S4.3.}
\end{figure}
From the perspective of backward proof search, the S4.3$\Box$ rule can
be thought of as producing a new premise for all boxed formula in its
conclusion, each of these formula being un-boxed separately in its own
premise. Thus the general statement of the rule contains an
indeterminate number of premises, one is necessary for each $\varphi_i
\in \Boxes$. For the sake of simplicity and clarity, at times only one
of these premises will be shown as a representative for all $n$
premises. That is, the rule will be represented in the following form
shown below at left:
\[
\AxiomC{$\Gamma , \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof
\qquad
\AxiomC{$\Gamma , \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\RightLabel{$\forall \psi. \wbx\psi \not\in \Sigma \cup \Delta$}
\UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof
\]
There are two different versions of the S4.3$\Box$ rule. Either the
context ($\Sigma$ and $\Delta$) can contain any formulae, as shown
above left, or they cannot include top-level boxed-formulae, as shown
above right. In the latter case, the $\Box \Gamma$ and $\Box \Boxes$
in the conclusion of the S4.3$\Box$ rule must correspond to exactly
all the top-level boxed formulae within that sequent. The two versions
of the calculus are in fact equivalent, following a proof of the
admissibility of Weakening for the latter; however, for efficient
backward proof search, the version above right is preferred as it is
invertible and hence does not require backtracking during proof search.
Henceforth, $\Sigma$ and $\Delta$ within the S4.3$\Box$ rule will be
restricted from containing the $\Box$ operator at the top-level. In
Isabelle, this is implemented by creating a new type of formula, based
on the default formula type. HOL's \texttt{typedef} allows a concise
method of declaring new types as a subset of an existing type:
\begin{verbatim}
typedef nboxfml =
"{f::formula. ALL (a::formula). f ~= FC ''Box'' [a]}"
\end{verbatim}
The Isabelle formalisation of the overall calculus is based on the calculus for S4 given in Figure~\ref{S4:isabellerules}. The only change is in the S4.3$\Box$ rule, which requires the mapping function \texttt{nboxseq} to create a new premise for each individual boxed formula in the succedent. The code for this is given in Figure~\ref{S43:isabellerules}.
%\lstset{basicstyle=\ttfamily\footnotesize}
\lstset{basicstyle=\ttfamily}
\begin{figure}[h!]
\begin{lstlisting}
(* Functions to unbox one formula for each premise *)
consts
ithprem :: "formula multiset => formula list => formula
=> formula sequent"
nprems :: "formula multiset => formula list
=> formula sequent list"
(* The boxes in the succedent are treated as a list As.
"ms_of_list (remove1 Ai As)" is the multiset consisting of
all elements in "As", with one copy of "Ai" removed. *)
defs
ithprem_def : "ithprem Gamma As Ai ==
mset_map Box Gamma + Gamma |-
{#Ai#} + mset_map Box (ms_of_list (remove1 Ai As))"
nprems_def : "nprems Gamma As == map (ithprem Gamma As) As"
consts
gs43_rls :: "formula sequent psc set"
s43box :: "formula sequent psc set"
(* The S4.3 box rule *)
inductive "s43box" intros
I : "(nprems gamma As, mset_map Box gamma |-
mset_map Box (ms_of_list As)) : s43box"
(* The S4.3 calculus as an extension of the LK calculus *)
inductive "gs43_rls" intros
lksI : "psc : lksss ==> psc : gs43_rls"
reflI : "psc : lkrefl ==>
pscmap (extend flr) psc : gs43_rls"
(* boxI allows extra formulae in conclusion only *)
boxI : "(p, c) : lkbox ==>
(p, extend (nboxseq flr) c) : gs43_rls"
\end{lstlisting}
\caption{\label{S43:isabellerules}S4.3 calculus as encoded in Isabelle}
\end{figure}
\lstset{basicstyle=\ttfamily\small}
\subsection{Weakening}
As the S4.3$\Box$ rule does not allow arbitrary contexts, \weaka{} must be proved by induction, in this case on both height and rank. In order to simplify the case for the S4.3$\Box$ rule and its multiple premises, \weaka{} is proven for the antecedent and succedent separately, and only considering a single formula at a time. The Isabelle encodings for these properties are given below. The induction itself proceeds on the height of the derivation, as well as a sub-induction on the rank of the formula $A$ being inserted.
\begin{description}
\item[\texttt{wk\_adm\_single\_antec rls}]~\\
For any \texttt{rls}-derivable sequent $S$, and any single formulae $A$,\\ if \texttt{$S \in$ derrec rls \{\}} then \texttt{$S + $(\{\#A\#\} |- \{\#\}) $\in$ derrec rls \{\}}.
\item[\texttt{wk\_adm\_single\_succ rls}]~\\
For any \texttt{rls}-derivable sequent $S$, and any single formulae $A$,\\ if \texttt{$S \in$ derrec rls \{\}} then \texttt{$S + $(\{\#\} |- \{\#A\#\}) $\in$ derrec rls \{\}}.
\end{description}
\begin{lemma}[\texttt{wk\_adm\_sides}]
If \texttt{wk\_adm\_single\_antec} and \texttt{wk\_adm\_single\_succ} both hold for a set of rules \texttt{rls}, then so does \texttt{wk\_adm}.
\end{lemma}
\begin{proof}
By multiset induction, repeatedly applying the results for single formulae.
\end{proof}
\begin{theorem}[\texttt{gs43\_wk\_adm}]
Weakening is admissible for the calculus \texttt{gs43\_rls}.
\end{theorem}
\begin{proof}
In the case of the S4.3$\Box$ rule, if $A$ is not boxed, then it is
allowed to be contained in the context of the rule's conclusion. The
derivability of the original premises, followed by an application of
a new S4.3$\Box$ rule including $A$ as part of its context, then
gives the required sequent. The difficulty arises when $A$ is a
boxed formula, say $A = \Box B$. For the sake of clarity, the
representation of the original sequent can be split into its boxed
and non-boxed components, so the original derivation
is:\marginpar{Was $\Boxesi{i}$ in succedent of premiss.}
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \wbx\Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof{}
\end{center}
When $A$ is to be added to the antecedent, the induction on height can
be used to add $A = \Box B$ to each of the original
premises. Following this by an application of the sub-induction on
formula rank, allows the addition of $B$, giving the derivability of
$B, \Box B, \Gamma, \Box \Gamma \vdash \varphi_i, \wbx\Boxesi{i}$. An
application of the S4.3$\Box$ rule then completes the case:
\begin{center}
\AxiomC{$B, \Box B, \Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Box B, \Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof{}
\end{center}
The final case to consider is that of adding $A = \Box B$ to the
succedent. The goal once again is to use the S4.3$\Box$ rule to give
the desired conclusion. From the original premises, the induction
hypothesis on height (inserting $\Box B$) gives the derivability of
$\Gamma, \Box \Gamma \vdash \varphi_i, \wbx\Boxesi{i}, \Box B$. A
different application of the S4.3$\Box$ rule, bringing in empty
contexts, on the original premises also gives the derivability of
$\Box \Gamma \vdash \Box \Boxes$. Applying the induction on formula
rank then shows that $\Box \Gamma \vdash B, \Box \Boxes$ is
derivable.
At this point, the derivability of all necessary premises for a new S4.3$\Box$ rule has been proven. These are sequents of the form $\Gamma, \Box \Gamma \vdash \varphi'_i, \Box \Boxesi{i}'$ where $\Boxes' = \Boxes, B$. The final rule application is then:
\begin{center}
\AxiomC{$\Gamma, \Box \Gamma \vdash \varphi'_i, \Box \Boxesi{i}'$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Box B, \Delta$}
\DisplayProof{}
\end{center}
\end{proof}
%In the base formalisation, a general lemma about \weaka{} suffices for a fairly broad range of calculi. If the conclusion of rules can be extended with an arbitrary context, then proving \weaka{} is very straightforward using an induction on height (premises in the formalisation). Weakening in formulae is as simple as instantiating the context of the rule as it was originally, but with the new formula also included. Note that this may require introducing new formulae in the premises as well, using the inductive hypothesis.
%\begin{lemma}[\texttt{wk\_adm\_ext\_concl}]\label{wk_adm:lem}
%If all rules in a calculus can be extended by arbitrary contexts in the conclusion, then Weakening is admissible in that calculus.
%\end{lemma}
%\begin{proof}
%By an induction on height, using drs.inductr (Lemma~\ref{inductr:lem}).
%\end{proof}
%This lemma is essentially a sufficient condition for \weaka{}, in the same
%style as the conditions for \cuta{} given by \cite{Rasga05}.
%For calculi where some rule(s) restrict contexts in their conclusion, the lemma \texttt{wk\_adm\_ext\_concl} no longer applies, and so a proof of \weaka{} requires the standard inductive style proof involving a case analysis of the last rule applied.
\subsection{Invertibility and Contraction}
Like S4, we prove inversion lemmas for the G3cp and Refl rules within the overall calculus. The only notable case occurs for the G3cp rules, where the last rule applied in the original derivation is S4.3$\Box$. If the original derivation is given by
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof{}
\end{center}
then proving invertibility for G3cp requires showing the derivability of all premises after applying a G3cp rule backwards from the endsequent of the S4.3$\Box$ rule. As the classical rules do not operate on boxed formulae, the rule can only modify $\Sigma$ or $\Delta$:
\begin{center}
\AxiomC{$\Sigma', \Box \Gamma \vdash \Box \Boxes, \Delta'$}
\LeftLabel{G3cp rule}
\UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof{}
\end{center}
Clarifying again, invertibility of the G3cp rule requires deriving $\Sigma', \Box \Gamma \vdash \Box \Boxes, \Delta'$.
The usual tactic would apply another instance of the S4.3$\Box$ rule to the original premises, but bringing in a different context. However, this does not admit a proof if there are boxed formula in $\Sigma'$ or $\Delta'$. For example, if the G3cp rule is L$\land$ and the principal formula is $A \land \Box B$ then $\Sigma'$ contains a boxed formula, $\Box B$, which cannot be introduced within the (box-free) context of a new S4.3$\Box$ rule application.
To accommodate this case, the premises of the modal rule are used to derive the conclusion without any context. Then \weaka{} is used to bring the remaining formulae in the premise of the G3cp rule:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Box \Gamma \vdash \Box \Boxes$}
\dashedLine
\LeftLabel{Weakening-admissibility}
\UnaryInfC{$\Sigma', \Box \Gamma \vdash \Box \Boxes, \Delta'$}
\DisplayProof{}
\end{center}
\begin{theorem}[\texttt{inv\_rl\_gs43\_refl} and \texttt{inv\_rl\_gs43\_lks}]
Refl (\texttt{lkrefl}) and all Classical rules (\texttt{lksss}) are invertible within the calculus \texttt{gs43\_rls}.
\end{theorem}
Before, for S4, proving invertibility is sufficient to lead to a \ctra{} proof. However, using invertibility alone does not allow an obvious transformation when dealing with the S4.3$\Box$ rule. In order to prove \ctra{}, we first require the following lemma:
TODO: possibly change the statement of this lemma?
\begin{lemma}[\texttt{gs43\_refl}]\label{lemma:R-refl-admin}
The rule R-refl is admissible in \texttt{gs43\_rls}.
\begin{center}
\AxiomC{$\Gamma \vdash \Delta, \Box A$}
\LeftLabel{R-refl}
\UnaryInfC{$\Gamma \vdash \Delta, A$}
\DisplayProof{}
\end{center}
The corresponding statement of the lemma in Isabelle states that
%\begin{lstlisting}
% seq : derrec gs43_rls {} -->
% (ALL X Y. seq = extend (X |- Y) (0 |- {#Box A#}) -->
% extend (X |- Y) (0 |- {#A#}) : derrec gs43_rls {})
%\end{lstlisting}
if a sequent \texttt{seq} is derivable in \texttt{gs43\_rls} and the sequent is equivalent to $X \vdash Y, \Box A$ for any $X$ and $Y$, then $X \vdash Y, A$ is also derivable.
\end{lemma}
\begin{proof}
By an induction on height, for all $\Gamma$ and $\Delta$. The analysis is on the last rule applied in deriving $\Gamma \vdash \Delta, \Box A$.
\begin{description}
\item[Case 1. The last rule applied was id.]
If $\Box A$ is parametric then $\Gamma \vdash \Delta$ is an axiom, and the conclusion will be also. If $\Box A$ is principal, then $\Gamma = \{\Box A\} \cup \Gamma'$ and the following transformation is applied:
\begin{center}
\AxiomC{}
\LeftLabel{id}
\UnaryInfC{$A, \Box A, \Gamma' \vdash \Delta, A$}
\LeftLabel{Refl}
\UnaryInfC{$\Box A, \Gamma' \vdash \Delta, A$}
\DisplayProof{}
\end{center}
\item[Case 2. The last rule applied was from G3cp.]
No rules in G3cp operate on a boxed formula, so $\Box A$ must be parametric. The induction hypothesis on height can thus be applied to the premise of the G3cp rule. Applying the original G3cp on the resulting sequent gives the desired conclusion.
\item[Case 3. The last rule applied was Refl.]
Like Case 2, $\Box A$ must be parametric, as Refl only operates on boxed formula in the antecedent.
\item[Case 4. The last rule applied was S4.3$\Box$.]
Then one premise of the original deduction un-boxes $\Box A$. Using Refl followed by \weaka{} on this premise is enough to produce the conclusion. For clarify, here we express $\Gamma = \Sigma \cup \Box \Gamma'$ and $\Delta = \Box \Boxes \cup \Delta'$. The original derivation is:
\begin{center}
\AxiomC{$\Pi_1$}
\noLine
\UnaryInfC{$\Gamma', \Box \Gamma' \vdash \Box \Boxes, A$}
\AxiomC{$\Pi_2$}
\noLine
\UnaryInfC{$\Gamma', \Box \Gamma' \vdash \varphi_i, \Box \Boxesi{i}, \Box A$}
\BinaryInfC{$\Sigma, \Box \Gamma' \vdash \Box \Boxes, \Delta', \Box A$}
\DisplayProof{}
\end{center}
This is transformed into:
\begin{center}
\AxiomC{$\Pi_1$}
\noLine
\UnaryInfC{$\Gamma', \Box \Gamma' \vdash \Box \Boxes, A$}
\LeftLabel{Refl}
\UnaryInfC{$\Box \Gamma' \vdash \Box \Boxes, A$}
\LeftLabel{Weakening-admissibility}
\dashedLine
\UnaryInfC{$\Sigma, \Box \Gamma' \vdash \Box \Boxes, \Delta', A$}
\DisplayProof{}
\end{center}
\end{description}
\end{proof}
%The above lemma is crucial in the case when the S4.3$\Box$ rule was the last used in a derivation.
\begin{theorem}[\texttt{gs43\_ctr\_adm}]
Contraction is admissible in \texttt{gs43\_rls}.
\end{theorem}
\begin{proof}
If the last rule used in the derivation was the S4.3$\Box$ rule,
there are two cases to consider. The case where the
contraction-formula is parametric is handled by simply re-applying
another instance of the S4.3$\Box$ rule like the S4 case.
Similarly, when the contraction-formula is principal in the
antecedent, then the proof proceeds like in S4. Specifically, one
copy of $\Box A$ from $\Sigma, \Box A, \Box A, \Box \Gamma \vdash
\Box \Boxes, \Delta$ must be removed. The original derivation is:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$A, A, \Box A, \Box A, \Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Sigma, \Box A, \Box A, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof{}
\end{center}
By contracting twice using first the induction hypothesis on height, then the induction hypothesis on rank, on all premises followed by an application of the S4.3$\Box$ rule, the desired endsequent is obtained:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$A, A, \Box A, \Box A, \Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\dashedLine
\LeftLabel{IH on height}
\UnaryInfC{$A, A, \Box A, \Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\dashedLine
\LeftLabel{IH on rank}
\UnaryInfC{$A, \Box A, \Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Sigma, \Box A, \Box \Gamma \vdash \Box \Boxes, \Delta$}
\DisplayProof{}
\end{center}
When the contraction-formula is principal in the succedent, then there are two cases of the premises to consider. Either a premise ``un-boxes'' one of the contraction-formulae\footnote{Technically, there are two syntactically identical premises which individually un-box one of the two copies of $\Box A$}, or it leaves both boxed. The original deduction is given by:
\begin{center}
\AxiomC{$\Pi_1$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \Box \Boxes, A, \Box A$}
\AxiomC{$\Pi_2$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}, \Box A, \Box A$}
\BinaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Box A, \Box A, \Delta$}
\DisplayProof{}
\end{center}
In the latter case, the induction hypothesis can be directly applied, removing one copy of the boxed formulae:
\begin{center}
\AxiomC{$\Pi_2$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i},
\Box A, \Box A$}
\dashedLine
\LeftLabel{IH on height}
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}, \Box A$}
\DisplayProof{}
\end{center}
In the former case, the original derivation is:
\begin{center}
\AxiomC{$\Pi_1$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \Box \Boxes, A, \Box A$}
\AxiomC{$\Pi_2$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}, \Box A, \Box A$}
\BinaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Box A, \Box A, \Delta$}
\DisplayProof{}
\end{center}
For this sub-case, we use the above Lemma~\ref{lemma:R-refl-admin} to
produce the following transformation:
\begin{center}
\AxiomC{$\Pi_1$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \Box \Boxes, A, \Box A$}
\dashedLine
\LeftLabel{R-refl}
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \Box \Boxes, A, A$}
\dashedLine
\LeftLabel{IH on rank}
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \Box \Boxes, A$}
\AxiomC{$\Pi_2$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box
\Boxesi{i}, \Box A, \Box A$}
\dashedLine
\LeftLabel{IH on height}
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}, \Box A$}
\LeftLabel{S4.3$\Box$}
\BinaryInfC{$\Sigma, \Box \Gamma \vdash \Box \Boxes, \Box A, \Delta$}
\DisplayProof{}
\end{center}
\end{proof}
\subsection{Cut}
\begin{theorem}[\texttt{gs43\_cas}]
Cut is admissible in the calculus \texttt{gs43\_Rls}.
\end{theorem}
\begin{proof}
When S4.3$\Box$ leads to the left cut-sequent, and the Refl rule is used on the right, the transformation mimics the corresponding case for S4. However, for the case where S4.3$\Box$ principal is principal on both sides requires a new transformation. For clarity, the premises above the S4.3$\Box$ rule on the left are given as two cases, depending on whether the cut-formula is un-boxed or not. The boxed formula in the succedents of the premises are also distinguished by the superscripts $L$ and $R$ for left and right cut premises respectively. Explicitly, these are $\Boxes^L = \{\varphi_1^L \dots \varphi_i^L \dots \varphi_n^L\}$ and $\Boxes^R = \{\psi_1^R \dots \psi_k^R \dots \psi_m^R\}$. The original cut thus has form:
\begin{center}
{\footnotesize
\AxiomC{$\Pi_L^a$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash \varphi_i^L, \Box \Boxesi{i}^L, \Box A$}
\AxiomC{$\Pi_L^b$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash A, \Box \Boxes^L$}
\LeftLabel{S4.3$\Box$}
\BinaryInfC{$\Sigma_L, \Box \Gamma_L \vdash \Box \Boxes^L, \Delta_L, \Box A$}
\AxiomC{$\Pi_R$}
\noLine
\UnaryInfC{$A, \Box A, \Gamma_R, \Box \Gamma_R \vdash \psi_k^R, \Box \Boxesi{k}^R$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\Box A, \Sigma_R, \Box \Gamma_R \vdash \Box \Boxes^R, \Delta_R$}
\LeftLabel{Cut on $\Box A$}
\BinaryInfC{$\Sigma_L, \Sigma_R, \Box \Gamma_L, \Box \Gamma_R \vdash \Box \Boxes^L, \Box \Boxes^R, \Delta_L, \Delta_R$}
\DisplayProof{}
}
\end{center}
To remove this cut, the derivation is transformed into one where the principal rule (S4.3$\Box$) is applied last to produce the desired endsequent. The problem is then proving that the premises of the following S4.3$\Box$ rule application are derivable. This in itself requires two different transformations of the original derivation, depending on the two forms that the premises can take; either the un-boxed formula in the succedent originated from the left cut premise, that is from $\Box \Boxes^L$, or from the right, within $\Box \Boxes^R$. These cases are named $\mathcal{P}_L$ and $\mathcal{P}_R$ respectively. The final S4.3$\Box$ rule used in our new transformation is then:
\begin{center}
\AxiomC{$\MP_L$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash \varphi_i^L, \Box \Boxesi{i}^L, \Box \Boxes^R$}
\AxiomC{$\MP_R$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash \Box \Boxes^L, \psi_k^R, \Box \Boxesi{k}^R$}
\LeftLabel{S4.3$\Box$}
\BinaryInfC{$\Sigma_L, \Sigma_R, \Box \Gamma_L, \Box \Gamma_R \vdash \Box \Boxes^L, \Box \Boxes^R, \Delta_L, \Delta_R$}
\DisplayProof{}
\end{center}
For both transformations, the same idea behind the principal S4$\Box$ rule case is used. We first derive the original cut-sequents but without their original contexts. These new sequents will be called $\mathcal{D}_L$ and $\mathcal{D}_R$ respectively. These are derived using the derivations in the original cut, but applying new instances of the S4.3$\Box$ rule.
Importantly, the new sequents $\mathcal{D}_L$ and $\mathcal{D}_R$ have the same height as the original cut-sequents.
\begin{center}
\AxiomC{$\Pi_L^a$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash \varphi_i^L, \Box \Boxesi{i}^L, \Box A$}
\AxiomC{$\Pi_L^b$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash A, \Box \Boxes^L$}
\LeftLabel{S4.3$\Box$}
\BinaryInfC{$\mathcal{D}_L = \Box \Gamma_L \vdash \Box \Boxes^L, \Box A$}
\DisplayProof{}
\end{center}
\begin{center}
\AxiomC{$\Pi_R$}
\noLine
\UnaryInfC{$A, \Box A, \Gamma_R, \Box \Gamma_R \vdash \psi_k^R, \Box \Boxesi{k}^R$}
\LeftLabel{S4.3$\Box$}
\UnaryInfC{$\mathcal{D}_R = \Box A, \Box \Gamma_R \vdash \Box \Boxes^R$}
\DisplayProof{}
\end{center}
Having introduced all the necessary notation and pre-requisites, the first actual case to consider is deriving $\mathcal{P}_L$. The induction on level allows $\mathcal{D}_R$ to be cut, on cut-formula $\Box A$, with all of the sequents given by the derivation $\Pi_L^a$ above the original left S4.3$\Box$ rule. The transformation performs $n$ cuts, for all premises corresponding to the formulae in $\Boxes^L$. The results of this cut then match exactly with $\mathcal{P}_L$ after using the admissibility of Weakening to introduce the formulae of $\Gamma_R$ in the antecedent.
\begin{center}
\AxiomC{$\Pi_L^a$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash \varphi_i^L, \Box \Boxesi{i}^L, \Box A$}
\AxiomC{$\MD_R$}
\noLine
\UnaryInfC{$\Box A, \Box \Gamma_R \vdash \Box \Boxes^R$}
\RightLabel{Cut on $\Box A$}
\BinaryInfC{$\Gamma_L, \Box \Gamma_L, \Box \Gamma_R \vdash \varphi_i^L, \Box \Boxesi{i}^L, \Box \Boxes^R$}
\dashedLine
\RightLabel{Weakening-admissibility}
\UnaryInfC{$\mathcal{P}_L = \Gamma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash \varphi_i^L, \Box \Boxesi{i}^L, \Box \Boxes^R$}
\DisplayProof{}
\end{center}
To derive the sequents in $\mathcal{P}_R$, the induction hypothesis on level is used to cut $\mathcal{D}_L$ with all of the premises above the right S4.3$\Box$ in the original cut, with cut-formula $\Box A$. The induction on formula rank on $A$ is then used to cut the sequent resulting from $\Pi_L^b$ with all these new sequents. Finally, \ctra{} allows the removal of the extra copies of $\Box \Gamma$ and $\Box \Boxes^L$, and concludes the case.
\begin{center}
\AxiomC{$\Pi_L^b$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash A, \Box \Boxes^L$}
\AxiomC{$\MD_L$}
\noLine
\UnaryInfC{$\Box \Gamma_L \vdash \Box \Boxes^L, \Box A$}
\AxiomC{$\Pi_R$}
\noLine
\UnaryInfC{$A, \Box A, \Gamma_R, \Box \Gamma_R \vdash \psi_k^R, \Box \Boxesi{k}^R$}
\RightLabel{Cut on $\Box A$}
\BinaryInfC{$\Box \Gamma_L, A, \Gamma_R, \Box \Gamma_R \vdash \Box \Boxes^L, \psi_k^R, \Box \Boxesi{k}^R$}
\RightLabel{Cut on $A$}
\BinaryInfC{$\Gamma_L, \Box \Gamma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash \Box \Boxes^L, \Box \Boxes^L, \psi_k^R, \Box \Boxesi{k}^R$}
\dashedLine
\RightLabel{Contraction-admissibility}
\UnaryInfC{$\mathcal{P}_R = \Gamma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash \Box \Boxes^L, \psi_k^R, \Box \Boxesi{k}^R$}
\DisplayProof{}
\end{center}
To conclude, the transformations above derive $\mathcal{P}_L$ and $\mathcal{P}_R$ while reducing cut-level or cut-rank. These are the premises of an instance of the S4.3$\Box$ rule which results in the conclusion of the original cut. This completes the \cuta{} proof.
\end{proof}
\section{The system GTD}
\label{s-gtd}
This section and the next describe Isabelle proofs of the
cut admissibility of the logic GTD described in \cite{mints-jaegerfest}
%
Axiomatically, GTD is $K$ with the additional axiom
$\Box A \Leftrightarrow \Box \Box A$.
The sequent inference rules involving $\Box$ are shown below:
$$
\frac{\wbx\Gamma, \Gamma \vdash A}{\Box \Gamma \vdash \Box A}
(\vdash\Box)
\qquad\qquad\qquad
\frac{\wbx\Gamma, \Gamma \vdash \Box A}{\Box \Gamma \vdash \Box A}
(\Box\vdash)
$$
% We first formalised $GTD$ as
% \texttt{glssc GTD}
% using a framework which had previously been applied to other logics.
% \texttt{GTD} means the rules involving $\Box$, and \texttt{glssc} refers to
% a set of classical logic rules, including explicit weakening and contraction
% rules.
% Our formalisation involves sequents consisting of multisets of formulae on
% either side of a turnstile.
% \begin{verbatim}
% datatype 'a sequent = Sequent "'a multiset" "'a multiset"
% \end{verbatim}
The above two rules are encoded as \texttt{GTD} shown below by
factoring out the form of $A$ as either $B$ or as $\wbx B$:
\begin{verbatim}
inductive "GTD" intros
I : "A = B | A = Box B ==>
([mset_map Box X + X |- {#A#}],
mset_map Box X |- {#Box B#}) : GTD"
\end{verbatim}
The second clause for \texttt{glssc} takes the rules in
\texttt{glne}\marginpar{This needs to be fixed!}
and adds a context (the same context) to the conclusion and \emph{all}
premises.
This means that the logical rules with two premises are of the context-sharing
form.
The following definitions explain this further where \verb!pscmap!
uniformly applies a function \verb!f! to each of the premises in the
list \verb!ps! and to the conclusion \verb!c!, while \verb!extend!
extends a given sequent \verb!seq! of the form $\Gamma \vdash \Delta$ with
a sequent \verb!XY! of the form $X \vdash Y$ built out of arbitrary
contexts $X$ and $Y$ to give the extended sequent \verb!seq + XY! of
the form $\Gamma, X \vdash \Delta, Y$:
% types
% 'a psc = "'a list * 'a" (* single step inference *)
% consts
% pscmap :: "('a => 'b) => 'a psc => 'b psc"
% (* extend a sequent by adding context to conclusion and premises *)
% extend :: "'a sequent => 'a sequent => 'a sequent"
\begin{verbatim}
primrec pscmap_def "pscmap f (ps, c) = (map f ps, f c)"
defs extend_def : "extend XY seq == seq + XY"
\end{verbatim}
% We reused some code from previous work in which the logical rules
% ($\vdash\lor$), ($\land\vdash$) and ($\vdash\lor$)
% were of the forms shown (without the context)
% $$
% \frac{A \vdash}{A \land B \vdash}
% \qquad
% \frac{B \vdash}{A \land B \vdash}
% \qquad
% \frac{\vdash A}{\vdash A \lor B }
% \qquad
% \frac{\vdash B}{\vdash A \lor B }
% \qquad
% \frac{A \vdash B}{\vdash A \to B }
% $$
% The rules used for classical logic (before extending them with a context)
% form the set \texttt{glne}: the rule sets
% \texttt{wkrls}, \texttt{ctrrls} $A$, \texttt{glil} and \texttt{glir}
% are the weakening rules, contraction (on $A$) rules, and the left and right
% logical introduction rules.
% \begin{verbatim}
% inductive "glne" (* rules before being extended *)
% intros
% wkI : "(ps, c) : wkrls ==> (ps, c) : glne"
% ctrI : "(ps, c) : ctrrls A ==> (ps, c) : glne"
% ilI : "(ps, c) : glil ==> (ps, c) : glne"
% irI : "(ps, c) : glir ==> (ps, c) : glne"
% \end{verbatim}
% To prove cut admissibility we actually used induction on a derivation to prove
% admissibility of the mix (multicut rule).
% \subsection{Framework of our induction proofs} \label{s-induction}
% FOLLOWING TEXT FROM OUR LPAR PAPER
% Many cut-elimination proofs proceed via two main phases. The first
% phase transforms the given derivations using several ``parametric''
% steps so that the cut-formula is the principal formula of the final
% rule in the resulting sub-derivations. The ``principal cut'' is then
% ``reduced'' into cuts which are ``smaller'' in some well-founded
% ordering such as size of cut-formula. We describe how we captured
% this two-phase structure of cut-elimination proofs, and present a
% widely applicable result that a parametric step is possible under
% certain conditions.
% We use the following framework for deriving cut-admissibility,
% or indeed any property $P$ of pairs of subtrees.
% In the diagram below, to prove $P (\MC_{l}, \MC_{r})$, the
% induction hypothesis is that $P (\MQ_{li}, \MC_{r})$ and $P (\MC_{l},
% \MQ_{rj})$ hold for all $i$ and $j$:
% \begin{center}
% \begin{prooftree}
% \AxiomC{$\MQ_{l1} \ldots \MQ_{ln}$}
% \RightLabel{$\rho_l$}
% \UnaryInfC{$\MC_{l}$}
% \AxiomC{$\MQ_{r1} \ldots \MQ_{rm}$}
% \RightLabel{$\rho_r$}
% \UnaryInfC{$\MC_{r}$}
% \RightLabel{(\textit{cut ?})}
% \dottedLine
% \BinaryInfC{?}
% \end{prooftree}
% \end{center}
% A proof of $P (\MC_{l}, \MC_{r})$ using this induction hypothesis
% inevitably proceeds by cases on the actual rules $\rho_l$ and
% $\rho_r$, and for a cut-formula $A$, on whether it is principal
% in either or both of $\rho_l$ and $\rho_r$. But we also use
% induction on the size of the cut-formula, or, more generally, on some
% well-founded relation on formulae.
% So we actually consider a property $P$ of a (cut) formula $A$
% and (left and right subtree conclusion) sequents $(\MC_l, \MC_r)$.
% In proving $P\ A\ (\MC_{l}, \MC_{r})$,
% in addition to the inductive hypothesis above, we assume
% that $P\ A'\ (\MD_l, \MD_r)$ holds generally for $A'$ smaller than $A$ and
% all ``\texttt{rls}-derivable'' sequents $\MD_l$ and $\MD_r$:
% \textit{i.e.} derivable from the empty set of
% premises using rules from $rls$. These intuitions give the
% following definition \texttt{gen\_step2sr} of
% a condition which permits one step of the inductive proof.
% Setting out proofs by using a number of lemmas, each stating
% \texttt{gen\_step2sr} \ldots for specific cases of the final rules on each side
% above the cut enables us to avoid having one huge monolithic proof in the
% Isabelle code.
% \begin{definition}[\texttt{gen\_step2sr}] \label{d-gen-step2sr}
% For a formula $A$, a property $P$,
% a subformula relation \texttt{sub},
% a set of rules \texttt{rls},
% inference rule instances $\MR_l = {(\psl, \MC_l)}$
% and $\MR_r = {(\psr, \MC_r)}$,
% \texttt{gen\_step2sr} $P\ A$ \texttt{sub rls} $(\MR_l, \MR_r)$
% means: %\\%[0.5em]
% % if %all the following hold:
% \begin{description}
% \item[if] forall ${A'}$ such that $(A', A) \in \texttt{sub}$
% and all \texttt{rls}-derivable sequents
% $\MD_l$ and $\MD_r$,
% ${P\ A'\ (\MD_l, \MD_r)}$ holds
% \item[and] for each ${\MP_{li}}$ in ${\psl}$,
% ${\MP_{li}}$ is \texttt{rls}-derivable and
% ${P\ A\ (\MP_{li}, \MC_r)}$ holds
% \item[and] for each ${\MP_{rj}}$ in ${\psr}$,
% ${\MP_{rj}}$ is \texttt{rls}-derivable and
% ${P\ A\ (\MC_l, \MP_{rj})}$ holds
% \item[and] ${\MC_l}$ and ${\MC_r}$ are \texttt{rls}-derivable.
% \item[then] ${P\ A\ (\MC_{l}, \MC_{r})}$ holds.
% \end{description}
% \end{definition}
% \begin{verbatim}
% gen_step2sr_simp: "gen_step2sr ?P ?A ?sub ?rls ((?aa, ?ba), ?ab, ?bb) =
% ((ALL A'. (A', ?A) : ?sub -->
% (ALL dl:derrec ?rls {}. ALL dr:derrec ?rls {}. ?P A' (dl, dr))) -->
% (ALL pl:set ?aa. pl : derrec ?rls {} & ?P ?A (pl, ?bb)) -->
% (ALL pr:set ?ab. pr : derrec ?rls {} & ?P ?A (?ba, pr)) -->
% ?ba : derrec ?rls {} --> ?bb : derrec ?rls {} --> ?P ?A (?ba, ?bb))"
% \end{verbatim}
% So the property $P$ we want to prove using this induction framework is that
% the final sequents $\MC_l$ and $\MC_r$ can be combined using the mix rule.
% The main theorem \texttt{gen\_step2sr\_lem} below for proving an
% arbitrary property $P$ states that if the step of the inductive proof
% is possible for all cases of final rule instances
% $\MR_l$ and $\MR_r$
% % ${(\psl, \MC_l)}$ and ${(\psr, \MC_r)}$
% on each side, then $P$ holds in all cases.
% \begin{theorem}[\texttt{gen\_step2sr\_lem}] \label{t-gen-step2sr-lem}
% If
% \begin{itemize}
% \item \texttt{A} is in the well-founded part of the subformula relation
% \texttt{sub},
% \item sequents $\MS_l$ and $\MS_r$ are \texttt{rls}-derivable, and
% \item for all formulae $A'$, and all rules $\MR_l$ and $\MR_r$,
% % ${(\psl, \MC_l)}$ and ${(\psr, \MC_r)}$,
% our induction step condition
% \texttt{gen\_step2sr} $P\ A'\ \texttt{sub rls}\ (\MR_l, \MR_r)$
% holds
% \end{itemize}
% then ${P\ A\ (\MS_l, \MS_r)}$ holds.
% \end{theorem}
% This enables us to split up an inductive proof, by showing,
% separately, that \texttt{gen\_step2sr} holds for particular cases of
% the final rules $(\MP_l, \MC_l)$ and $(\MP_r, \MC_r)$ on each side.
% For example, the inductive step for the case where the cut-formula $A$ is
% parametric, not principal, on the left is encapsulated in the
% following theorem where
% \mbox{\texttt{prop2 mar erls} $A\ (\MC_l, \MC_r)$} means
% that the conclusion of a multicut on \texttt{A} whose premises are
% $\MC_l$ and $\MC_r$ is derivable using rules \texttt{erls}.
% \begin{theorem}[\texttt{lmg\_gen\_step}]~\label{t-gs2sr}
% For any relation \texttt{sub} and any rule set \texttt{rls},
% given an instance of multicut with left and right subtrees
% ending with rules $\MR_l$ and $\MR_r$:
% \begin{description}
% \item[if] weakening is admissible for the rule set \texttt{erls},
% \item[and] all extensions of some rule $(\MP, X \vdash Y)$ are in the rule set
% \texttt{erls},
% \item[and] $\MR_l$ is an extension of $(\MP, X \vdash Y)$,
% \item[and] the cut-formula $A$ is not in $Y$
% (meaning that $A$ is parametric on the left)
% % \end{itemize}
% \item[then] \texttt{gen\_step2sr (prop2 mar erls)} $A$ \texttt{sub rls}
% $(\MR_l, \MR_r)$ holds.
% \end{description}
% \end{theorem}
% Theorem~\ref{t-gs2sr} codifies multi-cut elimination for parametric
% cut-formulae, and applies generally to many different
% calculi since it holds independently of the values of \texttt{sub} and
% \texttt{rls}. Of course, for a system with explicit weakening rules,
% such as $GTD$, weakening is {\it a fortiori} admissible.
% The above theorem uses the property \texttt{prop2 mar erls} (for rule set
% \texttt{erls}.
% We show the definitions of \texttt{prop2} and \texttt{mar} below.
% \begin{verbatim}
% inductive "mar rls A"
% I : "(Xl + ms_delete {A} Xr |- ms_delete {A} Yl + Yr) : derrec rls {}
% ==> (Xl |- Yl, Xr |- Yr) : mar rls A"
% inductive "mas rls A"
% I : "seql : derrec rls {} & seqr : derrec rls {} -->
% (seql, seqr) : mar rls A ==> (seql, seqr) : mas rls A"
% prop2_def : "prop2 f rls A seqs == seqs : f rls A"
% \end{verbatim}
% It may be noticed that \texttt{mar} and \texttt{mas} are similar except that
% \texttt{mas} contains explicitly the condition that the premises of the
% putative cut are derivable.
% In the context of induction on derivations, this is true anyway,
% so we have the following theorem
% \begin{verbatim}
% gs2_mas_mar: "gen_step2sr (prop2 mas ?rls) ?A ?sub ?rls =
% gen_step2sr (prop2 mar ?rls) ?A ?sub ?rls"
% \end{verbatim}
% (Later we will refer to \texttt{car} and \texttt{cas} which are corresponding
% concepts for single, rather than multiple, cuts).
% Then we get the following theorems:
% \begin{verbatim}
% glssc_gs2sr_GTD_r :
% "[| (?psa, ?ca) : extrs glne; (?psb, ?cb) : GTD |] ==>
% gen_step2sr (prop2 mar (glssc GTD)) ?A ?sub (glssc GTD)
% ((?psa, ?ca), ?psb, ?cb)"
% glssc_gs2sr_GTD_l :
% "[| (?psa, ?ca) : GTD; (?psb, ?cb) : extrs glne |] ==>
% gen_step2sr (prop2 mar (glssc GTD)) ?A ?sub (glssc GTD)
% ((?psa, ?ca), ?psb, ?cb)"
% \end{verbatim}
% That is, with a GTD rule on one side and one of the usual logical rule on the
% other, the inductive step is available.
% These results are easy because if the cut-formula is not the principal formula
% of the logical rule then Theorem~\ref{t-gs2sr} (and the corresponding result on
% the right) apply.
% If the cut-formula (which must be boxed)
% is the principal formula of the logical rule then the logical rule must be
% weakening or contraction, in which case applying multicut to its premise
% gives the required result.
% With logical rules on both sides, the following theorem applies:
% note that it applies to any logic \texttt{glssc ?R}
% (where $?R$ can stand for any set of rules).
% \begin{verbatim}
% glssc_gs2sr_ng:
% "[| c8ger_prop ?psubfml (glssc ?R) ?A (glne - wkrls - UNION UNIV ctrrls);
% (?psa, ?ca) : extrs glne; (?psb, ?cb) : extrs glne |] ==>
% gen_step2sr (prop2 mar (glssc ?R)) ?A ?psubfml (glssc ?R)
% ((?psa, ?ca), ?psb, ?cb)"
% \end{verbatim}
% The property \texttt{c8ger\_prop} says essentially that if \emph{single} cuts
% on subformulae of $A$ are admissible then a single cut on $A$
% is admissible where the last rules on either side are logical introduction
% rules introducing the cut-formula $A$.
% \begin{verbatim}
% "c8ger_prop ?isubfml ?drls ?A ?c8rls ==
% ALL ps qs pse qse X Y.
% (ps, 0 |- {#?A#}) : ?c8rls -->
% (qs, {#?A#} |- 0) : ?c8rls -->
% pse = map (extend (X |- Y)) ps -->
% qse = map (extend (X |- Y)) qs -->
% set pse Un set qse <= derrec ?drls {} -->
% (ALL sfa.
% (sfa, ?A) : ?isubfml --> (ALL seqs. seqs : cas ?drls sfa)) -->
% (X |- Y) : derrec ?drls {}"
% \end{verbatim}
% In the cases of the logical introduction rules proving multicut admissibility
% is more difficult than proving single cut admissibility.
% Where introduction of (just one instance of) the cut-formula $A$
% is the last step on each side before the cut,
% it is nesessary to perform multicut elimination on $A$ between
% $\MQ_{l1} \ldots \MQ_{ln}$ and $\MC_{r}$, and between
% $\MC_{l}$ and $\MQ_{r1} \ldots \MQ_{rm}$;
% then one performs single-cut elimination on the sub-formulae of $A$.
% These steps are part of the proof of \texttt{c8\_gs2\_mas}.
% An example follows.
% Note that here (unlike some of the other diagrams) the contexts
% $U$ and $Y$ may contain copies of the cut-formula.
% Let $Y'$ be $Y$ with copies of $A \land B$ deleted, and
% $U'$ be $U$ with copies of $A \land B$ deleted.
% \begin{center}
% \begin{prooftree}
% \AxiomC{$X \vdash A, Y$}
% \AxiomC{$X \vdash B, Y$}
% \RightLabel{($\vdash \land$)}
% \BinaryInfC{$X \vdash A \land B, Y$}
% \AxiomC{$U, A, B \vdash V$}
% \RightLabel{($\land \vdash$)}
% \UnaryInfC{$U, A \land B \vdash V$}
% \RightLabel{(\textit{mix ?})}
% \dottedLine
% \BinaryInfC{$X, U' \vdash Y', V$}
% \end{prooftree}
% \end{center}
% This is replaced by
% \begin{center}
% \begin{prooftree}
% \AxiomC{$X \vdash A, Y$}
% \AxiomC{$U, A \land B \vdash V$}
% \RightLabel{(\textit{inductive mix})}
% \dottedLine
% \BinaryInfC{$X, U' \vdash A, Y', V$}
% \dottedLine
% \UnaryInfC{\large (A)}
% \end{prooftree}
% \end{center}
% \begin{center}
% \begin{prooftree}
% \AxiomC{$X \vdash B, Y$}
% \AxiomC{$U, A \land B \vdash V$}
% \RightLabel{(\textit{inductive mix})}
% \dottedLine
% \BinaryInfC{$X, U' \vdash B, Y', V$}
% \dottedLine
% \UnaryInfC{\large (B)}
% \end{prooftree}
% \end{center}
% \begin{center}
% \begin{prooftree}
% \AxiomC{$X \vdash A \land B, Y$}
% \AxiomC{$U, A, B \vdash V$}
% \RightLabel{(\textit{inductive mix})}
% \dottedLine
% \BinaryInfC{$X, U', A, B \vdash Y', V$}
% \dottedLine
% \UnaryInfC{\large (C)}
% \end{prooftree}
% \end{center}
% Then (A), (B) and (C) are combined using inductive cuts on the smaller
% cut-formulae $A$ and $B$, and the necessary contractions,
% to derive the required sequent {$X, U' \vdash Y', V$}.
% \begin{verbatim}
% c8_gs2_mas:
% "[| wk_adm ?drls; ?prl = (?ps, 0 |- {#?A#}); ?qrl = (?qs, {#?A#} |- 0);
% ?prl : ?c8rls; ?qrl : ?c8rls;
% ?eprl = pscmap (extend (?Xl |- ?Yl)) ?prl;
% ?eqrl = pscmap (extend (?Xr |- ?Yr)) ?qrl;
% c8ger_prop ?sub ?drls ?A ?c8rls |] ==>
% gen_step2sr (prop2 mas ?drls) ?A ?sub ?drls (?eprl, ?eqrl)"
% \end{verbatim}
% We proved that \texttt{c8ger\_prop} holds in the following theorem.
% \begin{verbatim}
% rls_c8: "c8ger_prop ipsubfml (glssc ?rls) ?A
% (glne - wkrls - UNION UNIV ctrrls)"
% \end{verbatim}
% It remains to look at the case where the final rule on both sides of the
% desired cut are instances of the $GTD$ rules.
% Here there are two quite distinct cases, depending on which $GTD$ rule is used
% as the final step for the left premise of the cut.
% For the first case, the rule on the left is
% the $(\Box \vdash)$ rule as shown,
% and for the rule on the right,
% only its conclusion matters, and is as shown.
% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash \Box A$}
% \RightLabel{$(\Box\vdash)$}
% \UnaryInfC{$\Box \Gamma \vdash \Box A$}
% % \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% % \RightLabel{$\textit{ctr}^*\vdash$}
% % \UnaryInfC{$A, \Box A, \Delta, \Box \Delta \vdash B'$}
% \AxiomC{$\cdots$}
% \UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{mix ?})}
% \dottedLine
% \BinaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}
% we use the inductive hypothesis permitting multicutting $\Box A$ between
% $\Gamma, \Box \Gamma \vdash \Box A$ with $\Box A^n, \Box \Delta \vdash \Box B$
% then we use weakening and the $(\Box \vdash)$ rule, to get
% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash \Box A$}
% \AxiomC{$\cdots$}
% \UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{inductive mix})}
% \dottedLine
% \BinaryInfC{$\Gamma, \Box \Gamma, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{weak})}
% \UnaryInfC{$\Gamma, \Delta, \Box \Gamma, \Box \Delta \vdash \Box B$}
% \RightLabel{($\Box\vdash$)}
% \UnaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}
% The second case, with the $(\vdash \Box)$ rule on the left as shown,
% is more complicated.
% Note that, for the rule on the right, $B'$ can be either $\Box B$ or $B$.
% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash A$}
% \RightLabel{$(\Box\vdash)$}
% \UnaryInfC{$\Box \Gamma \vdash \Box A$}
% \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% \UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{mix ?})}
% \dottedLine
% \BinaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}
% In this case, from the premise on the right, we perform
% inductive mix on $\Box A$ with the conclusion on the left,
% then mix on $A$ with the premise on the left,
% contraction(s) on $\Box \Gamma$, and finally an instance of the
% $(\vdash \Box)$ or $(\Box \vdash)$ rule (whichever was on the right before).
% The result is shown below.
% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash A$}
% \AxiomC{$\Box \Gamma \vdash \Box A$}
% \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{(\textit{inductive mix})}
% \dottedLine
% \BinaryInfC{$A^n, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{(\textit{inductive mix})}
% \dottedLine
% \BinaryInfC{$\Gamma, \Box \Gamma, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{$(\textit{ctr}^*\vdash)$}
% \UnaryInfC{$\Gamma, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \UnaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}
% \begin{verbatim}
% glssc_gs2sr_GTD_GTD:
% "[| (?psa, ?ca) : GTD; (?psb, ?cb) : GTD |] ==>
% gen_step2sr (prop2 mar (glssc GTD)) ?A ipsubfml (glssc GTD)
% ((?psa, ?ca), ?psb, ?cb)"
% \end{verbatim}
% Finally we combine these results to get the mix admissibility result.
% \begin{verbatim}
% mas_GTD: "(?seql, ?seqr) : mas (glssc GTD) ?A"
% \end{verbatim}
% \section{Inductive proof of cut (\emph{not} mix) admissibility for GTD}
% \label{s-cut-gtd}
% The previous section dealt with a proof of cut admissibility where the
% inductive hypothesis was essentially that mix-admissibility is available for
% the end-sequents of ``smaller'' pairs of derivations.
% We now want to explore what it takes to produce an inductive proof where the
% inductive hypothesis is that (specifically) single-cut admissibility is
% available for ``smaller'' pairs of derivations.
% We define the ordinary logical rules of the differently from the above,
% so that the rules ($\vdash\lor$) and ($\land\vdash$) are
% of the forms shown (without the context)
% $$
% \frac{A, B \vdash}{A \land B \vdash}
% \qquad
% \frac{\vdash A, B}{\vdash A \lor B }
% $$
% In these forms, these rules are invertible.
% We define the rules of the system as follows.
% The rules used for classical logic (before extending them with a context)
% form the set \texttt{lkxcne}: the rule sets \texttt{idrls},
% \texttt{wkrls}, \texttt{ctrrls} $A$, \texttt{lksil} and \texttt{lksir}
% are the axioms, weakening rules, contraction (on $A$) rules,
% and the left and right logical introduction rules.
% \begin{verbatim}
% inductive "lkxcss xrls"
% intros
% extI : "psc : lkxcne ==> pscmap (extend flr) psc : lkxcss xrls"
% x : "psc : xrls ==> psc : lkxcss xrls"
% inductive "lkxcne"
% intros
% id : "psc : idrls ==> psc : lkxcne"
% wk : "psc : wkrls ==> psc : lkxcne"
% ctr : "psc : ctrrls A ==> psc : lkxcne"
% ilI : "psc : lksil ==> psc : lkxcne"
% irI : "psc : lksir ==> psc : lkxcne"
% \end{verbatim}
% When proving single-cut admissibility, the contraction rule causes a
% difficulty, since going up one step in the proof gives us an extra copy of the
% cut-formula to deal with, and the inductive hypothesis enables us to use an
% inductively available cut only to get rid of one copy of the cut-formula.
% The solution is to use the invertibility of the logical introduction rules,
% which reduces the problem of cut on a cut-formula $A$ containing a logical
% connective to cut on sub-formulae of $A$.
% Unfortunately the contraction rule causes the same sort of difficulty here as
% it does with the cut rule.
% So we have to prove, inductively, a sort of ``multi-invertibilty'' property,
% that multiple copies of a formula are invertible according to the introduction
% rule for that formula.
% Again, we define a predicate indicating that one step of an inductive proof
% of this result is available.
% Firstly, we define the set of inverses of a sequent according to a rule set:
% if $(ps, seq) \in irls$ and $p \in ps$,
% then $p \in \texttt{invs\_of}\ irls\ seq$.
% Then the property of interest is that when a sequent is derivable, its
% inverses are also derivable.
% The predicate \texttt{inv\_step} describes that this property holds for the
% end-sequent of a derivation, assuming that it holds for the preceding
% sequent(s).
% Note that there are two rule sets involved, the rules used for derivations and
% the rules being shown to be invertible.
% In the definition of \texttt{inv\_step}, \texttt{derivs} will be the set of
% derivable sequents.
% Then \texttt{inv\_step} \ldots means that
% for the last rule $(ps, concl)$ of a derivation:
% if the inverses of the premises $ps$ of that rule are derivable,
% then the inverses of the conclusion $concl$ are derivable.
% Finally, \texttt{gtd\_inv\_step} shows that the logical introduction rules,
% with each formula repeated $n$ times, and with contexts, are invertible,
% and \texttt{gtd\_inv\_rl} is the invertibility result.
% \begin{verbatim}
% invs_of_def: "invs_of ?irls ?seq ==
% {x. EX p ps. x = p & p : set ps & (ps, ?seq) : ?irls}"
% inv_step.simps: "inv_step ?derivs ?irls (?ps, ?concl) =
% (set ?ps <= ?derivs --> (ALL p:set ?ps. invs_of ?irls p <= ?derivs) -->
% invs_of ?irls ?concl <= ?derivs)"
% gtd_inv_step: "[| ?r : lksil Un lksir; ?x : lkxcss GTD |] ==>
% inv_step (derrec (lkxcss GTD) {}) (extrs (multiples {?r})) ?x"
% gtd_inv_rl: "Ball (extrs (multiples lksne)) (inv_rl (lkxcss GTD))"
% \end{verbatim}
% NOTE: From here the proof of cut admissibility is a single theorem with
% one long monolithic proof. Perhaps I should rearrange it so as to better
% enable a description of the intermediate results.
% First we need a change in the pattern of proof by induction.
% Referring to the diagram in \S\ref{s-induction},
% the induction hypothesis that $P (\MQ_{li}, \MC_{r})$ and $P (\MC_{l},
% \MQ_{rj})$ hold for all $i$ and $j$ will not be sufficient.
% Rather we will need an assumption that
% $P (\MQ'_{li}, \MC_{r})$ and $P (\MC_{l}, \MQ'_{rj})$ hold whenever
% $\MQ'_{li}$ is derived by a derivation no larger than the derivation
% of $\MQ_{li}$ (likewise for $\MQ'_{rj}$).
% This means that we need to define the height of a derivation tree, and
% therefore that we need to define a derivation tree value whose height can be
% defined and calculated.
% FOLLOWING FROM GLS LPAR PAPER -
% WE NEED TO MOVE IT EARLIER SINCE IT APPLIES TO SEVERAL SECTIONS
% ALSO DELETE IT FROM THE GLS SECTION LATER
% In~\cite{dawson-gore-cut-admissibility}, we modelled a derivation tree
% in HOL as a recursive structure which consists of a
% root sequent (which should be the conclusion of some rule), and an
% associated list of (sub)trees (each of which should derive a premise of
% that rule). The type of explicit derivation trees is a recursive
% datatype, such as:
% \begin{verbatim}
% datatype 'a dertree = Der 'a ('a dertree list)
% | Unf 'a (* unfinished leaf which remains unproved *)
% \end{verbatim}
% %
% We then had to express the property of such a tree, that it
% is in fact correctly based on the given rules, and so represents a
% valid derivation.
% A \textit{valid} tree is one whose inferences are in the set of rules
% and which as a whole has no premises.
% Thus we
% ``mix and match'' a deep embedding of derivation trees with a shallow
% embedding of inductively defined sets of derivable sequents.
% To ensure the correctness of our ``mixing and matching'' we needed the
% following relationship between our definitions of derivability according
% to the two embeddings.
% \begin{lemma} \label{l-derrec-valid}
% Sequent $X \vdash Y$ is derivable, shallowly,
% from the empty set of premises using rules \texttt{rls}
% (ie, is in \texttt{derrec rls} $\{\}$)
% %(ie, according to the definitions of \S\ref{s-dp})
% iff some explicit derivation tree
% \texttt{dt} is valid wrt.\ \texttt{rls} and has a conclusion
% $X \vdash Y$.
% \begin{verbatim}
% "(?a : derrec ?rls {}) = (EX dt. valid ?rls dt & conclDT dt = ?a)"
% \end{verbatim}
% \end{lemma}
% We can now define the height of such a tree, as
% \begin{verbatim}
% primrec (* height (max) of derivation tree *)
% "heightDT (Der seq dts) = Suc (heightDTs dts)"
% "heightDTs [] = 0"
% "heightDTs (dt # dts) = max (heightDT dt) (heightDTs dts)"
% \end{verbatim}
% Note that we had to use height as defined: we found that our first choice, to
% use the number of nodes in a derivation tree, did not work.
% So \texttt{height\_step2\_tr} \ldots states that the inductive step
% works for the two derivation trees above the putative cut
% (or whatever property we use this induction pattern for).
% Unlike in the case of \texttt{gen\_step2sr}, the (final) argument is a pair of
% derivation trees rather than the pair of bottom rules.
% Apart from this, \texttt{gen\_step2sr} is a stronger property
% (as it uses a weaker induction property), so we get the result
% \texttt{gs2\_cas\_hs\_tr} which links the two.
% This uses the relation on trees \texttt{casdt}, where cut-admissibility
% works between the conclusions of those trees.
% We also have a corresponding definition \texttt{masdt}
% and result \texttt{gs2\_mas\_hs\_tr} for multicuts.
% And, corresponding to \texttt{gen\_step2sr\_lem},
% we use the property by the lemma \texttt{height\_step2\_tr\_lem}.
% \begin{verbatim}
% height_step2_tr_eq: "height_step2_tr ?P ?A ?sub (?dta, ?dtb) =
% ((ALL A'. (A', ?A) : ?sub --> (ALL a b. ?P A' (a, b))) -->
% (ALL dtp. (dtp, ?dta) : measure heightDT --> ?P ?A (dtp, ?dtb)) -->
% (ALL dtq. (dtq, ?dtb) : measure heightDT --> ?P ?A (?dta, dtq)) -->
% ?P ?A (?dta, ?dtb))"
% inductive "casdt rls A"
% intros
% I : "valid rls dtl & valid rls dtr -->
% (conclDT dtl, conclDT dtr) : car rls A ==> (dtl, dtr) : casdt rls A"
% cas_casdt: "(conclDT ?dtl, conclDT ?dtr) : cas ?rls ?A ==>
% (?dtl, ?dtr) : casdt ?rls ?A
% gs2_cas_hs_tr:
% "gen_step2sr (prop2 cas ?rls) ?A ?sub ?rls (botRule ?dta, botRule ?dtb)
% ==> height_step2_tr (prop2 casdt ?rls) ?A ?sub (?dta, ?dtb)"
% height_step2_tr_lem: "[| ?A : wfp ?sub;
% ALL A dta dtb. height_step2_tr ?P A ?sub (dta, dtb) |] ==>
% ?P ?A (?dta, ?dtb)"
% \end{verbatim}
% Since we have proved invertibility for the logical introduction rules,
% when the cut-formula is a compound formula, then, regardless of what the
% final rules in the actual derivation trees are, we can use the invertibility
% and reduce the problem to that of cuts on smaller formula.
% We then use the fact that for all the logical connnectives,
% with their left and right logical introduction rules,
% we can use cuts on the subformulae on the premises of the introduction rules
% to achieve the effect of a cut on the whole formula
% on the conclusions of those introduction rules.
% This is expressed in the following theorem:
% \begin{verbatim}
% gprstep_q: "[| All (ctr_adm ?drls); wk_adm ?drls;
% (?ps, {#} |- {#?A#}) : lksir; (?qs, {#?A#} |- {#}) : lksil;
% ?pse = map (extend (?Xl |- ?Yl)) ?ps;
% ?qse = map (extend (?Xr |- ?Yr)) ?qs;
% set ?pse Un set ?qse <= derrec ?drls {};
% ALL sfa. (sfa, ?A) : ipsubfml --> (ALL Xl Yl Xr Yr.
% (Xl |- mins sfa Yl, mins sfa Xr |- Yr) : cas ?drls sfa);
% extrs lksne <= ?drls |] ==> (?Xl + ?Xr |- ?Yl + ?Yr) : derrec ?drls {}"
% \end{verbatim}
% There then remains the cases where the cut-formula $A$ is not a compound formula
% introduced by the logical introduction rules in the sets
% \texttt{lksil} and \texttt{lksir}.
% This means that $A$ is either a boxed formula or a primitive proposition
% (or, in our formulation, a formula variable).
% Because the bottom rule on either side may be a contraction on $A$,
% in which case cutting with the premise of that rule is of no help,
% we look upwards on either side to the lowest rule
% which is not a contraction on $A$.
% We have a lemma \texttt{top\_ctr\_r} which says that you can go up a derivation
% tree to a rule which is not contraction on $A$ on the right.
% A similar lemma \texttt{top\_ctr\_l} applies to contraction on the left.
% \begin{verbatim}
% top_ctr_r: "[| ?ctrrl = ([{#} |- {#?A#} + {#?A#}], {#} |- {#?A#});
% valid ?rls ?dt; conclDT ?dt = extend ?flr ({#} |- {#?A#}) |] ==>
% EX dtn n. botRule dtn ~: extrs {?ctrrl} & valid ?rls dtn &
% heightDT ?dt = heightDT dtn + n &
% conclDT dtn = extend ?flr (times (Suc n) ({#} |- {#?A#}))"
% \end{verbatim}
% We then look at the final rule of that derivation tree (which is necessarily
% not a contraction).
% There are cases where the rule is either one of the box rules or is an
% extension $\rho'$ of a rule $\rho$ in \texttt{lkxcne},
% and in this case the rule may or may not have $A$ as its principal formula.
% Where the rule has $A$ (in succedent position) as its principal formula,
% it can only be weakening (or the axiom, which is a trivial case).
% In this case either there are no contractions following the weakening, in which
% case weakening (of $A$) makes the cut-elimination trivial, or
% we construct a tree without the weakening step and with one fewer contractions,
% and this tree has the same conclusion;
% as this tree is smaller, we can apply the inductive hypothesis that
% cut-elimination is available.
% % end of rwr_tacs
% Next there is the case where the principal formula of the rule $\rho$
% is not $A$.
% This case is like the parametric rule case of the simpler cut-elimiation
% proofs.
% \begin{center}
% \begin{prooftree}
% \AxiomC{$X' \vdash Y', A^n$}
% \RightLabel{($\rho'$)}
% \UnaryInfC{$X \vdash Y, A^n$}
% \RightLabel{($\textit{ctr}^* \vdash$)}
% \UnaryInfC{$X \vdash Y, A$}
% \AxiomC{$A, U \vdash V$}
% \RightLabel{(\textit{cut ?})}
% \dottedLine
% \BinaryInfC{$X, U \vdash Y, V$}
% \end{prooftree}
% \end{center}
% Here we must apply the requisite number of contractions on $A$ to the premises
% of $\rho'$, then apply (using the inductive hypothesis) cut on $A$ to each of
% them, and finally apply $\rho''$ which is the appropriate (but different from
% $\rho'$) extension of $\rho$.
% \begin{center}
% \begin{prooftree}
% \AxiomC{$X' \vdash Y', A^n$}
% \RightLabel{($\textit{ctr}^* \vdash$)}
% \UnaryInfC{$X' \vdash Y', A$}
% \AxiomC{$A, U \vdash V$}
% \RightLabel{(\textit{inductive cut})}
% \dottedLine
% \BinaryInfC{$X', U \vdash Y', V$}
% \RightLabel{($\rho''$)}
% \UnaryInfC{$X, U \vdash Y, V$}
% \end{prooftree}
% \end{center}
% The remaining case is where the last rule on the left above the contractions on
% $A$ is one of the $GTD$ rules.
% But as their conclusion is of the form $\Box \Gamma \vdash \Box A$,
% this tells us that there are in fact no contractions following this rule.
% We now look at the right side, and again, look for the last rule above a
% continuous sequence of contractions on the cut-formula.
% Among the cases of the last rule on the right above the contractions,
% the cases of axiom or weakening involving $A$, or an extension of
% a rule in \texttt{lkxcne} whose principal formula is not $A$, are similar to
% those above.
% This leaves us the case where the last rules on both sides above any
% contractions are the GTD rules.
% For the first case, the rule on the left is
% the $(\Box \vdash)$ rule as shown,
% and for the rule on the right,
% only its conclusion matters, and is as shown.
% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash \Box A$}
% \RightLabel{$(\Box\vdash)$}
% \UnaryInfC{$\Box \Gamma \vdash \Box A$}
% % \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% % \RightLabel{$\textit{ctr}^*\vdash$}
% % \UnaryInfC{$A, \Box A, \Delta, \Box \Delta \vdash B'$}
% \AxiomC{$\cdots$}
% \UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
% \RightLabel{$(\textit{ctr}^*\vdash)$}
% \UnaryInfC{$\Box A, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{cut ?})}
% \dottedLine
% \BinaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}
% We use the inductive hypothesis permitting cutting $\Box A$ between
% $\Gamma, \Box \Gamma \vdash \Box A$ and $\Box A, \Box \Delta \vdash \Box B$
% then we use weakening and the $(\Box \vdash)$ rule, to get
% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash \Box A$}
% \AxiomC{$\cdots$}
% \UnaryInfC{$\Box A, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{inductive cut})}
% \dottedLine
% \BinaryInfC{$\Gamma, \Box \Gamma, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{weak})}
% \UnaryInfC{$\Gamma, \Delta, \Box \Gamma, \Box \Delta \vdash \Box B$}
% \RightLabel{($\Box\vdash$)}
% \UnaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}
% The second case, with the $(\vdash \Box)$ rule on the left as shown,
% is more complicated.
% Note that, for the rule on the right, $B'$ can be either $\Box B$ or $B$.
% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash A$}
% \RightLabel{$(\Box\vdash)$}
% \UnaryInfC{$\Box \Gamma \vdash \Box A$}
% \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% \UnaryInfC{$\Box A^n, \Box \Delta \vdash \Box B$}
% \RightLabel{$(\textit{ctr}^*\vdash)$}
% \UnaryInfC{$\Box A, \Box \Delta \vdash \Box B$}
% \RightLabel{(\textit{cut ?})}
% \dottedLine
% \BinaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}
% In this case, from the premise on the right, we perform contractions on
% $\Box A$, then inductive cut on $\Box A$ with the conclusion on the left,
% then contractions on $A$, then cut on $A$ with the premise on the left,
% contraction(s) on $\Box \Gamma$, and finally an instance of the
% $(\vdash \Box)$ or $(\Box \vdash)$ rule (whichever was on the right before).
% The result is shown below.
% \begin{center}
% \begin{prooftree}
% \AxiomC{$\Gamma, \Box \Gamma \vdash A$}
% \AxiomC{$\Box \Gamma \vdash \Box A$}
% \AxiomC{$A^n, \Box A^n, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{$(\textit{ctr}^*\vdash)$}
% \UnaryInfC{$A^n, \Box A, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{(\textit{inductive cut})}
% \dottedLine
% \BinaryInfC{$A^n, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{$(\textit{ctr}^*\vdash)$}
% \UnaryInfC{$A, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{(\textit{inductive cut})}
% \dottedLine
% \BinaryInfC{$\Gamma, \Box \Gamma, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{$(\textit{ctr}^*\vdash)$}
% \UnaryInfC{$\Gamma, \Box \Gamma, \Delta, \Box \Delta \vdash B'$}
% \RightLabel{$(\vdash \Box)$ or $(\Box \vdash)$}
% \UnaryInfC{$\Box \Gamma, \Box \Delta \vdash \Box B$}
% \end{prooftree}
% \end{center}
% Finally we combine these results to get the cut admissibility result,
% in terms of explicit derivation trees, and then in terms of derivability.
% \begin{verbatim}
% gtd_casdt: "(?dta, ?dtb) : casdt (lkxcss GTD) ?A" : Thm.thm
% gtd_cas: "(?cl, ?cr) : cas (lkxcss GTD) ?A" : Thm.thm
% \end{verbatim}
\section{GTD without structural rules CHANGE TITLE} \label{s-cut-gtdns}
We now look at proving cut admissibility for a version of GTD without structural
rules, where the box rules have their conclusions (only)
extended with an arbitrary context, which permits weakening to be admissible.
We define the rules of the system as follows. The rules used for
classical logic (before extending them with a context) form the set
\texttt{lksne} where the rule sets \texttt{idrls}, \texttt{lksil} and
\texttt{lksir} are the axioms and the left and right logical
introduction rules: see Figure~\ref{S4:rules}.\marginpar{JED please
check verbatim code!}
\begin{definition}
Given, a rule set \verb!xrls!, every rule of \verb!xrls! is in the
rule set \verb!lkssx xrls!, and
every rule \verb!psc! in rule set \verb!lknse! gives a
rule in \verb!lkssx xrls! obtained by uniformly extending
both the premise and conclusion of \verb!psc! with an arbitrary
context (sequent) \verb!flr!:
\end{definition}
\begin{verbatim}
inductive "lkssx xrls" intros
x : "psc : xrls ==> psc : lkssx xrls"
extI : "psc : lksne ==> pscmap (extend flr) psc : lkssx xrls"
\end{verbatim}
Given a rule set \verb!rules!,
the rule set \verb!extcs rules! is obtained by extending only the
conclusion \verb!c! of each rule \verb!(ps, c)! in
\verb!rules! by an arbitrary context (sequent) \verb!flr! (while
leaving the premises unchanged):
\begin{verbatim}
inductive "extcs rules" intros
I : "(ps, c) : rules ==> (ps, extend flr c) : extcs rules"
\end{verbatim}
The rule set \verb!gtdns! for the logic GTD is obtained by
extending only the conclusion of the rule \verb!GTD! and by
extending every rule of \verb!lknse!:
\begin{verbatim}
gtdns == lkssx (extcs GTD)
\end{verbatim}
First we prove weakening admissibility.
It follows directly from
\begin{verbatim}
wk_adm_extrs_cs: "wk_adm (extrs ?rlsa Un extcs ?rls)"
\end{verbatim}
which is proved in the same way that weakening admissibility is proved for S4.
For contraction admissibility,
first we need to prove invertibility of the logical rules.
SIMILAR to S4. Uses
\begin{verbatim}
lks_inv_stepm:
val it = "?psc : extrs lksne ==> inv_stepm (extrs lksne) (extrs lksne) ?psc"
inv_stepm_disj_cs:
"[| seq_meet ?c ?ic = 0; extcs {(?ps, ?c)} = ?rls; ?rl : ?rls |] ==>
inv_stepm ?rls (extrs {(?ips, ?ic)}) ?rl"
inv_stepm_disj:
"[| seq_meet ?c ?ic = 0; extrs {(?ps, ?c)} = ?rls; ?rl : ?rls |] ==>
inv_stepm ?rls (extrs {(?ips, ?ic)}) ?rl"
inv_stepm_scrls:
"[| extrs {?srl} = ?rls; ?rl : ?rls; ?srl : scrls; ?irl : scrls;
snd ?srl = snd ?irl --> ?srl = ?irl |] ==>
inv_stepm ?rls (extrs {?irl}) ?rl"
\end{verbatim}
The results \texttt{inv\_stepm\_disj\_cs} and \texttt{inv\_stepm\_disj}
are for the case where the formula to be inverted is in the context of
the conclusion of the last rule of the derivation:
the first premise gives you that the formula to be inverted is
not the principal formula of the rule, though it is expressed in a way
which is relevant to a case where the rules in question have more than just one
principal formula.
The result \texttt{inv\_stepm\_scrls} (whose proof uses
\texttt{inv\_stepm\_disj}) uses the fact that for each formula there
is a unique introduction rule, so an inversion step is either
parametric or gives you the premise(s) of the last rule applied.
%gtdns_inv_rl: "Ball (extrs lksne) (inv_rl (lkssx (extcs GTD)))"
\begin{lemma}
Every rule of \verb!lksss! is invertible in the calculus
\verb!gtdns_rls!:
\end{lemma}
\begin{verbatim}
gtdns_inv_rl: "Ball lksss (inv_rl gtdns_rls)"
\end{verbatim}
Then, to prove contraction admissibility,
SIMILAR to S4
we use
\begin{verbatim}
ctxt_ctr_adm_step1_cs: "[| pg_meet ?concl (?As + ?As) <= ?As;
?rl = (?ps, ?concl); (?ps, extend ?flr ?concl) = ?erl;
extcs {?rl} <= ?rules |] ==> ctr_adm_step1 (derrec ?rules {}) ?erl ?As"
\end{verbatim}
to handle the case where at least one of the copies of the formula to be
contracted arises from the extension of the conclusion of the box rule.
\texttt{ctr\_adm\_step1} is a simplified version of \texttt{ctr\_adm\_step},
without the inductive hypothesis relating to smaller formulae.
Now, for cut admissibility: the difficult cases are where the last rule on both
sides is one of the two box rules.
Since the proof is effectively the same whichever of the two rules is on the
right, we define
\begin{verbatim}
inductive "s4g prs"
intros
I : "A : prs B ==>
([mset_map Box X + X |- {#A#}], mset_map Box X |- {#Box B#}) : s4g prs"
\end{verbatim}
and we prove the two results
\begin{verbatim}
s4_box_box_lem:
"[| ?prsl = (%B. {B}); wk_adm ?drls; All (ctr_adm ?drls);
extcs (s4g ?prsl) <= ?drls; extcs (s4g ?prsr) <= ?drls;
(map conclDT ?dtll, ?cl) : extcs (s4g ?prsl);
(map conclDT ?dtlr, ?cr) : extcs (s4g ?prsr) |]
==> sumh_step2_tr (prop2 casdt ?drls) ?A ipsubfml
(Der ?cl ?dtll, Der ?cr ?dtlr)"
gtd_box_box_lem:
"[| ?prsl = (%B. {Box B}); wk_adm ?drls; All (ctr_adm ?drls);
extcs (s4g ?prsl) <= ?drls; extcs (s4g ?prsr) <= ?drls;
(map conclDT ?dtll, ?cl) : extcs (s4g ?prsl);
(map conclDT ?dtlr, ?cr) : extcs (s4g ?prsr) |]
==> sumh_step2_tr (prop2 casdt ?drls) ?A ipsubfml
(Der ?cl ?dtll, Der ?cr ?dtlr)"
\end{verbatim}
For the cut-elimination proof we also use results for the
parametric cases, that is, where the cut-formula appears in the context of the
last rule on either side above the cut.
This includes cases where that rule is in \texttt{extrs} \ldots
(where the rule has a context which appears in premises and conclusion)
and where that rule is in \texttt{extcs} \ldots
(where the rule has a context which appears only in the conclusion).
\begin{verbatim}
lcg_gen_step: "[| wk_adm ?erls; extrs {(?ps, ?U |- ?V)} <= ?erls; ~ ?A :# ?V;
?pscl = pscmap (extend (?W |- ?Z)) (?ps, ?U |- ?V) |] ==>
gen_step2sr (prop2 car ?erls) ?A ?any ?erls (?pscl, ?pscr)"
lcg_gen_steps_extcs:
"[| wk_adm ?rls; extcs {(?ps, ?c)} <= ?rls; ~ ?A :# succ ?c |] ==>
gen_step2sr (prop2 car ?rls) ?A ?sub ?rls ((?ps, extend ?flr ?c), ?psr, ?cr)"
\end{verbatim}
Finally we need to deal with the cases of matching instances of the usual
logical introduction rules.
Here we use the general result
\begin{verbatim}
gs2sr_alle: "[| wk_adm ?prls; c8_ercas_prop ?psubfml ?prls ?A ?rls;
?rls <= iscrls; idrls <= ?prls; extrs ?rls <= ?prls;
(?psa, ?ca) : extrs ?rls; (?psb, ?cb) : extrs ?rls |] ==>
gen_step2sr (prop2 car ?prls) ?A ?psubfml ?prls ((?psa, ?ca), ?psb, ?cb)"
\end{verbatim}
This theorem (which incorporates the parametric cases) uses
\texttt{c8\_ercas\_prop} which says essentially that if both sides of the cut are
logical introduction rules, and cut is admissible on smaller cut-formulae,
then the cut in question is admissible.
The property \texttt{c8sg\_prop} is almost identical ---
the difference is weakening / contraction.
(LATER - on looking back at the previous section I find the result
\texttt{gprstep\_q} shown -
basically that result plus the case of the axiom rules gives you
\texttt{gen\_lksne\_c8sg} below)
Omitting the definition of \texttt{c8\_ercas\_prop},
here is the theorem which uses it:
\begin{verbatim}
c8_ercas_gs2: "[| c8_ercas_prop ?psubfml ?drls ?A ?c8rls;
?prl = (?ps, 0 |- {#?A#}); ?prl : ?c8rls;
?qrl = (?qs, {#?A#} |- 0); ?qrl : ?c8rls;
?eprl = pscmap (extend ?pe) ?prl; ?eqrl = pscmap (extend ?qe) ?qrl |] ==>
gen_step2sr (prop2 car ?drls) ?A ?psubfml ?drls (?eprl, ?eqrl)"
c8sg_ger: "c8sg_prop ?sub ?rls ?drls ?A ==> c8_ercas_prop ?sub ?drls ?A ?rls"
\end{verbatim}
The key property here is that
\begin{verbatim}
gtdns_lksne_c8sg: "c8sg_prop ipsubfml (lkssx (extcs GTD)) ?A lksne"
\end{verbatim}
which in turn uses the more general result which is not specific to GTD
\begin{verbatim}
gen_lksne_c8sg: "[| All (ctr_adm ?drls); wk_adm ?drls; extrs lksne <= ?drls |]
==> c8sg_prop ipsubfml lksne ?drls ?A"
\end{verbatim}
Finally we get the cut admissibility result:
\begin{verbatim}
gtdns_casdt: "(?dt, ?dta) : casdt (lkssx (extcs GTD)) ?A"
gtdns_cas:
"(?Xl |- mins ?A ?Yl, mins ?A ?Xr |- ?Yr) : cas (lkssx (extcs GTD)) ?A"
\end{verbatim}
%\input{gtdnew}
%\input{s4c}
\input{s4cns}
\input{refs}
\end{document}