\section{Free-cut elimination in linear logic}
\label{sect:free-cut-elim}
\todo{include some bounds on free-cut elimination? Look at paper "Corrected upper bounds for free-cut elimination" by Beckmann and Buss for comparison.}

 While in plain logical systems such as linear logic cut rules can be eliminated, this is in general not the case anymore when one considers extension with a theory $\mathcal T$ . For this reason we need now to define the kind of cuts that  will remain in proofs after reduction. We will call these \textit{anchored cuts}. 
  
  Our first idea would be to consider as anchored  a cut whose cut-formulas  $A$ in the two premises are both principal for their rule, and at least one of these rules is non-logical. Now, the problem with this tentative definition is that a rule (R) of  $\mathcal T$ can contain several principal formulas  (in $\Sigma'$, $\Delta'$) and so we would like to allow an anchored cut on each of these principal formulas. Consider for instance the following derivation, where we have underlined principal formulas:
  \patrick{Anupam, could you please display this derivation in a suitable way?}
  \[
  \vlderivation{
\vliin{cut_2}{}{ \seqar  \Delta}{
\vliin{cut_1}{}{\seqar A_2 }{\vlin{\rigrul{\lor}}{}{\seqar \underline{A_1}}{}}{\vliin{(R)}{}{\underline{A_1}\seqar \underline{A_2}}{}{} }
}{
\vliin{\lefrul{\land}}{}{\underline{A_2}\seqar \Delta}{}{}
}
}
\]
  Here $cut_1$ is anchored in this sense, but not $cut_2$. 
  Therefore we consider a more general definition:
    \begin{definition}\label{def:anchoredcut}
  We define in a mutual inductive way the notion of \textit{hereditarily principal formula} and \textit{anchored cut} in a $\mathcal T$-proof :
  \begin{itemize}
  \item A formula $A$ in a sequent $\Gamma \seqar \Delta$ is \textit{hereditarily principal} for a rule (S), if either (i) the sequent is conclusion of the rule (S) and $A$ is principal in it, or 
(ii)  the sequent is conclusion of an anchored cut,  the direct ancestor of $A$ in the corresponding premise is hereditarily principal for the rule (S), and the rule (S) is non-logical.
  \item An instance of cut rule is an \textit{anchored cut} if  either its cut-formulas $A$ in the two premises are both hereditarily principal for non-logical rules, or one is hereditarily principal for a non-logical rule and the other one is principal for a logical rule.
  \end{itemize}
  \end{definition}
%  Observe that by this definition if a formula $A$ in a sequent is hereditarily principal for a rule (S) which is a logical rule, then the sequent is conclusion of this rule (S) and $A$ is principal for this rule.  The generalization from principal formula to hereditarily principal formula is really made for non-logical rules (R).
  So as a consequence of this definition, an anchored cut on a formula $A$ is of the following form:
  \begin{itemize}
  \item at least one of the two premises of the cut has above it a sub-branch of the proof which starts (top-down) with a non-logical rule (R) with $A$ as one of its principal formulas, and then a sequence of anchored cuts  in which $A$ is part of the context;
  \item the other premise is either of the same form, or a logical rule with principal formula $A$. 
  \end{itemize}
  
