\section{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 \cite{Negri05} and \cite{castellini06} are perhaps the closest representatives in the literature. As noted in Section~\ref{background:S4}, 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 given in \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 $\phi_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:
\[
\AxiomC{$\Gamma , \Box \Gamma \vdash \varphi_i, \Box \Boxesi{i}$}
\LeftLabel{S4.3$\Box$}
\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, or they cannot include top-level Boxes. 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 non-boxed version is preferred as it does not require backtracking.
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{lstlisting}
typedef nboxfml =
"{f::formula. ALL (a::formula). f ~= FC ''Box'' [a]}"
\end{lstlisting}
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}
\begin{figure}[ht]
\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.
"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 overall S4.3 calculus, as an extension of the LK calculus *)
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 (nboxseq flr) c) : gs4_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:
\begin{center}
\AxiomC{$\Pi$}
\noLine
\UnaryInfC{$\Gamma', \Box \Gamma' \vdash \varphi_i, \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, \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, \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}]
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 a 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$}
\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 to produce the following transformation:
\begin{center}
\AxiomC{$\Pi_1$}
\noLine
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \Box \Boxes, A, \Box A$}
\LeftLabel{R-refl}
\UnaryInfC{$\Gamma, \Box \Gamma \vdash \Box \Boxes, A, A$}
\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$}
\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}