\subsection{The Deep Inference Calculus}
\label{sec:deep}


\begin{figure}[t]
{\small

%% $$
%% \infer[id^d]
%% {X[\,Y^l[A] \seq Y^r[A]\,]}{
%% \mbox{
%%   $\begin{array}{c}
%%   X[~] \mbox{ is a hollow context}, \\
%%   Y^l \mbox{ is a left-context} \mbox{ and } 
%%   Y^r \mbox{ is a right-context.}
%%   \end{array}
%%   $
%% }
%% }
%% \infer[cut]
%% {X[\Sc \seq \Tc]}
%% {X_1[\Sc_1 \seq \Tc_1, A] & X_2[\Sc_2, A \seq \Tc_2]}
%% $$

Propagation rules:
%% $$
%% \infer[pl]
%% {X[\Sc, A \seq (\Sc' \seq \Tc'), \Tc]}
%% {
%%  X[\Sc \seq (A, \Sc' \seq \Tc'), \Tc]
%% }
%% \qquad
%% \infer[pr]
%% {X[(\Sc \seq \Tc), \Sc' \seq A, \Tc']}
%% {X[(\Sc \seq \Tc, A), \Sc' \seq \Tc']}
%% $$

$$
\infer[pl_1]
{X[\Sc, A \seq (\Sc' \seq \Tc'), \Tc]}
{
 X[\Sc \seq (A, \Sc' \seq \Tc'), \Tc]
}
\qquad
\infer[pr_1]
{X[(\Sc \seq \Tc), \Sc' \seq A, \Tc']}
{X[(\Sc \seq \Tc, A), \Sc' \seq \Tc']}
$$
$$
\infer[pl_2]
{X[\Sc, (\Sc', A \seq \Tc') \seq \Tc]}
{X[\Sc, A, (\Sc' \seq \Tc') \seq \Tc]}
\qquad
\infer[pr_2]
{X[\Sc \seq \Tc, (\Sc' \seq \Tc', A)]}
{X[\Sc \seq \Tc, A, (\Sc' \seq \Tc')]}
$$

Identity and logical rules: In branching rules, $X[~] \in X_1[~] \merge X_2[~]$,
$\Sc \in \Sc_1 \merge \Sc_2$ and $\Tc \in \Tc_1 \merge \Tc_2$.
$$
\infer[id^d]
{X[\Uc, p \seq p, \Vc]}
{\mbox{$X[~]$, $\Uc$ and $\Vc$ are hollow.}}
\qquad
\infer[\punit_l^d]
{X[\punit, \Uc \seq \Vc]}
{\mbox{$X[~]$, $\Uc$ and $\Vc$ are hollow. }}
\qquad
\infer[\punit_r^d]
{X[\Sc \seq \Tc, \punit]}
{X[\Sc \seq \Tc]}
$$
$$
\infer[\tunit_l^d]
{X[\Sc, \tunit \seq \Tc]}
{X[\Sc \seq \Tc]}
\qquad
\infer[\tunit_r^d]
{X[\Uc \seq \tunit, \Vc]}
{\mbox{$X[~]$, $\Uc$ and $\Vc$ are hollow. }}
$$
$$
\infer[\ltens_l^d]
{X[\Sc, A \ltens B \seq \Tc]}
{X[\Sc, A, B \seq \Tc]}
\qquad
\infer[\ltens_r^d]
{X[\Sc \seq A \ltens B, \Tc]}
{X_1[\Sc_1 \seq A, \Tc_1] & X_2[\Sc_2 \seq B, \Tc_2]}
$$
$$
\infer[\limp_l^d]
{X[\Sc, A \limp B \seq \Tc]}
{
X_1[\Sc_1 \seq A, \Tc_1] & X_2[\Sc_2, B \seq \Tc_2]
}
\qquad
\infer[\limp_r^d]
{X[\Sc \seq \Tc, A \limp B]}
{X[\Sc \seq \Tc, (A \seq B)]}
$$
$$
\infer[\parr_l^d]
{X[\Sc, A \parr B \seq \Tc]}
{
 X_1[\Sc_1, A \seq \Tc_1]
 &
 X_2[\Sc_2, B \seq \Tc_2]
}
\qquad
\infer[\parr_r^d]
{X[\Sc \seq A \parr B, \Tc]}
{X[\Sc \seq A, B, \Tc]}
$$
$$
\infer[\excl_l^d]
{X[\Sc, A \excl B \seq \Tc]}
{X[\Sc, (A \seq B) \seq \Tc]}
\qquad
\infer[\excl_r^d]
{X[\Sc \seq A \excl B, \Tc]}
{X_1[\Sc_1 \seq A, \Tc_1] 
&
 X_2[\Sc_2, B \seq \Tc_2]
}
$$
}
\caption{The deep inference system $\biilldn$. }
% \caption{The deep inference system $\biilldn$. In branching rules, $X[~] \in X_1[~] \merge X_2[~]$,
% $\Sc \in \Sc_1 \merge \Sc_2$ and $\Tc \in \Tc_1 \merge \Tc_2$.}
\label{fig:fbilld}
\end{figure}