%  Now, for instance a cut on a (principal) formula $A \lor B$ between a rule $\rigrul{\lor}$ and a rule (R) (where  $A \lor B$ occurs in $\Sigma'$) is anchored, while a cut between 
%  a rule $\rigrul{\lor}$ and a rule $\lefrul{\lor}$ is not.
   
   A cut which is not anchored will also be called a \textit{free-cut}.
  
  With this new definition both $cut_1$ and $cut_2$ in the previous example are anchored.
   
   \patrick{@Anupam: if we need to shorten this part, I think we should anyway keep the key lemmas \ref{lem:hereditaryprincipalnonlogical} and \ref{lem:keycommutations}.  In the proof of the thm itself, I would give priority to keep the first case, maybe by skipping the first situation and keeping the second item, $S_1$=$!r$, $?l$ or $R$. Second case could be kept too, and third case could be briefly summarized and pushed in the appendix or online version.}
   
   Let us first prove a key lemma on hereditarily principal formulas:
   \begin{lemma}\label{lem:hereditaryprincipalnonlogical}
   A formula occurrence $A$ on the l.h.s. (resp. r.h.s.) of a sequent and hereditarily principal for a non-logical rule (R) 
   cannot be of the form $A=?A'$ (resp. $A=!A'$).
   \end{lemma}
   \begin{proof}
   Assume that $A$ is an occurrence of formula on the l.h.s. of the sequent and hereditarily principal for a non-logical rule (R), then a direct ancestor of this formula is principal for (R) and thus by condition 4. $A$ cannot be of the form $?A'$. The other case is identical.
   \end{proof}
   
   Now we can state the main result of this section:
   \begin{theorem}
   \label{thm:free-cut-elim}[Free-cut elimination]
    Given a theory  $\mathcal{T}$, any  $\mathcal T$-proof $\pi$ can be transformed into a $\mathcal T$-proof $\pi'$ with same conclusion sequent and without any free-cut.
   \end{theorem}
    The proof will be given below. It will proceed in a way similar to the classical proof of cut elimination for linear logic, but here for eliminating only free-cuts, and we will have to check that all steps of the reasoning are compatible with the fact that the proof here also contains $\mathcal{T}$ rules. Define the \textit{degree} of a formula as the number of logical connectives or quantifiers in it.  Let us first state an easy building-block of the proof:
    \begin{lemma}[Logical non-exponential cut-elimination steps]\label{lem:logical steps}
    Any cut $c$ whose cut-formulas $A$ are both principal formulas of logical rules distinct from $?$, $!$, $wk$, $cntr$ rules can be replaced in one step by cuts on formulas of strictly lower degree (0, 1 or 2 cuts).
    \end{lemma}
    \begin{proof}
    This is exactly as in plain linear logic. Just note that the case of a quantifier formula involves a substitution by a term $t$ throughout the proof, and this is where we need condition 3 on non-logical rules requiring that they are closed by substitution.
    \end{proof}
    Actually the most important part of the proof of Thm \ref{thm:free-cut-elim} will be the handling of the commutation steps, since this is where the new non-logical rules could raise some problems.
     
     First, observe that the only rules in which there is a condition on the context are the following ones: $(\rigrul{\forall})$, $(\lefrul{\exists})$, $(\rigrul{!})$, $(\lefrul{?})$, $(R)$. These are thus the rules for which the commutation with cut steps are not straightforward. Commutations with logical rules  other than $(\rigrul{!})$, $(\lefrul{?})$ are done in the standard way, as in plain linear logic:
     \begin{lemma}[Standard commutations]\label{lem:standardcommutations}
     Any logical rule  distinct from $(\rigrul{!})$, $(\lefrul{?})$ can be commuted top-down with any cut $c$. If the logical rule is binary this will produce two cuts.
     \end{lemma}
    (Just remind that for  $(\rigrul{\forall})$, $(\lefrul{\exists})$ rules this can involve renaming of eigenvariables if necessary.)
    
     In the following we will need to be more careful about rules $(\rigrul{!})$, $(\lefrul{?})$, $(R)$. For that we establish our second key lemma:
  \begin{lemma}[Key commutations]\label{lem:keycommutations}
     A cut of the following form, where $?A$ is non principal for $(R)$, can be commuted with the $(R)$ rule:
 \[
     \vliinf{cut}{}{ !\Gamma', \Gamma,  \Sigma'   \seqar \Delta', ?A, ?\Pi, ?\Pi'}
                    { \vlinf{(R)}{}{!\Gamma, \Sigma'  \seqar \Delta', ?A, ?\Pi}{  \{ !\Gamma, \Sigma_i  \seqar \Delta_i, ?A, ?\Pi \}_{i\in I} } }
                    {  \vlinf{}{}{?A, !\Gamma' \seqar  ?\Pi'}{} } 
\]
    Similarly if $(R)$ is replaced with $(\rigrul{!})$, with $?A$ in its r.h.s. context. Similarly also for the symmetric situations:
    cut on the l.h.s. of the conclusion of an $(R)$ or a $(\lefrul{?})$ rule on a (non-principal) formula $!A$, with a sequent $!\Gamma' \seqar  ?\Pi', !A$.
  \end{lemma}  
     \begin{proof}
     The first subderivation can be replaced by:
      \[
     \vlinf{(R)}{}{ !\Gamma', !\Gamma,  \Sigma'   \seqar \Delta', ?\Pi, ?\Pi'}
                                 { \vliinf{cut}{}{\{!\Gamma', !\Gamma, \Sigma_i  \seqar \Delta_i, ?\Pi,?\Pi' \}_{i\in I}} { \vlinf{}{}{ !\Gamma, \Sigma_i  \seqar \Delta_i, ?A, ?\Pi}{}} {  \vlinf{}{}{?A, !\Gamma' \seqar  ?\Pi'}{} } }
                                 \]
     Here if an eigenvariable in $\Sigma_i, \Delta_i$ happens to be free in $!\Gamma', ?\Pi'$ we rename it to avoid the collision, which is possible because by condition 2 on non-logical rules these eigenvariables do not appear in $\Sigma', \Delta'$ or $!\Gamma, ?\Pi$. So the occurrence of $(R)$ in this new subderivation is valid.
     
     Similarly  for the symmetric derivation with a   cut on the l.h.s. of the conclusion of an $(R)$ on a formula $!A$.
     The analogous situations with rules  $(\rigrul{!})$ and $(\lefrul{?})$ are handled in the same way, and were already known in linear logic.
     \end{proof}
     Now we have all the necessary lemmas to proceed with the proof of the theorem.
    \begin{proof} (of Thm  \ref{thm:free-cut-elim})
    Given a cut rule $c$ in a proof $\pi$, we call  \emph{degree} $\deg( c)$  the degree of its  cut-formula. Now the \emph{degree} of the proof $\deg( \pi)$ is the multiset of the degrees of its non-anchored formulas. The degrees will be compared with the multiset ordering.
    
    The demonstration will proceed by induction on the degree  $\deg( \pi)$.  For a given degree we will proceed with a sub-induction on the \textit{height} $\height{\pi}$ of the proof.
    
    Consider a proof $\pi$ of non-null degree. We will show how to reduce it to a proof of strictly lower degree. Consider a top-most non-anchored cut $c$ in $\pi$, that is to say such that there is no non-anchored cut above $c$.  Let us call $A$ the cut-formula, and $(S_1)$ (resp. $(S_2)$) the rule above the left (resp. right) premise of $c$.  
