\subsection{The Equivalence of the Deep and Shallow Nested Sequent Calculi}
\label{sec:equiv}

%\subsubsection{From $\biilldn$ to $\biillsn$}
%\paragraph{From $\biilldn$ to $\biillsn$}
%We now show that $\biillsn$ is equivalent to $\biilldn.$
% \subsection{The equivalence between deep and shallow calculi}
% \label{sec:equiv}

% %\subsubsection{From $\biilldn$ to $\biillsn$}
% %\paragraph{From $\biilldn$ to $\biillsn$}
% We now show that $\biillsn$ is equivalent to $\biilldn.$

%In one direction, 
From $\biilldn$ to $\biillsn$, it is enough to show that
every deep inference rule is {\em cut-free derivable} in $\biillsn$.
For the identity and the constant rules, this follows from the fact that hollow structures
can be weakened away, as they add nothing to provability (see App. E).
%\cite{ARXIV}). 
For the other logical rules, a key idea to their soundness 
is that the context splitting operation is derivable in $\biillsn.$ 
This is a consequence of the following lemma (see App. E.1).
%\cite{ARXIV}).

\begin{lemma}
\label{lm:dist}
The following rules are derivable in $\biillsn$ without cut:
$$
\infer[dist_l]
{(\Xc_1, \Xc_2  \seq \Yc_1,\Yc_2), \Uc \seq \Vc}
{
(\Xc_1 \seq \Yc_1), (\Xc_2 \seq \Yc_2), \Uc \seq \Vc
}
\qquad
\infer[dist_r]
{\Uc \seq \Vc, (\Xc_1, \Xc_2  \seq \Yc_1,\Yc_2)}
{
 \Uc \seq \Vc, (\Xc_1 \seq \Yc_1), (\Xc_2 \seq \Yc_2)
}
$$
\end{lemma}
Intuitively, these rules embody
the weak distributivity formalised by the Grishin (b) rule. 
% It is not surprising that these rules are derivable, as they essentially embody
% the weak distributivity principle formalised by the Grishin(b) rule. 

\begin{lemma}
\label{lm:merge}
If $\Xc \in \Xc_1 \merge \Xc_2$ then the rules below are cut-free derivable in $\biillsn$:
$$
\infer[m_l]
{\Xc, \Uc \seq \Vc}
{
\Xc_1, \Xc_2, \Uc \seq \Vc
}
\qquad
\infer[m_r]
{\Uc \seq \Vc, \Xc}
{
\Uc \seq \Vc, \Xc_1, \Xc_2
}
$$
\end{lemma}
\begin{proof}
This follows straightforwardly from Lem.~\ref{lm:dist}.
\end{proof}

\begin{lemma}
\label{lm:context-merge}
Suppose $X[~] \in X_1[~] \merge X_2[~]$ and suppose there exists $Y[~]$
such that for any $\Uc$ 
and any $\rho \in \{drp_1, drp_2, rp_1, rp_2\}$,
the figure below left is a valid inference
rule in $\biillsn$:
\[
\qquad
\qquad\qquad
\infer[\rho]
{X[\Uc]}
{Y[\Uc]}
\qquad\qquad
\infer[\rho]
{X_1[\Uc]}
{Y_1[\Uc]}
\qquad
\qquad
\infer[\rho]
{X_2[\Uc]}
{Y_2[\Uc]}
\]
Then there exists $Y_1[~]$ and $Y_2[~]$ such that
$Y[~] \in Y_1[~] \merge Y_2[~]$ and the second and the third figures above 
are also valid instances of $\rho$ in $\biillsn$.
\end{lemma}
\begin{proof}
This follows from the fact that $X[~]$, $X_1[~]$ and $X_2[~]$ have exactly the same
nested structure, so whatever display rule applies to one also applies to the others. 
\end{proof}