A deep inference rule can be applied to any sequent within a nested sequent. This poses a problem
in formalising context splitting rules, e.g., $\ltens$ on the right. To be sound, we need
to consider a context splitting that splits an entire tree of sequents, as formalised next. 

%% A correct formulation of the rules needs to take into account context splitting in branching rules.
%% In the traditinal sequent calculus for linear logic, context splitting is just a partition of
%% the multisets in a sequent. Since a context in our setting is a tree of traditional sequents, 
%% context splitting in our case requires splitting of every sequent in the tree. This is formalised 
%% as follows.

% The {\em merge set of two sequents} $X_1$ and $X_2$, denoted by $X_1
% \merge X_2$, is defined inductively as follows where $Y_i \in P_i
% \merge S_i$, for $1 \leq i \leq m$, and $Z_j \in Q_j \merge T_j$, for $1
% \leq j \leq n$:
%% \item Suppose $X_1 = (\Sc \seq \Tc)$. Then both 
%% $(\Sc, X_2 \seq \Tc)$ and $(\Sc \seq X_2, \Tc)$ are in $X_1 \merge X_2$.
%% \item Suppose $X_2 = (\Sc \seq \Tc)$. Then both 
%% $(\Sc, X_1 \seq \Tc)$ and $(\Sc \seq X_1, \Tc)$ are in $X_1 \merge X_2$.
%% \item Suppose $X_1 = (\Sc, X_1' \seq \Tc)$. Then 
%% $(\Sc, Y \seq \Tc)$ is in $X_1 \merge X_2$, for every $Y \in X_1' \merge X_2.$
%% \item Suppose $X_2 = (\Sc, X_2' \seq \Tc)$. Then 
%% $(\Sc, Y \seq \Tc)$ is in $X_1 \merge X_2$, for every $Y \in X_1 \merge X_2'.$
%% \item Suppose $X_1 = (\Sc \seq X_1', \Tc)$. Then 
%% $(\Sc \seq Y, \Tc)$ is in $X_1 \merge X_2$, for every $Y \in X_1' \merge X_2.$
%% \item Suppose $X_2 = (\Sc \seq X_2', \Tc)$. Then 
%% $(\Sc \seq Y, \Tc)$ is in $X_1 \merge X_2$, for every $Y \in X_1 \merge X_2'.$

Given two sequents $X_1$ and $X_2$, their {\em merge set} $X_1
\merge X_2$ is defined inductively as:
\begin{center}
\begin{tabular}[c]{l@{\extracolsep{2cm}}cl}
% $X_1 \merge X_2 = $
 \multicolumn{3}{l}{
  $X_1 \merge X_2 = \{~ 
   (\Gamma_1, \Gamma_2, Y_1, \dots, Y_m \seq \Delta_1, \Delta_2, Z_1,
    \dots, Z_n) ~\mid$
 }
\\
  & & $X_1 = (\Gamma_1, P_1, \dots, P_m \seq \Delta_1, Q_1,\dots,Q_n)$
  \mbox{ and }
\\
  & & 
  $X_2 = (\Gamma_2, S_1, \dots, S_m \seq \Delta_2, T_1, \dots, T_n)$
 \mbox{ and }
\\
 & &
  $Y_i \in P_i \merge S_i$ for $1 \leq i \leq m$ 
  and $Z_j \in Q_j \merge T_j$ for $1 \leq j \leq n$
  $~\}$
\end{tabular}
\end{center}

% Suppose $X_1 = (\Gamma, P_1, \dots, P_m \seq \Delta, Q_1,\dots,Q_n)$
% and $X_2 = (\Gamma', S_1, \dots, S_m \seq \Delta', T_1, \dots, T_n).$
% Then the sequent 
% $
% (\Gamma, \Gamma', Y_1, \dots, Y_m \seq \Delta, \Delta', Z_1, \dots, Z_n)
% $
% is in $X_1 \merge X_2$, where $Y_i \in P_i \merge S_i$, for $1 \leq i \leq m$,
% and $Z_j \in Q_j \merge T_j$, for $1 \leq j \leq n.$

Note that the merge set of two sequents may not always be defined
since mergeable sequents need to have the same structure.
%up to
%associativity and commutativity of the structural connective comma.
%`,'. 
Note also that, because there can be more than one way to enumerate
elements of a multiset in the left/right hand side of a sequent, 
the result of the merging of two nested sequents is a set, rather
than a single nested sequent. 
When
$X \in X_1 \merge X_2$, we say that $X_1$ and $X_2$ are a {\em
  partition} of $X.$ Fig.~\ref{fig:partition} (ii) and (iii) show a partitioning
of the nested sequent~\eqref{eq:1}
in the tree representation.
% $$
% (e,f \seq g), (p, (u,v \seq x,y) \seq q,r), a, b \seq c, d, (\cdot \seq s), 
% $$
%% can be partitioned into %the following nested sequents:
%% $$
%% (e \seq g), (p, (u \seq x) \seq \cdot ), a \seq c, (\cdot \seq \cdot)
%% $$
%% and 
%% $
%% (f \seq \cdot), ( (v \seq y) \seq q,r), b \seq  d, (\cdot \seq s).
%% $
%% Figure~\ref{fig:partition} shows this
%% partitioning in the tree representation. 
Note that the partitions (ii) and (iii) must have the same tree
structure as the original sequent (i).
%% \qed
%% \end{example}

%% Obviously, every sequent has at least one partition, i.e., the sequent itself and the
%% empty sequent $\sunit \seq \sunit$, and can have more than 
%% one partition. 

Given two contexts
$X_1[~]$ and $X_2[~]$ 
their merge set $X_1[~] \merge X_2[~]$
is defined as follows:

  \begin{tabular}[c]{lcl}
  \multicolumn{3}{l}{  
     If $X_1[~] = [~]$ and $X_2[~] = [~]$ 
     then $X_1[~] \merge X_2[~] = \{ [~] \}$
   }
\\
    If $X_1[~]$ & $=$ &
          $(\Gamma_1, Y_1[~], P_1,\dots,P_m \seq \Delta_1, Q_1,\dots,Q_n)$
    and
\\
    \hphantom{If} $X_2[~]$ & $=$ &
          $(\Gamma_2, Y_2[~], S_1,\dots,S_m \seq \Delta_2, T_1,\dots,T_n)$
   then
\\
   $X_1[~] \merge X_2[~]$ & $=$ &
      $\{~ (\Gamma_1, \Gamma_2, Y[~], U_1,\dots,U_m \seq \Delta_1,\Delta_2,
          V_1,\dots,V_n)~~ \mid$
\\
   & &
        $
        \begin{array}{l} 
         Y[~] \in Y_1[~]\merge Y_2[~] 
        \mbox{ and }
        U_i \in P_i \merge S_i 
        \mbox{ for } 
        1 \leq i \leq m
        \mbox{ and } \\
        V_j \in Q_j \merge T_j
        \mbox{ for } 
        1 \leq j \leq n 
       ~\}
        \end{array}$
%  \end{tabular}
\\
%  \begin{tabular}[c]{lcl}
    If $X_1[~]$ & $=$ & $(\Gamma_1, P_1,\dots,P_m \seq \Delta_1, Y_1[~], Q_1,\dots,Q_n)$
    and
    \\
    \hphantom{If} $X_2[~]$ & $=$ & $(\Gamma_2, S_1,\dots,S_m \seq \Delta_2, Y_2[~], T_1,\dots,T_n)$
    then
    \\
    $X_1[~] \merge X_2[~]$ & $=$ & 
    $\{~
      (\Gamma_1, \Gamma_2, U_1,\dots,U_m \seq \Delta_1,\Delta_2, Y[~],
       V_1,\dots,V_n)$ $\mid$
    \\
     & &
    $\begin{array}{l}
     Y[~] \in Y_1[~]\merge Y_2[~] \mbox{ and }
     U_i \in P_i \merge S_i \mbox{ for } 1 \leq i \leq m \mbox{ and }\\
     V_j \in Q_j \merge T_j$ for $1 \leq j \leq n ~\}
     \end{array}
    $
  \end{tabular}

If $X[~] = X_1[~] \merge X_2[~]$ we say $X_1[~]$ and $X_2[~]$
are a {\em partition} of $X[~]$.

% The {\em merge set $X_1[~] \merge X_2[~]$ of two contexts} 
% % of the same type (i.e., they are either both positive or both negative) 
% $X_1[~]$ and $X_2[~]$, is defined as follows:
% \begin{itemize}
% \item If $X_1[~] = [~]$ and $X_2[~] = [~]$ then $X_1[~] \merge X_2[~] = \{ [~] \}.$
% \item Suppose $X_1[~] = (\Gamma, X_1'[~], P_1,\dots,P_m \seq \Delta, Q_1,\dots,Q_n)$ 
% and $$X_2[~] = (\Gamma', X_2'[~], S_1,\dots,S_m \seq \Delta', T_1,\dots,T_n).$$
% Then 
% $
% (\Gamma, \Gamma', Y[~], U_1,\dots,U_m \seq \Delta,\Delta', V_1,\dots,V_n)
% \in X_1[~] \merge X_2[~]$, where
% $Y[~] \in X_1'[~]\merge X_2'[~]$, $U_i \in P_i \merge S_i$, for $1 \leq i \leq m$,
% and $V_j \in Q_j \merge T_j$, for $1 \leq j \leq n.$

% \item Suppose $X_1[~] = (\Gamma, P_1,\dots,P_m \seq \Delta, X_1'[~], Q_1,\dots,Q_n)$ 
% and $X_2[~] = (\Gamma', S_1,\dots,S_m \seq \Delta', X_2'[~]T_1,\dots,T_n).$
% Then 
% $
% (\Gamma, \Gamma', U_1,\dots,U_m \seq \Delta,\Delta', Y[~], V_1,\dots,V_n)
% \in X_1[~] \merge X_2[~]$, where
% $Y[~] \in X_1'[~]\merge X_2'[~]$, $U_i \in P_i \merge S_i$, for $1 \leq i \leq m$,
% and $V_j \in Q_j \merge T_j$, for $1 \leq j \leq n.$
% \end{itemize}
%We say that $X_1[~]$ and $X_2[~]$ are {\em composable} if 
%their merge set is defined. 

We extend the notion of a merge set between multisets of formulae and sequents
as follows. Given 
$
\Xc = \Gamma \cup \{X_1,\dots,X_n\}
$
and
$
\Yc = \Delta \cup \{Y_1,\dots,Y_n\} 
$
their merge set contains all multisets of the form:
$
\Gamma \cup \Delta \cup \{Z_1,\dots,Z_n\}
$
where $Z_i \in X_i \merge Y_i.$
%% $\Xc$ and $\Yc$, the multiset 
%% $$
%% \Xc' \cup \Yc' \cup \{R_1,\dots,R_n\}
%% $$
%% for some $n \geq 0$, is an element of $\Xc \merge \Yc$ if and only if
%% there exist $\{P_1,\dots,P_n \} \subseteq \Xc$
%% and $\{Q_1,\dots,Q_n\} \subseteq \Yc$ such that 
%% \begin{itemize}
%% \item $R_i \in P_i \merge Q_i$ for every $1 \leq i \leq n$, and
%% \item $\Xc' = \Xc \setminus \{P_1,\dots,P_n\}$
%% and $\Yc' = \Yc \setminus \{Q_1,\dots,Q_n\}.$
%% \end{itemize}
%% In other words, elements of $\Xc \merge \Yc$ are obtained from 
%% compositions and multiset unions of selected subsets of $\Xc$ and $\Yc$. 
%% Note that in particular the multiset union of $\Xc \cup \Yc$ is
%% in the merge set $\Xc \merge \Yc$. 

%% The {\em merge set} of two sequents $X_1$ and $X_2$, denoted by $X_1 \merge X_2$,
%% is defined inductively as follows: 
%% Suppose $X_1$ and $X_2$ are, respectively, 
%% $$
%% \Sc_1, U_1, \dots, U_m \seq \Tc_1, V_1,\dots,V_n
%% $$
%% and
%% $$
%% \Sc_2, Y_1, \dots, Y_m \seq \Tc_2, Z_1, \dots, Z_n.
%% $$
%% Then any sequent $X$ of the form
%% $$
%% \Sc_1,\Sc_2, S_1,\dots,S_m, \seq \Tc_1,\Tc_2, T_1, \dots, T_n
%% $$
%% where $S_i \in U_i \merge Y_i$ and $T_j \in V_j \merge Z_j$, is in $X_1 \merge X_2.$
%% If $X_1$ and $X_2$ are not of the form given above, then $X_1 \merge X_2 = \sunit.$

%% Merging of contexts are defined similarly. The {\em merge set} of 
%% two contexts $X_1[~]$ and $X_2[~]$, denoted by $X_1[~] \merge X_2[~]$, 
%% is defined as follows:
%% \begin{itemize}
%% \item If $X_1[~] = [~]$ and $X_2[~] = [~]$ then $X_1[~] \merge X_2[~] = \{[~]\}.$
%% \item If $X_1[~]$ and $X_2[~]$ are, respectively, 
%% $$
%% \Sc_1, U_1, \dots, U_m, X_1'[~] \seq \Tc_1, V_1,\dots,V_n
%% $$
%% and
%% $$
%% \Sc_2, Y_1, \dots, Y_m, X_2'[~] \seq \Tc_2, Z_1, \dots, Z_n
%% $$
%% then any context $X[~]$ of the following form is in $X_1[~] \merge X_2[~]$:
%% $$
%% \Sc_1,\Sc_2, S_1,\dots,S_m, X'[~] \seq \Tc_1,\Tc_2, T_1, \dots, T_n
%% $$
%% where $S_i \in U_i \merge Y_i$ and $T_j \in V_j \merge Z_j$ and $X'[~] \in X_1'[~] \merge X_2'[~].$

%% \item If $X_1[~]$ and $X_2[~]$ are, respectively, 
%% $$
%% \Sc_1, U_1, \dots, U_m \seq \Tc_1, V_1,\dots,V_n, X_1'[~]
%% $$
%% and
%% $$
%% \Sc_2, Y_1, \dots, Y_m \seq \Tc_2, Z_1, \dots, Z_n, X_2'[~]
%% $$
%% then any context $X[~]$ of the following form is in $X_1[~] \merge X_2[~]$:
%% $$
%% \Sc_1,\Sc_2, S_1,\dots,S_m \seq \Tc_1,\Tc_2, T_1, \dots, T_n, X'[~]
%% $$
%% where $S_i \in U_i \merge Y_i$ and $T_j \in V_j \merge Z_j$ and $X'[~] \in X_1'[~] \merge X_2'[~].$

%% \item $X_1[~] \merge X_2[~] = \sunit$ in all other cases. 
%% \end{itemize}

A nested sequent $X$ (resp. a context $X[~]$) 
is said to be {\em hollow} iff it contains no occurrences of formulae.
%Similarly, a context $X[~]$ is said to be {\em hollow} iff $X[~]$ contains no occurrences of formulae. 
For example, %$[~]$ is a hollow context, and so is 
$(\sunit \seq \sunit) \seq (\sunit \seq [~]), (\sunit \seq \sunit)$ is a hollow context.

The deep inference system for $\biill$, called $\biilldn$, 
is given in Fig.~\ref{fig:fbilld}. 
Fig.~\ref{fig:bierman-deep} shows a cut-free derivation of Bierman's example in $\biilldn.$
%\begin{example}
%% A proof in $\biilldn$ of the Bierman example is given below, where
%% principal formulas are typeset in bold fonts.

\begin{figure}
{\footnotesize
$$
\infer[\limp_r^d]
{(a \parr b) \parr c \seq a, \mathbf{(b \parr c \limp d) \parr e \limp d \parr e} }
{
 \infer[\parr_r^d]
 { (a \parr b) \parr c \seq a, ((b \parr c \limp d) \parr e \seq \mathbf{d \parr e})}
 {
  \infer[\parr_l^d]
  { (a \parr b) \parr c \seq a, (\mathbf{(b \parr c \limp d) \parr e} \seq d, e)}
  {
   \infer[\limp_l^d]
   {(a \parr b) \parr c \seq a, (\mathbf{b \parr c \limp d} \seq d)} 
   {
    \infer[\parr_r^d]
    {(a \parr b) \parr c \seq a, (\sunit \seq \mathbf{b \parr c})} 
    {
     \infer[\parr_l^d]
     {\mathbf{(a \parr b) \parr c} \seq a, (\sunit \seq b, c)} 
     {
      \infer[\parr_l^d]
      {\mathbf{a \parr b} \seq a, (\sunit \seq b)}
      {
        \infer[id^d]
        {a \seq a, (\sunit \seq \sunit)}
        { }
        &
        \infer[pl_1]
        {b \seq (\sunit \seq b)}
        {
           \infer[id^d]
           {\sunit \seq (b \seq b)}{}
        }
      }
      &
      \infer[pl_1]
      {c \seq (\sunit \seq c)}
      {
       \infer[id^d]
       {\sunit \seq (c \seq c)}
       {}
      }
     }
    }
    &
    \!\!
    \infer[id^d]
    {\sunit \seq (d \seq d)}
    {}
   }
   &
   \infer[id^d]
   { \sunit \seq (e \seq e)}
   {}
  }
 } 
}
$$
}
\caption{A cut-free derivation of Bierman's example in $\biilldn$.}
\label{fig:bierman-deep}
\end{figure}
%\qed
%\end{example}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% LocalWords: mergeable eq lcl iff

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

