Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\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}