\begin{theorem}
\label{thm:soundness}
If a sequent $X$ is provable in $\biilldn$ then it is cut-free provable in $\biillsn.$
\end{theorem}
\begin{proof}
We show that every rule of $\biilldn$ is cut-free derivable in $\biillsn.$
%% The identity rule $id^d$ is derivable by Lemma~\ref{lm:idd}.
We show here a derivation of the rule $\limp^d_l$; the rest can be proved similarly.
%We construct the derivation bottom up. 
So suppose the conclusion of the rule is $X[\Sc, A \limp B \seq \Tc]$, and the
premises are $X_1[\Sc_1 \seq A, \Tc_1]$ and $X_2[\Sc_2, B \seq \Tc_2]$, where
$X[~] \in X_1[~]\merge X_2[~]$, $\Sc \in \Sc_1 \merge \Sc_2$ and
$\Tc \in \Tc_1 \merge \Tc_2.$
There are two cases to consider, depending on whether $X[~]$ is positive or negative.
We show here the former case, as the latter case is similar. 
Prop.~\ref{prop:display} entails that $X[\Sc, A \limp B \seq \Tc]$ is display equivalent to
$\Uc \seq (\Sc, A \limp B \seq \Tc)$ for some $\Uc$. By Lem.~\ref{lm:context-merge}, we have
$\Uc_1$ and $\Uc_2$ such that
$\Uc \in \Uc_1 \merge \Uc_2$, and $(\Uc_1 \seq \Vc)$ and $(\Uc_2 \seq \Vc)$ 
are display equivalent to, respectively, $X_1[\Vc]$ and $X_2[\Vc]$, for any $\Vc.$
%% \begin{equation}
%% \label{eq:soundness}
%% \Uc_1 \seq \Vc \qquad \equiv \qquad X_1[\Vc]
%% \qquad
%% \mbox{ and }
%% \qquad
%% \Uc_2 \seq \Vc \qquad \equiv \qquad X_2[\Vc]
%% \end{equation}
%% for any $\Vc.$
The derivation of $\limp^d_l$ in $\biillsn$ is thus constructed as follows:
%%  (where doubly-lined
%% inference rules indicate zero or more rule applications):
$$
\infer[\mbox{Prop. \ref{prop:display}}]
{X[\Sc, A \limp B \seq \Tc]}
{
 \infer[rp_1]
 {\Uc \seq (\Sc, A \limp B \seq \Tc)}
 {
  \infer[ml;ml;mr]
  {\Uc, \Sc, A \limp B \seq \Tc}
  {
   \infer[\limp_l]
   {\Uc_1, \Uc_2, \Sc_1, \Sc_2, A \limp B \seq \Tc_1, \Tc_2}
   {
    \infer[rp_2]
    {\Uc_1, \Sc_1 \seq A, \Tc_1}
    {
     \infer[\mbox{Lem. \ref{lm:context-merge}}]
     {\Uc_1 \seq (\Sc_1 \seq A, \Tc_1)}
     {X_1[\Sc_1 \seq A, \Tc_1]}
    }
    & 
    \infer[rp_2]
    {\Uc_2, \Sc_2, B \seq \Tc_2}
    {
     \infer[\mbox{Lem. \ref{lm:context-merge}}]
     {\Uc_2 \seq (\Sc_2, B \seq \Tc_2)}
     {
      X_2[\Sc_2, B \seq \Tc_2]
     }
    }
   }
  }
 }
}
$$
\end{proof}

%\subsubsection{From $\biillsn$ to $\biilldn$}

%We now show the converse direction of the equivalence, i.e., 
%every cut-free derivation of a sequent in $\biillsn$ can be transformed into 
%a cut-free derivation in $\biilldn$ of the same sequent.
%% Since the logical rules and the identity rule of $\biillsn$ are just special cases of
%% their counterparts in $\biilldn$, it is enough to show that structural rules of $\biillsn$
%% are admissible in $\biilldn$.
%This is 