\[    
     \vliinf{c \; \; \cut}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \vlinf{S_1}{}{\Gamma \seqar \Delta, A}{} }{\vlinf{S_2}{}{\Sigma, A \seqar \Pi}{}}
\]
    Intuitively we will proceed as follows: if $A$ is not hereditarily principal in one of its premises  we will try to commute $c$ with the rule along its left premise  $(S_1)$, and if it is not possible commute it   with the rule along its right premise  $(S_2)$; if $A$ is hereditarily principal in both premises we will proceed with a cut-elimination step. So let us distinguish  three cases:
    
   \begin{itemize}
    \item \textbf{First case}: the cut-formula $A$ on the l.h.s. of  $c$ is non hereditarily principal. 
    
\begin{itemize}
\item Consider first the situation where $(S_1)$ is not one of the rules $(\rigrul{!})$, $(\lefrul{?})$, $(R)$.

In this case the commutation of $c$ with $(S_1)$ can be done in the usual way, by using Lemma \ref{lem:standardcommutations}. Let us handle as an example the case where $(S_1)=(\rigrul{\laand})$.
{\small
\[
\vlderivation{
\vliin{c}{}{ \Gamma, \Sigma \seqar B_1\vlan B_2, \Delta, \Pi }{ \vliin{S_1=\rigrul{\vlan}}{}{\Gamma  \seqar B_1\vlan B_2, \Delta, A}{ \vlhy{\Gamma  \seqar B_1, \Delta, A} }{\vlhy{\Gamma  \seqar  B_2,\Delta, A}}}{ \vlhy{ \Sigma, A \seqar  \Pi} }
}
\quad\to\quad
\vlderivation{
\vliin{\rigrul{\vlan}}{}{  \Gamma, \Sigma \seqar B_1\vlan B_2, \Delta, \Pi  }{
\vliin{c_1}{}{\Gamma,\Sigma \seqar B_1, \Delta, \Pi }{ \vlhy{\Gamma  \seqar B_1, \Delta, A} }{\vlhy{ \Sigma, A \seqar  \Pi} }
}{
\vliin{c_2}{}{\Gamma,\Sigma \seqar B_2, \Delta, \Pi }{ \vlhy{\Gamma  \seqar B_2, \Delta, A} }{\vlhy{ \Sigma, A \seqar  \Pi} }
}
}
\]
}
%\vlderivation{
%\vliin{\vlan}{}{\Gamma,\Delta,A\vlan B }{
%\vliin{c_1}{}{\Gamma,\Delta,A }{ \vlhy{\Gamma,A,C} }{ \vlhy{ \Delta,C^\bot } }
%}{
%\vliin{ c_2 }{}{\Gamma,\Delta,B}{ \vlhy{\Gamma,B,C } }{ \vlhy{\Delta,C^\bot} }
%}
%}
%\]


