\section{Free-cut elimination in linear logic}
\label{sect:free-cut-elim}
% 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}. 
  We first define which cut instances may remain in proofs after free-cut elimination.
%  They are called \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:
%  See for instance (the principal formulas are underlined):
%  \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 propose a more general definition:
Since our nonlogical rules may have many principal formulae on which cuts may be anchored, we need a slightly more general notion of principality.
    \begin{definition}\label{def:anchoredcut}
  We define the notions of \textit{hereditarily principal formula} and \textit{anchored cut} in a $\system$-proof, for a system $\system$, by mutual induction as follows:
  \begin{itemize}
  \item A formula $A$ in a sequent $\Gamma \seqar \Delta$ is \textit{hereditarily principal} for a rule instance (S) if either (i) the sequent is in the conclusion of (S) and $A$ is principal in it, or 
(ii)  the sequent is in the conclusion of an anchored cut, the direct ancestor of $A$ in the corresponding premise is hereditarily principal for the rule instance (S), and the rule (S) is nonlogical.
  \item A cut-step is an \textit{anchored cut} if the two occurrences of its cut-formula $A$ in each premise are hereditarily principal for nonlogical steps, or one is hereditarily principal for a nonlogical step and the other one is principal for a logical step.
  \end{itemize}
     A cut which is not anchored will also be called a \textit{free-cut}.
  \end{definition}
  As a consequence of this definition, an anchored cut on a formula $A$ has the following properties:
  \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 nonlogical step (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 is a logical step 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.
%   

  
%  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:
Due to condition 4 in Sect.~\ref{sect:preliminaries}, we have the following:
   \begin{lemma}\label{lem:hereditaryprincipalnonlogical}
   A formula occurrence $A$ on the LHS (resp.\ RHS) of a sequent and hereditarily principal for a nonlogical rule (R) 
   cannot be of the form $A=?A'$ (resp. $A=!A'$).
   \end{lemma}
  
   
   Now we can state the main result of this section:
   \begin{theorem}
   [Free-cut elimination]
   \label{thm:free-cut-elim}
    Given a system  $\system$, any  $\system$-proof $\pi$ can be transformed into a $\system$-proof $\pi'$ with same end sequent and without any free-cut.
   \end{theorem}
    %The proof will be given below. It will proceed
     The proof proceeds in a way similar to the classical proof of cut elimination for linear logic,
%, but here for eliminating only free-cuts, and one has 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, which comes from standard linear logic:
%%    \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} is  the handling of the commutation steps, since this is where the new non-logical rules could raise some problems.
but eliminating only free-cuts and verifying compatibility with our notion of nonlogical rule, in particular for the commutation cases.
     
     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 pure linear logic:\footnote{Note that, for the $(\rigrul{\forall})$, $(\lefrul{\exists})$ rules, there might also be a global renaming of eigenvariables if necessary.}
     \begin{lemma}[Standard commutations]\label{lem:standardcommutations}
     Any logical rule  distinct from $(\rigrul{!})$, $(\lefrul{?})$ can be commuted under a cut. If the logical rule is binary this may produce two cuts, each in a separate branch.
     \end{lemma}
    
    
%     In the following we will need to be more careful about rules $(\rigrul{!})$, $(\lefrul{?})$, $(R)$. For that we establish our second key lemma:
        For rules $(\rigrul{!})$, $(\lefrul{?})$, $(R)$ we establish our second key lemma:
  \begin{lemma}[Key commutations]\label{lem:keycommutations}
     A cut of the following form, where $?A$ is not principal for $(R)$, can be commuted above the $(R)$ step:
 \[
     \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'}{} 
?A, !\Gamma' \seqar  ?\Pi'
                    	} 
\]
    Similarly if $(R)$ is replaced with $(\rigrul{!})$, with $?A$ in its RHS context, and also for the symmetric situations:
    cut on the LHS of the conclusion of an $(R)$ or a $(\lefrul{?})$ step on a (non-principal) formula $!A$, with a sequent $!\Gamma' \seqar  ?\Pi', !A$.
  \end{lemma}  
     \begin{proof}
     The derivation is transformed as follows:
      \[
     \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}{}
 !\Gamma, \Sigma_i  \seqar \Delta_i, ?A, ?\Pi
                                 		 } {
%                                 		  \vlinf{}{}{?A, !\Gamma' \seqar  ?\Pi'}{} 
?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 nonlogical 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 LHS of the conclusion of an $(R)$ on a formula $!A$.
     The analogous situations with rules  $(\rigrul{!})$ and $(\lefrul{?})$ are handled in the same way, as usual in linear logic.
     \end{proof}
     %Now we have all the necessary lemmas to proceed with the proof of the theorem.

    Now we can prove the main free-cut elimination result:
    \begin{proof}[Proof sketch of Thm.~\ref{thm:free-cut-elim}]
    Given a cut step $c$ in a proof $\pi$, we call  \emph{degree} $\deg( c)$  the number of connectives and quantifiers of its  cut-formula. Now the \emph{degree} of $\pi$, $\deg( \pi)$, is the multiset of the degrees of its non-anchored cuts. We consider the usual Dershowitz-Manna ordering on multisets of natural numbers \cite{Dershowitz:1979:PTM:359138.359142}.\footnote{Let $M,N: \Nat \to \Nat$ be two multisets of natural numbers. Then $M<N$ if $M\neq N$ and, whenever $M(x) > N(x)$ there is some $y >x$ such that $N(y) > M(y)$. When $M$ and $N$ are finite, i.e.\ have finite support, $<$ is well-founded.}
       The proof proceeds by induction on $\deg( \pi)$.  For a given degree we proceed with a sub-induction on the \textit{height} $\height{\pi}$ of the proof.
    
    Consider a proof $\pi$ of non-null degree. We want to show how to reduce it to a proof of strictly lower degree. Consider a top-most non-anchored cut $c$ in $\pi$, i.e.\ 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 proceed as follows: if $A$ is not hereditarily principal in one of its premises  we try to commute $c$ with the rule along its left premise  $(S_1)$, and if not possible then commute it with the rule along its right premise $(S_2)$, by Lemmas \ref{lem:hereditaryprincipalnonlogical}, \ref{lem:standardcommutations} and \ref{lem:keycommutations}. If $A$ is hereditarily principal in both premises we proceed with a cut-elimination step, as in standard linear logic. For this second step, the delicate part is the elimination of exponential cuts, for which we use a big-step reduction. This works because the contexts in the nonlogical rules $(R)$ are marked with $!$ (resp. $?$) on the LHS (resp. RHS). 
%    See the appendix for the full proof.
    \end{proof}
    
%   \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} }
%}
%}
%\]
%}
%
%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}