The other direction of the equivalence is proved by a permutation argument: we first add the structural rules to 
$\biilldn$, then we show that these structural rules permute up over all (non-constant) 
logical rules of $\biilldn.$ Then when the structural rules appear just below the $id^d$ or
the constant rules, they become redundant. There are quite a number of cases to consider, but
they are not difficult once one observes the following property of $\biilldn$: 
in every rule, every context in the premise(s) has the same tree structure 
as the context in the conclusion of the rule. This observation takes care of permuting
up structural rules that affect only the context. The non-trivial cases are those where
the application of the structural rules changes the sequent where the logical rule is applied. 
We illustrate a case in the following lemma. The detailed proof 
can be found in App. E.2.
%\cite{ARXIV}.

%% We next show that the structural rules permute up over logical rules (other than the constant-rules) 
%% and propagation rules of $\biilldn$. That is, 
%% if we were to add the structural rules to $\biilldn$, every application of a structural rule
%% below a logical/propagation rule can be replaced by a derivation consisting zero or more application of logical/propagation rules, followed
%% by an application of the same structural rule in each premise of the derivation. 


\begin{lemma}
\label{lm:permute}
The rules $drp_1$, $rp_1$, $drp_2$, $rp_2$, $gl$, and $gr$ permute up over all logical rules of $\biilldn.$
\end{lemma}
\begin{proof}
({\em Outline}) 
We illustrate here %a case involving 
a non-trivial interaction between a structural rule
and $\limp_l$, where the conclusion sequent of $\limp_l$ is changed by 
that structural rule. The other non-trivial cases follow the same pattern, i.e., propagation
rules are used to move the principal formula to the required structural context. 

{\footnotesize
$$
\infer[rp_1]
{\Sc, C \limp B \seq (\Tc \seq \Uc)}
{
\infer[\limp_l]
{\Sc, C \limp B, \Tc \seq \Uc}
{
 {\Sc_1, \Tc_1 \seq C, \Uc_1}
&
 {\Sc_2, \Tc_2 , B \seq  \Uc_2}
}
}
\quad
\leadsto
\quad
\infer[pl_1]
{\Sc, C \limp B \seq (\Tc \seq \Uc)}
{
 \infer[\limp_l]
 {\Sc \seq (C \limp B, \Tc \seq \Uc)}
 {
  \infer[rp_1] 
  {\Sc_1 \seq (\Tc_1 \seq C, \Uc_1)}
  {\Sc_1, \Tc_1 \seq C, \Uc_1}
  &
  \infer[rp_1]
  {\Sc_2 \seq (\Tc_2, B \seq \Uc_2)}
  {\Sc_2, \Tc_2, B \seq \Uc_2}
 }
}
$$
}
\end{proof}

\begin{theorem}
If a sequent $X$ is cut-free $\biillsn$-derivable then it is also $\biilldn$-derivable.
\end{theorem}
% \begin{theorem}
% If a sequent $X$ is derivable in $\biillsn$ then it is also cut-free derivable in $\biilldn$.
% \end{theorem}
%% \begin{proof}
%% By the cut-elimination theorem for $\biillsn$, we only need to consider cut-free derivations
%% of $X$ in $\biillsn.$
%% So let $\Pi$ be a cut-free derivation of $X$ in $\biillsn.$ 
%% By Lemma~\ref{lm:permute}, we can transform $\Pi$ to a derivation in $\biilldn$ by permuting up all the structural rules
%% over logical/propagation rules, starting from the topmost structural rules in $\Pi.$
%% These structural rules eventually disappear when they
%% hit the identity rule $id^d$ or the constant rules $\punit^d_l$ and $\tunit^d_r$; thus we are left
%% with a derivation in $\biilldn.$
%% 
%% \end{proof}

\begin{corollary}\label{cor:dc=dn}
A formula is cut-free $\biilldc$-derivable iff it is $\biilldn$-derivable.
\end{corollary}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% LocalWords: Grishin drp rp mr eg ig gl iff

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "root"
%%% End: 

