\documentclass{amsart}
%\documentclass[landscape]{slides}
%\usepackage[normalem]{ulem}
\usepackage{amssymb, bussproofs, amsmath, amsthm, datetime}

%\usepackage{graphicx, xcolor}

\usepackage{enumerate}



\newtheorem{theorem}{Theorem}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{remark}{Remark}

\title{Simplified cut-elimination for modal provability logics}

%\author{}
\email{revantha@logic.at}

\address{\today. \currenttime}

%\institute{
%Technische Universit\"{a}t Wien, Vienna, Austria.\\
%\email{revantha@logic.at}
%}

%\authorrunning{Ramanayake}
%\titlerunning{Short proofs of cut-elimination for~$\sys{GL}$ and related logics}

\newcommand{\sys}[1]{\mathsf{#1}}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\imp}{\rightarrow}
\renewcommand{\rule}[1]{(\text{#1})}
\newcommand{\mh}[1]{\text{mh}(#1)}

\renewcommand{\qed}{\hfill $\dashv$}
\begin{document}

\begin{abstract}
  We give simple, uniform and modular proofs of cut-elimination for $\sys{GL}$,
  $\sys{Go}$ and $\sys{Grz}$. The existing proofs in the literature are highly
  intricate and specialised.
\end{abstract}

\maketitle

\section{Problem?}

What does the cut-elimination procedure produce for the following cut:

\[
\AxiomC{$p, \Box q \Ra \Box \lnot\lnot q$}
\AxiomC{$\Box \lnot\lnot q \Ra \Box q, p$}
\BinaryInfC{$p, \Box q \Ra \Box q, p$}
\DisplayProof
\]

It appears to produce this:
\[
\AxiomC{$q, \Box q \Ra q$}
\UnaryInfC{$p, \Box q \Ra \Box q, p$}
\DisplayProof
\]

But this is NOT a derivation since it breaks the (*) condition?

It may be that you need to keep an eye out for instances of (id) at every step
of the proof ? For example, the base case is ``if $U, X \Ra Y, V$ is an instance
of (id) then stop''.

Another possible problem is that mh is not respected upwards by cut!

\section{Introduction}

Modal provability logics extend the basic normal modal logic $\sys{K}$ with
axioms which interpret the $\Box$ connective as the mathematical notion of being
``provable'' in Peano Arithmetic~\cite{boolos}. There are several variants with
characteristic axioms named after G\"odel, L\"ob and Grzegorczyk:

\smallskip
\begin{center}
\begin{tabular}[c]{ll}
 Name of Logic & Characteristic Axiom 
\\
  $\sys{GL}$ & $\Box(\Box p \imp  p) \imp \Box p$ 
\\
  $\sys{Go}$ & $\Box(\Box (p \imp \Box p) \imp p) \imp \Box p$ 
\\
  $\sys{Grz}$ & $\Box(\Box (p \imp \Box p) \imp p) \imp p$ 
\end{tabular}
\end{center}
\smallskip


While the ``provability'' interpretation is now well-understood, the
proof-theory of these logics is intricate and somewhat controversial as we
explain next.

Following Gentzen~\cite{gentzen-szabo-translation}, the literature abounds with
proofs of cut-elimination for various logics using size of the cut formula and
height of the premise derivations. But these measures proved inadequate for
proving cut-elimination for $\sys{GL}$, so Valentini introduced a third novel
measure called width, and showed that cut-elimination for~$\sys{GL}$ now
required a triple induction over size, height and width~\cite{valentini-}.

Controversy arose when it was (erroneously) claimed that Valentini's proofs
contained a gap~\cite{gore-ramanayake-resolved} and various authors provided
alternative proofs of cut-elimination in response \cite{mints,negri,}. The
question was resolved in Valentini's favour, with all proofs verfied using an
interactive theorem prover Isabelle/HOL~\cite{dawson-gore-ramanayake-verified}.

\textbf{His???} proofs for the logic $\sys{Go}$ are even more intricate,
involving .... \marginpar{Rev, can you please fill in this part as I can't
  remember the details any more.}

Thus the proof-theory of provability logics was significantly more complicated
than the proof-theory of numerous other modal logics.

Recently, Brighton~\cite{} gave yet another method for proving cut-elimination
for $\sys{GL}$ which is significantly shorter and simpler than any of the
existing proofs of cut-elimination in the literature because it uses only a
double induction on weight and ``maximum height of regress trees''.

Here, we finesse Brighton's argument by porting it to a sequent calculus, rather
than ``regress-trees'', and fix some errors in Valentini's original
proof. Moreover we show how this argument extends to~$\sys{Go}$ where the only
extant proof~\cite{???} is highly intricate.

**more story and citations**

\section{Syntax and Axiomatisations of Provability Logics}

\begin{figure}[t]
  \centering
\begin{tabular}{cc}
\multicolumn{2}{c}{
\AxiomC{}
\LeftLabel{\rule{id}}
\UnaryInfC{$X,A \Ra A, Y$}
\DisplayProof
}
\\[1.5em]
\AxiomC{$X\Ra Y, A$}
\AxiomC{$B,X\Ra Y$}
\LeftLabel{\rule{$\imp$ l}}
\BinaryInfC{$A\imp B,X\Ra Y$}
\DisplayProof
&
\AxiomC{$A,X\Ra Y,B$}
\LeftLabel{\rule{$\imp$ r}}
\UnaryInfC{$X\Ra Y,A\imp B$}
\DisplayProof
\\[1.5em]
\AxiomC{$A,X\Ra Y$}
\AxiomC{$B,X\Ra Y$}
\LeftLabel{\rule{$\lor$ l}}
\BinaryInfC{$A\lor B,X\Ra Y$}
\DisplayProof
&
\AxiomC{$X\Ra Y,A,B$}
\LeftLabel{\rule{$\lor$ r}}
\UnaryInfC{$X\Ra Y,A\lor B$}
\DisplayProof
\\[1.5em]
\AxiomC{$A,B,X\Ra Y$}
\LeftLabel{\rule{$\land$ l}}
\UnaryInfC{$A\land B, X\Ra Y$}
\DisplayProof
&
\AxiomC{$X\Ra A, Y$}
\AxiomC{$X\Ra B, Y$}
\LeftLabel{\rule{$\land$ r}}
\BinaryInfC{$X\Ra A\land B, Y$}
\DisplayProof
\\[1.5em]
\AxiomC{$X\Ra Y,A$}
\LeftLabel{\rule{$\lnot$ l}}
\UnaryInfC{$\lnot A,X\Ra Y$}
\DisplayProof
&
\AxiomC{$A,X\Ra Y$}
\LeftLabel{\rule{$\lnot$r}}
\UnaryInfC{$X\Ra Y,\lnot A$}
\DisplayProof
\\[1.5em]
\multicolumn{2}{c}{
\AxiomC{$\Box X,X,\Box B\Ra B$}
\LeftLabel{$\rule{GLR}$}
\RightLabel{$U$ non-boxed multiset}
\UnaryInfC{$U,\Box X\Ra \Box B,V$}
\DisplayProof
}
\\[1.5em]
\multicolumn{2}{c}{
\AxiomC{$\Box X, X, \Box (B \imp  \Box B) \Ra  B$}
\LeftLabel{$\rule{GoR}$}
\RightLabel{$U$ non-boxed multiset}
\UnaryInfC{$U, \Box X \Ra  \Box B, V$}
\DisplayProof
}
\\[1.5em]
\multicolumn{2}{c}{
\AxiomC{$A, \Box A, X \Ra Y$}
\LeftLabel{$\rule{T}$}
\RightLabel{need some side-conditions for mh-argument}
\UnaryInfC{$\Box A , X\Ra  Y$}
\DisplayProof
}
\end{tabular}
  \caption{Sequent Rules}
  \label{fig:seq-pc}
\end{figure}

Modal formulae are constructed from an infinite set $\mathcal{P}$ of atomic
formulae using the Backus-Naur form below where $p \in \mathcal{P}$:
\[
   A, B ::= p \mid \lnot A \mid A \imp B \mid A \lor B \mid A \land B \mid \Box A
\]
The $\Diamond$ connective does not appear explicitly but is defined via 
$\Diamond A := \lnot\Box\lnot A$.

A \textit{boxed formula} has $\Box$ as its main connective while a 
 \textit{non-boxed} formula does not. A boxed/non-boxed multiset contains
only boxed/non-boxed formulae.

The Hilbert-calculus for the basic normal modal logic $\sys{K}$ is obtained by
extending a Hilbert-calulus for classical propositional logic with the axiom 
$\Box (p \imp q) \imp (\Box p \imp \Box q)$ and the inference
rule of neccessitation: from $A$ infer $\Box A$. The various provability logics
are then obtained by adding further axioms as shown below:

\begin{center}
\begin{tabular}[c]{lll}
 Name of Logic & \multicolumn{2}{c}{Axioms}
\\
  $\sys{GL}$ & $\Box(\Box p \imp  p) \imp \Box p$ &
\\
  $\sys{GL_{lin}}$ & $\Box(\Box p \imp  p) \imp \Box p$ & $\Box (\Box p \imp q) \lor \Box (\Box q \imp q)$
\\
  $\sys{Go}$ & $\Box(\Box (p \imp \Box p) \imp p) \imp \Box p$ &
\\
  $\sys{Grz}$ & $\Box(\Box (p \imp \Box p) \imp p) \imp \Box p$ &  $\Box p \imp p$
\end{tabular}
\end{center}

The axiomatisation of $\sys{Grz}$ given above is indirect since the
characteristic axiom 
$\Box(\Box (p \imp \Box p) \imp p) \imp p$ 
is actually obtained by chaining the two axioms
shown in the table above. This axiomatisation justifies the sequent rules for 
$\sys{Grz}$ to follow.


\section{Sequent Caluli, Semi-derivations and Maximum Height}

A sequent is a tuple $(X,Y)$ of formula multisets, written $X\Ra Y$.
Let~$X\cap Y$, $X\cup Y$ and~$\emptyset$ denote, respectively, the multiset
intersection, union and empty multiset. So $\{A\}\cup\{A\}$ is the multiset
consisting of two occurrences of~$A$. In sequents, we also write $A, X$ or $X,A$ to stand for 
${A} \cup X$, and similarly write $X,Y$ for $X \cup Y$.

% Using this notation, 
% a sequent $X' \Ra Y'$ satisfying $X' \cap Y' \neq \emptyset$ can be written as
% $A, X \Ra A, Y$ for appropriate $X$ and $Y$,
% and is called an \textit{initial sequent}.
The various sequent calculi are shown below using rules from Figure~\ref{fig:seq-pc}:

\begin{center}
\begin{tabular}[c]{ll}
  Name & Sequent Calculus Rules
\\
   $\sys{PC}$ & \rule{id} \rule{$\lnot$L} \rule{$\lnot$R} \rule{$\imp$L}
                \rule{$\imp$R}
                \rule{$\land$L} \rule{$\land$R}
                \rule{$\lor$L} \rule{$\lor$R}
\\
   $\sys{GLS}$ & $\sys{PC}$ + $\rule{GLR}$
\\
   $\sys{GoS}$ & $\sys{PC}$ + $\rule{GoR}$
\\
   $\sys{GrzS}$ & $\sys{PC}$ + \rule{GoR} + \rule{T}
\end{tabular}
\end{center}

\begin{definition}[semi-derivation, derivation]
A \emph{semi-derivation} in the sequent calculus is defined inductively as a sequent, or a rule applied upwards to a leaf of a semi-derivation, that additionally satisfies
\begin{quote}
($\ast$) an initial sequent occurs only as a leaf
\end{quote}
If every leaf of the semi-derivation is an initial sequent, then it is called a
\emph{derivation} and its end-sequent (root) is said to be \emph{derivable}.
\end{definition}

Note that~($\ast$) ensures that only minimal derivations are permitted: no rule
is applied upwards to an initial sequent as captured by the \rule{id} rule. 
Apart from this, the definition of derivation above is the standard
one. The following definition of height is also standard.
\begin{definition}[height]
The \emph{height} of a semi-derivation is the number of sequents along its longest branch.
\end{definition}

% The sequent calculus~$\sys{GLS}$ is obtained by the addition of the following
% rule to the above.
% \marginpar{How to delete the offending Box-formulae in succedent of conclusion}
% \begin{center}
% \AxiomC{$\Box X,X,\Box B\Ra B$}
% \RightLabel{$\rule{GLR}$; $U$ \textbf{non}-boxed multiset, $V$ non-boxed multiset}
% \UnaryInfC{$U,\Box X\Ra \Box B,V$}
% \DisplayProof
% \end{center}

% The sequent calculus~$\sys{GoS}$ is obtained by replacing~$\rule{GLR}$
% with~$\rule{GoR}$:
% \marginpar{I don't see why V is non-boxed?}
% \begin{center}
% \AxiomC{$\Box X, X, \Box (B \imp  \Box B) \Ra  B$}
% \RightLabel{$\rule{GoR}$; $U$ \textbf{non}-boxed multiset, $V$ non-boxed multiset}
% \UnaryInfC{$U, \Box X \Ra  \Box B, V$}
% \DisplayProof
% \end{center}

\begin{figure}[t]
  \centering
\begin{tabular}{cc}
\AxiomC{$X,X,Y\Ra Z$}
\RightLabel{$\rule{lc}$}
\UnaryInfC{$X,Y\Ra Z$}
\DisplayProof
&
\AxiomC{$X\Ra Y, Z, Z$}
\RightLabel{$\rule{rc}$}
\UnaryInfC{$X\Ra Y, Z$}
\DisplayProof
\\[1em]
\AxiomC{$X\Ra Y$}
\RightLabel{$\rule{w}$}
\UnaryInfC{$U,X\Ra Y,V$}
\DisplayProof
&
\AxiomC{$X\Ra Y,A$}
\AxiomC{$A,U\Ra V$}
\RightLabel{$\rule{cut}$}
\BinaryInfC{$X,U\Ra Y,V$}
\DisplayProof
\end{tabular}
\caption{Structural Rules}
\label{fig:rules-structural}
\end{figure}

In both~$\rule{GLR}$ and~$\rule{GoR}$, the purpose of
restricting~$U$ to a non-boxed multiset is to ensure that all boxed formulae in the
antecedent persist upwards in the semi-derivation via $\Box X$. This will be exploited in the
proof of Lemma~\ref{lem-subsequent} to show that every sequent has a
semi-derivation of maximum height.

A single premise sequent rule is \textit{admissible} in a calculus if the
conclusion is derivable whenever the premise is derivable.  An admissible rule
is \textit{height preserving} if the height of the derivation of the conclusion
is no greater than that of the derivation of the premise.

It is easy to see via a standard proof theoretic induction on height 
that the rules $\rule{lc}$, $\rule{rc}$ of contraction and $\rule{w}$ of
weakening from Figure~\ref{fig:rules-structural} are admissible
%in~$\mathcal{C}$~($\mathcal{C}\in\{\sys{GLS},\sys{GoS}\})$.
in both $\sys{GLS}$ and $\sys{GoS}$. Using these rules, it is easy to establish the following.

\begin{theorem}
  The sequent calculi~$\sys{GLS}+\rule{cut}$ and~$\sys{GoS}+\rule{cut}$ are
  sound and complete for the axiomatically formulated logics~$\sys{GL}$
  and~$\sys{Go}$ respectively.
\end{theorem}

In the sequel we show how to replace~$\sys{GLS}+\rule{cut}$
and~$\sys{GoS}+\rule{cut}$ with~$\sys{GLS}$ and~$\sys{GoS}$, respectively, by
showing how to transform a derivation with cuts into a derivation of the same
end-sequent without cuts. 

% Such an argument was shown for~$\sys{GL}$ **story**
% and~$\sys{Go}$. The feature of our work here is that we are able to obtain the
% results for both logics via a simple and uniform argument. While cut-elimination
% using size of the cut formula and height of the premises is ubiquitous in proofs
% of cut-elimination (starting from Gentzen), Valentini introduced a novel new
% measure called width for~$\sys{GL}$. Brighton gave a new proof for~$\sys{GL}$
% via induction on the size of the cut formula and the maximal height of regress
% trees. Here we finesse the latter argument, fixing some errors in the former and
% also porting the argument to the sequent calculus. Moreover we show how this
% argument extends to~$\sys{Go}$ where the only extant proof ** is highly
% intricate.

% **more story and citations**

While height-preserving contraction suffices for most proof theoretic arguments,
the use of ``maximum height of a semi-derivation of a sequent'' as an induction
parameter requires a more precise result. A rule is 
\textit{perfectly height preserving (php) admissible} if 
the derivations of the conclusion and premise have identical heights.

\begin{lemma}\label{lem-php}
The contraction rule is php-admissible in 
% both $\mathcal{C}$~($\mathcal{C}\in\{\sys{GLS},\sys{GoS}\})$.
both $\sys{GLS}$ and $\sys{GoS}$.
\end{lemma}

\begin{proof}
Induction on the height of a derivation.\marginpar{Will you not need an
  inversion lemma for this ?}
\end{proof}

The \textit{complexity} of a sequent $s$ is the number~$|s|$ of logical connectives in~$s$.
\begin{lemma}\label{lem-subsequent}[semi-derivation maximum height mh]
  In~$\mathcal{C}$~($\mathcal{C}\in\{\sys{GLS},\sys{GoS}\})$, every sequent~$s$
  has a semi-derivation of maximum height, denoted by~$\mh{s}$. Moreover, for
  every rule instance with a premise~$s_{1}$ and conclusion~$s_{0}$:
  $\mh{s_{1}}<\mh{s_{0}}$.
\end{lemma}
\begin{proof}
The proofs for~$\sys{GLS}$ and~$\sys{GoS}$ are almost identical so we only consider $\sys{GL}$.

Certainly for every sequent~$s$, there is a semi-derivation ending with~$s$:
consider the semi-derivation comprising of the single sequent~$s$. To prove the
first claim, we will show that every semi-derivation of~$s$ has height bounded
by a function in~$|s|$.

First note that any boxed formula in the antecedent of a sequent persists in all
sequents above it since no rule removes a formula~$\Box B$ upwards from the
antecedent. This means that the number of $\rule{GLR}$ rules along every branch
is bounded by the number of boxed formulae in s, for otherwise, some branch
would contain two $\rule{GLR}$ rules with the same diagonal formula~$\Box B$ and
hence the conclusion of the upper rule would have the
form~$U,\Box B \Ra \Box B,V$ violating ($\ast$). 

Observe that the complexity of
the premise of a $\rule{GLR}$ rule is at most twice the complexity of the
conclusion: the doubling is because the premise contains~$\Box X,X,\Box B,B$
whenever the conclusion has the form~$\Box X\Ra\Box B$. 
N.B. In the case
  of~$\sys{GoS}$, ``at most twice'' should be replaced by ``at most four times''
  to account for the larger formula~$\Box(B\imp\Box B)$ in the premise.

Next, note that the number of propositional rules that can be applied upwards from a given sequent is finite since each such rule results in a sequent with strictly less complexity. We can bound the number of propositional rules that can occur above a sequent $s'$ by its complexity~$|s'|$.

Putting this all together, and 
bounding the number of boxed formulae in~$s$ by~$|s|$,
%and putting this all together, 
the height of a semi-derivation of a sequent~$s$ in~$\sys{GLS}$ ($\sys{GoS}$) is bounded by below left (resp. below right).
\begin{align*}
|s|\cdot 2|s|\cdot 4|s|\cdot 8|s|\cdots 2^{|s|}\cdot |s|
\qquad\qquad & \qquad\qquad
|s|\cdot 4|s|\cdot 16|s|\cdot 64|s|\cdots 4^{|s|}\cdot |s|
\end{align*}

For the second claim, suppose $s_1/s_0$ is an instance of some rule $\rule{r}$
and let~$d_{\text{max}}$ be a semi-derivation witnessing the maximum height of
the premise~$s_{1}$. Then the semi-derivation obtained from $d_{\text{max}}$ by
applying $\rule{r}$ to its end-sequent is a semi-derivation of~$s_{0}$ with greater height.
\end{proof}

\section{Cut-elimination for~$\sys{GLS}$}


\begin{theorem}[Cut-elimination for~$\sys{GLS}$]\label{thm-CE-GLS}
  The cut rule is eliminable from~$\sys{GLS}$.
\end{theorem}
\begin{proof}
  Without loss of generality, it suffices to eliminate cut from a derivation
  concluding with the cut-rule with cut-free left premise~$X \Ra Y,A$ and
  cut-free right premise~$A, U\Ra V$. We proceed via primary induction (PI) on the size of the
  cut-formula and secondary induction (SI) on the maximum height of the combined
  context~$\mh{X,U\Ra Y,V}$. Now, consider the last rule in each premise. 

If $X \Ra Y, A$ is an instance of \rule{id} because $X \cap Y \neq \emptyset$,
or $A, U \Ra V$ is an instance of \rule{id} because $U \cap V \neq \emptyset$,
then so is $X,U\Ra Y,V$.

If $X \Ra Y, A$ is an instance of \rule{id} because $A \in X$
and $A, U \Ra V$ is an instance of \rule{id} because $A \in V$,
then so is $X,U\Ra Y,V$.

If the cut-formula~$A$ is not principal in either premises of the the last rule,
then the cut is shifted upwards following the usual Gentzen reductions. Of
course, we need to verify that this does not increase the maximum height. To see
that it does not, we illustrate with a generic binary rule $\rule{r}$. Suppose
that the left premise of cut ends as below left, so $A$ is not principal in this
instance of $\rule{r}$:
\begin{center}
\begin{tabular}{cc}
\AxiomC{$X' \Ra  Y', A$}
\AxiomC{$X''\Ra Y'',A$}
\RightLabel{$\rule{r}$}
\BinaryInfC{$X \Ra  Y,A$}
\DisplayProof
&
\AxiomC{$X',U\Ra Y',V$}
\AxiomC{$X'',U\Ra Y'',V$}
\RightLabel{$\rule{r}$}
\BinaryInfC{$X,U \Ra  Y, V$}
\DisplayProof
\end{tabular}
\end{center}
Consider the rule instance of $\rule{r}$ above right, which is what every one of
Gentzen's transformations will produce, with the proviso that the derivations of
the two premises may now contain an instance of cut on $A$. Since the
cut-formulae is still $A$, the size of the cut-formula has not changed. Moreover, from
part two of Lemma~\ref{lem-subsequent}, it follows that
$\mh{X',U \Ra Y', V} < \mh{X,U \Ra Y,V}$ and
$\mh{X'',U \Ra Y'', V} < \mh{X,U \Ra Y,V}$,
which means that we can apply the SIH
to the premises to obtain cut-free derivations of $X',U \Ra Y',V$ and
$X'',U \Ra Y'',V$. Apply~$\rule{r}$ to these to obtain a cut-free derivation
of~$X,U \Ra Y,V$, as shown above right.

If the cut-formula~$A$ is principal in both premises by propositional rules then the usual
Gentzen reductions suffice, since the new cuts are on smaller formulae and hence
the primary induction hypothesis applies. For example
the derivation below containing a cut on $A = B \land C$

\begin{center}
\AxiomC{$X \Ra  Y,B$}
\AxiomC{$X \Ra  Y,C$}
\BinaryInfC{$X \Ra  Y, B \land C$}
%
\AxiomC{$B,C,U\Ra V$}
\UnaryInfC{$B \land C,U\Ra V$}
\BinaryInfC{$X,U\Ra Y,V$}
\DisplayProof
\end{center}
can be transformed to the following containing a cut on the smaller formula $B$:
\begin{center}
\AxiomC{$X\Ra Y,B$}
%
\AxiomC{$X \Ra  Y,C$}
\AxiomC{$B,C,U\Ra V$}
\RightLabel{\rule{cut}}
\BinaryInfC{$B,X,U\Ra Y,V$}
\RightLabel{\rule{cut}}
\BinaryInfC{$X,X,U\Ra Y,Y,V$}
\RightLabel{Contraction Lemma~\ref{lem-php}}
\dashedLine
\UnaryInfC{$X,U\Ra Y,V$}
\DisplayProof
\end{center}
which falls under the PIH, giving a cut-free derivation of 
$X,U\Ra Y,V$.

Finally consider when the cut-formula $A =\Box B$ is principal in both premises:
\begin{center}
\AxiomC{$\Box X, X, \Box B \Ra  B$}
\RightLabel{$\rule{GLR}$}
\UnaryInfC{$L,\Box X \Ra  \Box B,M$}
%
\AxiomC{$\Box B, B, \Box U, U, \Box C \Ra  C$}
\RightLabel{$\rule{GLR}$}
\UnaryInfC{$R, \Box B, \Box U \Ra  \Box C,S$}
%
\RightLabel{\rule{cut}}
\BinaryInfC{$L, R, \Box X,\Box U\Ra \Box C, M, S$}
\DisplayProof
\end{center}
The two $\rule{GLR}$ rule premises give an instance of cut with a smaller
cut-formula $B$.  The PIH gives a cut-free derivation of
$\Box X, X, \Box B, \Box B, \Box U, U, \Box C \Ra C$, and hence by contraction
admissibility, a cut-free derivation of
$\Box X, X, \Box B, \Box U, U, \Box C \Ra C$.

But observe that the left premise can also be derived without weakening in $L$ and
$M$ as shown below left, and that php-contraction on
$\Box X, X, \Box X, \Box U, U, \Box C \Ra  C$
gives 
$L,R, \Box X, \Box U \Ra  \Box C, M,S$
via \rule{GLR} as shown below right:
\begin{center}
  \begin{tabular}[c]{l@{\extracolsep{1cm}}l}
\AxiomC{$\Box X, X, \Box B \Ra  B$}
\RightLabel{$\rule{GLR}$}
\UnaryInfC{$\Box X \Ra  \Box B$}
\DisplayProof
&
\AxiomC{$\Box X, X, \Box X, \Box U, U, \Box C \Ra  C$}
\RightLabel{php-ctr (Lem~\ref{lem-php})}
\dashedLine
\UnaryInfC{$\Box X, X, \Box U, U, \Box C \Ra  C$}
\RightLabel{$\rule{GLR}$}
\UnaryInfC{$L,R, \Box X, \Box U \Ra  \Box C, M,S$}
\DisplayProof
  \end{tabular}
\end{center}
So $\mh{\Box X, X, \Box X, \Box U, U, \Box C \Ra  C} < \mh{L,R, \Box X, \Box U \Ra  \Box C, M, S}$. Applying SIH to $\Box X, X, \Box B, \Box U, U, \Box C \Ra  C$ and $\Box X \Ra  \Box B$ we get a cut-free derivation of $\Box X, X, \Box X, \Box U, U, \Box C \Ra  C$. By contraction admissibility there is a cut-free derivation of $\Box X, X, \Box U, U, \Box C \Ra  C$. Applying~$\rule{GLR}$ we get a cut-free derivation of~$L, R,\Box X, \Box U \Ra  \Box C,M,S$.
\end{proof}

\section{Cut elimination for~$\sys{GoS}$}

If we try to apply directly to~$\sys{GoS}$ the cut-elimination argument for~$\sys{GLS}$, we encounter the following obstacle in the case when~$\Box$ is principal in both premises and we apply the PIH using the premises of each~$\rule{GoS}$ rule:
\begin{center}
\AxiomC{$\Box X, X, \Box(B\imp\Box B) \Ra  B$}
\AxiomC{$\Box B, B, \Box U, U, \Box(C\imp\Box C) \Ra  C$}
\RightLabel{PIH}
\dashedLine
\BinaryInfC{$\Box X, X, \Box(B\imp\Box B), \Box B, \Box U, U, \Box(C\imp\Box C) \Ra  C$}
\DisplayProof
\end{center}
The issue is the occurrence of~$\Box(B\imp\Box B)$ in the antecedent that we did not encounter before.
\marginpar{I don't see the issue?}
To resolve this, we will need a standard invertibility lemma.
\begin{lemma}
If~$X,A\imp B\Ra Y$ is derivable in~$\sys{GoS}$, then so is $X, B \Ra  Y$.
\end{lemma}
\begin{proof}
Induction on the height of the derivation of~$X,A\imp B\Ra Y$.
\end{proof}

The following lemma shows that the occurrence of~$\Box(B\imp\Box B)$ can be removed.
\marginpar{This effectively says that GoR reduces to GLR! That is, every GoS
  derivation can be transformed into a GLS derivation. Now apply the previous
  cut-elimination result and then undo the GLS rules into GoR rules!}

\begin{lemma}\label{lem-GoS-fm-remove}
If $X, \Box (C \imp  \Box C) \Ra  Y$ is derivable in~$\sys{GoS}$, then so is $X, \Box C \Ra  Y$.
\end{lemma}
Induction on the height of the given derivation. 

Base case: If $X\cap Y\neq \emptyset$ then $X,\Box C\Ra Y$ is the required
derivation. 
Otherwise, $Y=Y'\cup \Box(C\imp\Box C)$, so use the following derivation
of $X, \Box C \Ra Y$,
where $X = \Box X_1 \cup U$ with $U$ non-boxed:
\begin{center}
\AxiomC{$\Box C \Ra  \Box C$}
\dashedLine
\RightLabel{$\rule{w}$}
\UnaryInfC{$C, \Box X_1, \Box C,C,\Box((C\imp \Box C)\imp \Box(C\imp \Box C)) \Ra  \Box C$}
\RightLabel{\rule{$\imp$R}}
\UnaryInfC{$\Box X_1, X_1, \Box C, C, \Box((C\imp \Box C)\imp \Box(C\imp \Box C)) \Ra  C\imp \Box C$}
\RightLabel{\rule{GoR}}
\UnaryInfC{$\Box X_1, U, \Box C \Ra  \Box (C\imp \Box C), Y'$}
\DisplayProof
\end{center}
Suppose that the last rule is~$\rule{GoR}$ with
$X = U \cup \Box X_1$ and
$Y = \{\Box B\} \cup V$:
\begin{center}
\AxiomC{$\Box X_1, X_1, \Box (C\imp \Box C), C\imp \Box C, \Box (B \imp  \Box B) \Ra  B$}
\RightLabel{$\rule{GoR}$}
\UnaryInfC{$U, \Box (C\imp \Box C), \Box X_1 \Ra  \Box B, V$}
\DisplayProof
\end{center}
By IH on the premise, we obtain $\Box X_1, X_1, \Box C, C\imp \Box C, \Box (B \imp \Box B) \Ra
B$.
Furthermore, by invertibility of~$\rule{$\imp$l}$ we get
$\Box X_1, X_1, \Box C, \Box C, \Box (B \imp \Box B) \Ra B$. By contraction and
weakening admissibility we get
$\Box X_1, X_1, \Box C, C, \Box (B \imp \Box B) \Ra B$. Now apply~$\rule{GoR}$ to
get $U, \Box X_1, \Box C \Ra \Box B, V$,
which is
$X, \Box C \Ra Y$.

Suppose the last rule is some other generic (binary) rule below.
\begin{center}
\AxiomC{$X', \Box (C\imp \Box C) \Ra  Y'$}
\AxiomC{$X'', \Box (C\imp \Box C) \Ra  Y''$}
\RightLabel{$\rule{r}$}
\BinaryInfC{$X, \Box (C\imp \Box C) \Ra  Y$}
\DisplayProof
\end{center}
Then proceed as follows
\begin{center}
\AxiomC{$X', \Box (C\imp \Box C) \Ra  Y'$}
\RightLabel{IH}
\dashedLine
\UnaryInfC{$X',\Box C\Ra Y'$}
%
\AxiomC{$X'', \Box (C\imp \Box C) \Ra  Y''$}
\RightLabel{IH}
\dashedLine
\UnaryInfC{$X'',\Box C\Ra Y''$}
\RightLabel{$\rule{r}$}
\BinaryInfC{$X, \Box C \Ra  Y$}
\DisplayProof
\end{center}

\begin{theorem}[Cut-elimination for~$\sys{GoS}$] 
The cut rule is eliminable from~$\sys{GoS}$.
\end{theorem}
\begin{proof}
  Once again, without loss of generality, it suffices to eliminate cut from a
  derivation concluding with the cut-rule with cut-free left premise~$X \Ra Y,A$
  and cut-free right premise~$A, U\Ra V$. Primary induction on the size of the
  cut-formula and secondary induction on the maximum height of the combined
  contexts~$\mh{X,U\Ra Y,V}$. The proof is identical to that of
  Theorem~\ref{thm-CE-GLS} except the following case.

Consider the case when the cut formula~$\Box B$ is principal in both premises.
\begin{center}
\AxiomC{$\Box X, X, \Box (B\imp \Box B) \Ra  B$}
\RightLabel{$\rule{GoR}$}
\UnaryInfC{$L,\Box X \Ra  \Box B,M$}
%
\AxiomC{$\Box B, B, \Box U, U, \Box (C\imp \Box C) \Ra  C$}
\RightLabel{$\rule{GoR}$}
\UnaryInfC{$R,\Box B, \Box U \Ra  \Box C,S$}
\BinaryInfC{$L,R,\Box X,\Box U\Ra \Box C,M,S$}
\DisplayProof
\end{center}
By PIH using the premises of each~$\rule{GoR}$ rule, we obtain a cut-free derivation of $\Box X, X, \Box (B\imp \Box B), \Box B, \Box U, U, 
\Box(C\imp \Box C) \Ra$  C. By Lemma~\ref{lem-GoS-fm-remove} we have a cut-free derivation of $\Box X, X, \Box B, \Box B, \Box U, U, 
\Box(C\imp \Box C) \Ra  C$. Hence by contraction admissibility, a cut-free derivation of $\Box X, X, \Box B, \Box U, U, \Box(C\imp \Box C) \Ra  C$. 

Observe that
\begin{center}
\AxiomC{$\Box X, X, \Box X, \Box U, U, \Box(C\imp \Box C) \Ra  C$}
\RightLabel{php contraction (Lem.~\ref{lem-php})}
\dashedLine
\UnaryInfC{$\Box X, X, \Box U, U, \Box(C\imp \Box C) \Ra  C$}
\RightLabel{$\rule{GoR}$}
\UnaryInfC{$L,R\Box X, \Box U \Ra  \Box C,M,S$}
\DisplayProof
\end{center}
So~$\mh{\Box X, X, \Box X, \Box U, U, \Box(C\imp \Box C) \Ra  C} < \mh{L,R,\Box X, \Box U \Ra  \Box C,M,S}$. Applying SIH to $\Box X, X, \Box B, \Box U, U, \Box(C\imp \Box C) \Ra  C$ and $\Box X \Ra  \Box B$ we get a cut-free derivation of $\Box X, X, \Box X, \Box U, U, \Box(C\imp \Box C)\Ra  C$. By contraction admissibility there is a cut-free derivation of $\Box X, X, \Box U, U, \Box(C\imp \Box C) \Ra  C$. Applying~$\rule{GoR}$ we get a cut-free derivation of $\Box X, \Box U \Ra  \Box C$.
\end{proof}

\bibliographystyle{plain}
\bibliography{provability}
\end{document}
