
\section{S4}

\subsection{Related Work}
\label{background:S4}
TODO: how much background do we want?

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 are detrimental for automated reasoning and so provides a practical motivation for proving admissibility results for calculus free of such rules.
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}

\cite{Goubault96} acknowledges the problem posed by absorbing Weakening into
the R$\Box$ rule. However, the solutions discussed are given in the context of
typed $\lambda$-calculi for a minimal version of S4, interpreted as 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.

\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 axiom does not require atoms, and that there are only rules for $\Box$ formulae with $\lozenge \varphi$ interpreted as $p_0 \land \lnot p_0$. The rules of the calculus are shown in Figure \ref{S4:rules}.

\begin{figure}[t]
\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
&
    \AxiomC{$\Gamma , \Box \Gamma \vdash \varphi$}
    \LeftLabel{S4$\Box$}
    \UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \varphi, \Delta$}
    \DisplayProof
\end{tabular}
\caption{\label{S4:rules}Sequent calculus 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.
\begin{lstlisting}
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  : "(p, c) : lkbox ==> (p, extend flr c) : gs4_rls"
\end{lstlisting}

\subsection{Results}

\begin{theorem}[\texttt{gs4\_wk\_adm}]
Weakening is admissible for \texttt{gs4\_rls}.
\end{theorem}
\begin{proof}
This follows from the fact that all rules allow arbitrary contexts in their conclusion.
\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.

\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$\Box$ rule.

\begin{itemize}
\item
If the last rule was Refl then $\Gamma = \Gamma', \Box A$ and the original derivation is:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma', A, \Box A \vdash \Delta, \varphi \lor \psi$}
\LeftLabel{Refl}
\UnaryInfC{$\Gamma', \Box A \vdash \Delta, \varphi \lor \psi$}
\DisplayProof{}
\end{center}
Applying the inductive hypothesis on the premises gives a derivation of $\Gamma', A, \Box A \vdash \Delta, \varphi, \psi$. Apply Refl to this gives the required $\Gamma', \Box A \vdash \varphi, \phi, \Delta$.

\item
If the last rule was S4$\Box$ then $\Gamma = \Sigma, \Box \Gamma'$ and $\Delta = \Box A, \Delta'$ and the original derivation looks like:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma', \Box \Gamma' \vdash A$}
\LeftLabel{S4$\Box$}
\UnaryInfC{$\Sigma, \Box \Gamma' \vdash \Box A, \Delta', \varphi \lor \psi$}
\DisplayProof{}
\end{center}
To derive $\Gamma \vdash \varphi, \phi, \Delta$, simply apply a new instance of S4$\Box$ to the original premises, this time with $\varphi, \psi$ as the context instead of $\varphi \lor \psi$:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma', \Box \Gamma' \vdash A$}
\LeftLabel{S4$\Box$}
\UnaryInfC{$\Sigma, \Box \Gamma' \vdash \Box 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 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}.

When the rule above the contraction is an instance of the S4$\Box$ rule, there are two possible cases. Either one or both copies of the contraction-formula exist within the context of the S4$\Box$ rule, or both copies are principal.

In the former case, 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 is (where either $\Box \varphi = A$ or $A \in \Delta$):
\begin{center}
\AxiomC{$\Gamma, \Box \Gamma \vdash \varphi$}
\LeftLabel{S4$\Box$}
\UnaryInfC{$\Sigma, \Box \Gamma \vdash \Box \varphi, A, \Delta$}
\DisplayProof{}
\end{center}

Applying the S4$\Box$ rule without introducing the second copy of $A$ in the context gives a proof of $\Sigma, \Box \Gamma \vdash \Box \varphi, \Delta$ as required (note $A$ is still in the succedent as $\Box \varphi = A$ or $A \in \Delta$). Similarly, if $A$ is in the context $\Sigma$ the new S4$\Box$ rule is then:
\begin{center}
\AxiomC{$\Gamma, \Box \Gamma \vdash \varphi$}
\LeftLabel{S4$\Box$}
\UnaryInfC{$\Sigma - A, \Box \Gamma \vdash \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$\Box$ 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 $\Box B$. The original rule is thus represented by:
\begin{center}
\AxiomC{$B, B, \Box B, \Box B,\Gamma, \Box \Gamma \vdash \varphi$}
\LeftLabel{S4$\Box$}
\UnaryInfC{$\Sigma, \Box B, \Box B, \Box \Gamma \vdash \varphi, \Delta$}
\DisplayProof{}
\end{center}

The copies of $\Box B$ and $B$ can be contracted upon, first using the induction hypothesis on height, and then on rank. The S4$\Box$ rule can then be applied to give the required conclusion.
\begin{center}
\AxiomC{$B, \Box B,\Gamma, \Box \Gamma \vdash \varphi$}
\LeftLabel{S4$\Box$}
\UnaryInfC{$\Sigma, \Box B, \Box \Gamma \vdash \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$\Box$ 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$\Box$ rule on the left, and also principal in either the Refl or the S4$\Box$ rule on the right. As there are all modal rules, the Cut in question must be on a boxed formula, $\Box A$.


%%%%%%%%%% S4 left, refl right %%%%%%%%%%
In the former case, the original Cut has form:

\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash A$}
\LeftLabel{S4$\Box$}
\UnaryInfC{$\Sigma, \Box \Gamma_L \vdash \Delta_L, \Box A$}
    \AxiomC{$\Pi_r$}
    \noLine
    \UnaryInfC{$ A, \Box A, \Gamma_R \vdash \Delta_R$}
    \LeftLabel{Refl}
    \UnaryInfC{$\Box A, \Gamma_R \vdash \Delta_R$}
\LeftLabel{Cut on $\Box A$}
\BinaryInfC{$\Sigma, \Box \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, \Box \Gamma_L \vdash A$}
        \AxiomC{$\Pi_l$}
        \noLine
        \UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash A$}
        \LeftLabel{S4$\Box$}
        \UnaryInfC{$\Sigma, \Box \Gamma_L \vdash \Delta_L, \Box A$}
                \AxiomC{$\Pi_r$}
                \noLine
                \UnaryInfC{$A, \Box A, \Gamma_R \vdash \Delta_R$}
            \RightLabel{Cut on $\Box A$}
            \BinaryInfC{$A, \Sigma, \Box \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
    \RightLabel{Cut on $A$}
    \BinaryInfC{$\Sigma, \Gamma_L, \Box \Gamma_L, \Box \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
    \dashedLine
    \RightLabel{Contraction-admissibility}
    \UnaryInfC{$\Sigma, \Gamma_L, \Box \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
    \LeftLabel{Refl}
    \UnaryInfC{$\Sigma, \Box \Gamma_L, \Gamma_R \vdash \Delta_L, \Delta_R$}
\DisplayProof
\end{center}

Importantly, the new Cut on $\Box 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$\Box$ is principal on both sides, the original Cut has form:

\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash A$}
\LeftLabel{S4$\Box$}
\UnaryInfC{$\Sigma_L, \Box \Gamma_L \vdash \Delta_L, \Box A$}
    \AxiomC{$\Pi_r$}
    \noLine
    \UnaryInfC{$A, \Box A, \Gamma_R, \Box \Gamma_R \vdash B$}
    \LeftLabel{S4$\Box$}
    \UnaryInfC{$\Box A, \Sigma_R, \Box \Gamma_R \vdash \Box B, \Delta_R$}
\LeftLabel{Cut on $\Box A$}
\BinaryInfC{$\Sigma_L, \Sigma_R, \Box \Gamma_L, \Box \Gamma_R \vdash \Box 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, \Box \Gamma_L \vdash A$}
\LeftLabel{S4$\Box$}
\UnaryInfC{$\Sigma_L, \Box \Gamma_L \vdash \Delta_L, \Box A$}
        \AxiomC{$\Pi_r$}
        \noLine
        \UnaryInfC{$A, \Box A, \Gamma_R, \Box \Gamma_R \vdash B$}
    \LeftLabel{Cut on $\Box A$}
    \BinaryInfC{$A, \Sigma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash B, \Delta_L$}
\DisplayProof
\end{center}

Unfortunately, this results in a deduction where we can no longer recover the
$\Box B$ present in the conclusion of the original Cut. The nature of the
calculus and the S4$\Box$ 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 \cite{Troelstra}.

To overcome this issue, without introducing the complications and new branching rule in the solution of \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$\Box$ rule differs from the original by simply not adding any context in the conclusion. Formally, the $\Sigma$ and $\Delta$ of the generic S4$\Box$ rule in Figure \ref{S4:rules} are $\emptyset$ in the new S4$\Box$ instance below:

\begin{center}
\AxiomC{$\Pi_l$}
\noLine
\UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash A$}
        \AxiomC{$\Pi_l$}
        \noLine
        \UnaryInfC{$\Gamma_L, \Box \Gamma_L \vdash A$}
        \LeftLabel{S4$\Box$ (new)}
        \UnaryInfC{$\Box \Gamma_L \vdash \Box A$}
                \AxiomC{$\Pi_r$}
                \noLine
                \UnaryInfC{$A, \Box A, \Gamma_R, \Box \Gamma_R \vdash B$}
            \RightLabel{Cut on $\Box A$}
            \BinaryInfC{$A, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash B$}
    \RightLabel{Cut on $A$}
    \BinaryInfC{$\Gamma_L, \Box \Gamma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash B$}
    \dashedLine
    \RightLabel{Contraction-admissibility}
    \UnaryInfC{$\Gamma_L, \Box \Gamma_L, \Gamma_R, \Box \Gamma_R \vdash B$}
    \LeftLabel{S4$\Box$}
    \UnaryInfC{$\Sigma_L, \Sigma_R, \Box \Gamma_L, \Box \Gamma_R \vdash \Box 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 required. As the combined height of the derivations leading to $\Box \Gamma_L \vdash \Box A$ and $A, \Box A, \Gamma_R, \Box \Gamma_R \vdash B$ is lower than the level of the original Cut, the induction hypothesis on level can be applied.
\end{proof}