Observe that here $c$ is replaced by two cuts $c_1$ and $c_2$. Call $\pi_i$ the sub-derivation of last rule $c_i$, for $i=1,2$. As for $i=1, 2$ we have
$\deg{\pi_i}\leq \deg{\pi}$ and $\height{\pi_i}< \height{\pi}$ we can apply the induction hypothesis, and reduce $\pi_i$ to a proof $\pi'_i$ of same conclusion and with
$\deg{\pi'_i} < \deg{\pi_i}$. Therefore  by replacing $\pi_i$ by $\pi'_i$ for $i=1, 2$ we obtain a proof $\pi'$ such that $\deg{\pi'}<\deg{\pi}$.  

The case (S)=($\lefrul{\laor}$) is identical, and the other cases are similar. % (see the Appendix for more examples). 

\item Consider now the case where $(S_1)$ is equal to $(\rigrul{!})$, $(\lefrul{?})$ or $(R)$. Let us also assume that the cut-formula is hereditarily principal in its r.h.s. premise, because if this does not hold we can move to the second case below. 

First consider  $(S_1)=(\rigrul{!})$. As $A$ is not principal in the conclusion of $(\rigrul{!})$ it is of the form $A=?A'$. By assumption we know that  $A=?A'$ in the conclusion of $(S_2)$ is hereditarily principal on the l.h.s., so by Lemma \ref{lem:hereditaryprincipalnonlogical} it cannot be hereditarily principal for a non-logical rule, so by definition of hereditarily principal we deduce that $(S_2)$ is not an $(R)$ rule. It cannot be an  $(\rigrul{!})$ rule either because then $?A'$ could not be a principal formula in its conclusion. Therefore the only possibility is that 
 $(S_2)$ is an  $(\lefrul{?})$ rule. So the r.h.s. premise is of the shape $?A',!\Gamma' \seqar ?\Pi'$ and by Lemma \ref{lem:keycommutations} the commutation on the l.h.s. is possible. We can conclude as previously. The case where  $(S_1)=(\lefrul{?})$ is the same.
 
 Now consider the case where $(S_1)=(R)$.  As $A$ is not hereditarily principal in the conclusion of $(R)$, it is a context formula and it is on the r.h.s., so by definition of $(R)$ rules it is  the form $A=?A'$. So as before by Lemma \ref{lem:hereditaryprincipalnonlogical} we deduce that   $(S_2)=(\lefrul{?})$, and  so the r.h.s. premise is of the shape $?A',!\Gamma' \seqar ?\Pi'$.  By Lemma \ref{lem:keycommutations} the commutation on the l.h.s. is possible, and so again we conclude as previously.
 \end{itemize}
    \item \textbf{Second case}: the cut-formulas on the l.h.s. and r.h.s. of  $c$ are both non hereditarily principal. 
    
   After the first case we are here left with the situation where  $(S_1)$ is equal to $(\rigrul{!})$, $(\lefrul{?})$ or $(R)$.
   \begin{itemize}
    \item Consider the case where  $(S_1)$=$(\rigrul{!})$, $(\lefrul{?})$, so $A$ is of the form $A=?A'$. All cases of commutation of $c$ with $(S_2)$ are as in standard linear logic, except if $(S_2)=(R)$. In this case though we cannot have $A=?A'$ because of the shape of rule $(R)$. So we are done. 
    \item Consider  $(S_1)=(R)$. Again as $A$ is not principal in the conclusion of $(S_1)$ and on the r.h.s. of the sequent it is a context formula, and thus of the form  $A=?A'$. As $?A'$ is not principal in the conclusion of $(S_2)$, it is thus a context formula on the l.h.s. of sequent, and therefore $(S_2)$ is not a rule $(R)$. So $(S_2)$ is a logical rule. If it is not an $(\rigrul{!})$ or an $(\lefrul{?})$ it admits commutation with the cut, and we are done. If it is equal to $(\rigrul{!})$ or $(\lefrul{?})$ it cannot have $?A'$ as a context formula in the l.h.s. of its conclusion, so these subcases do not occur.  
   \end{itemize}
 
   
    \item \textbf{Third case}: the cut-formulas on the l.h.s. and r.h.s. of  $c$ are both  hereditarily principal.
     
    By assumption $c$ is non anchored, so none of the two cut-formulas is hereditarily principal for a non-logical rule $(R)$. We can deduce from that
    that the l.h.s. cut-formula is principal for $(S_1)$ and the r.h.s. cut-formula is principal for $(S_2)$. Call $\pi_1$ (resp. $\pi_2$) the subderivation
    of last rule $(S_1)$ (resp. $(S_2)$).
     
    Then we consider the following sub-cases, in order:
     \begin{itemize}
         \item \textbf{weakening sub-case}: this is the case  when one of the premises of $c$ is a $wk$ rule. W.l.o.g. assume that it is the left premise of $c$ which is conclusion of $\rigrul{\wk}$, with principal formula $A$. We eliminate the cut by keeping only the l.h.s. proof $\pi_1$, removing the last cut $c$ and last    $\rigrul{\wk}$ rule    on $A$, and by adding enough
        $\rigrul{\wk}$, $\lefrul{\wk}$ rules to introduce all the new formulas in the final sequent.  The degree has decreased.

      \item \textbf{exponential sub-case}: this is when one of the premises of $c$ is conclusion of a $cntr$, $\rigrul{?}$ or $\lefrul{!}$ rule on a formula $?A$ or $!A$, and the other one is not a conclusion of $\wk$.
      
       Assume w.l.o.g. that it is the right premise which is conclusion of $\lefrul{\cntr}$ or $\lefrul{!}$ on $!A$, and thus the only possibility for the left premise is to  be conclusion of $\rigrul{!}$.  This is rule $(S_1)$ on the picture, last rule of the subderivation $\pi_1$, and we denote its conclusion as $!\Gamma' \seqar ?\Delta', !A$. We will use here a global rewriting step. For that consider in $\pi_2$ all the top-most direct ancestors of the cut-formula $!A$, that is to say direct ancestors which do not have any more direct ancestors above. Let us denote them as $!A^{j}$ for $1\leq j \leq k$. Observe that each $!A^{j}$ is principal formula of a rule $\lefrul{!}$ or $\lefrul{wk}$. Denote by $\rho$ the subderivation
       of $\pi_2$ which has as leaves the sequents premises of these  $\lefrul{!}$ or $\lefrul{wk}$ rules with conclusion containing $!A^{j}$.
       Let $\rho'$ be a derivation obtained from $\rho$ by renaming if necessary eigenvariables occurring in premises of rules $\lefrul{\exists}$, $\rigrul{\forall}$, $(R)$  so that none of them belongs to $FV(!\Gamma', ?\Delta')$, where we recall that $!\Gamma' \seqar ?\Delta',!A$ is the l.h.s. premise of the cut $c$.
  Now, let $\pi'_1$ be the immediate subderivation of $\pi_1$, of conclusion       $!\Gamma' \seqar ?\Delta',A$.  We then define the derivation 
  $\rho''$ obtained from   $\rho'$ in the following way:
  \begin{itemize}
  \item add a cut $c_j$ with (a copy) of $\pi'_1$ on $A^j$ at each leaf which is premise of a rule  $\lefrul{!}$;
  \item add to each sequent coming from $\rho'$  an additional context $!\Gamma'$ on the l.h.s. and an additional context $?\Delta'$ on the r.h.s., and additional $wk$ rules to introduce these formulas below the $\lefrul{wk}$ rules on formulas $!A^{j}$;
  \item introduce suitable $\lefrul{cntr}$ and $\rigrul{cntr}$ rules after multiplicative binary rules $\rigrul{\land}$, $\lefrul{\lor}$  in such a way to replace $!\Gamma', !\Gamma'$ (resp. $?\Delta', ?\Delta'$) by  $!\Gamma'$ (resp. $?\Delta'$). 
  \end{itemize}
  
  It can be checked that  $\rho''$ is a valid derivation, because all the conditions for context-sensitive rules $(\rigrul{\forall})$, $(\lefrul{\exists})$, $(\rigrul{!})$, $(\lefrul{?})$, $(R)$ are satisfied. In particular the rules $(\rigrul{!})$, $(\lefrul{?})$, $(R)$ are satisfied because the contexts have been enlarged with $!$ formulas on the l.h.s. of the sequents ($!\Gamma'$) and ?  formulas on the r.h.s. of the sequents ($?\Gamma'$).  
  
  Now, let $\pi'$ be the derivation obtained from $\pi$ by removing the cut $c$ and replacing the subderivation $\rho$ by $\rho''$. The derivation $\pi'$ is a valid one, it has the same conclusion $!\Gamma', \Sigma \seqar ?\Delta', \Pi$ and with respect to $\pi$ we have replaced one non-anchored cut $c$ with at most $k$ ones $c_j$, but which are of strictly lower degree. So $\deg(\pi')<\deg(\pi)$ and we are done.

      
      \item \textbf{logical sub-case}: we are now left with the case where both premises of $c$ are conclusions of rules others than $?$, $!$, $wk$, $cntr$. We can thus apply Lemma \ref{lem:logical steps}.
         If one of the premises is an axiom $\lefrul{\bot}$, $\id$ or $\rigrul{\bot}$, then $\pi$ can be rewritten to a suitable proof $\pi'$ by removing $c$ and the axiom rule. Otherwise both premises introduce the same connective, either  $\land$, $\lor$, $\laor$, $\laand$, $\forall$ or $\exists$. In each case a specific rewriting rule replaces the cut $c$ with one cut of strictly lower degree. 
      %See the Appendix.
           \end{itemize}
     \end{itemize}
     \end{proof}
