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

\section{Free-cut elimination in linear logic}

\todo{patrick}

\anupam{Possibly need to include the cases for affine logic too, e.g.\ if weakening is native, since it does not play nice as an axiom.}

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

%   \begin{definition}\label{def:anchoredcut}

%  An instance of cut rule in a  $\mathcal T$-proof is an \textit{anchored cut} if  its cut-formulas $A$ in the two premises are both principal for their rule, and at least one of these rules is non-logical.

%  \end{definition}

  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. See as example Fig. \ref{Fig:twosuccessiveanchorcuts}. Therefore we consider a more general definition:

%  \begin{figure}

%  \[

%  \vlderivation{

%    \vliinf{c1}{!\Gamma , \Gamma_1 \seqar A(t) , ?\Delta }{

%  \vlinf{(ind)}{(x \notin \FV(\Gamma, \Delta))}{ !\Gamma , A(\epsilon) \seqar A(t) , ?\Delta }{ !\Gamma , A(x) \seqar A(s x ), ?\Delta }}

%  {\Gamma_1\seqar A(\epsilon) }

%                   }

%  \]               

%%				\vlin{\cntr}{}{\Gamma, ?A}{

%%					\vlin{\wk}{}{\Gamma, ?A, ?A}{\vlhy{\Gamma, ?A}}

%%				}

%

%  \caption{Example}\label{Fig:twosuccessiveanchorcuts}

%  \end{figure}

  \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 the sequent is conclusion of the rule (S) and $A$ is principal in it, or 

  the sequent is conclusion of an anchored cut, and  the direct ancestor of $A$ in one of the two  premises is hereditarily principal for the rule (S).

  \item An instance of cut rule is an \textit{anchored cut} if  its cut-formulas $A$ in the two premises are both hereditarily principal for a rule, and at least one of these rules is non-logical.

  \end{itemize}

  \end{definition}

  So 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 non-anchored will also be called a \textit{free-cut}.

   Now we can state the main result of this section:

   \begin{theorem}

    Given a theory  $\mathcal T$, any  $\mathcal T$-proof $\pi$ can be transformed into a $\mathcal T$-proof $\pi'$ with same conclusion sequent and in which all cuts are anchored.

   \end{theorem}

   \begin{proof}

    The proof will proceed in a way similar to the classical proof of cut elimination for linear logic, but here for eliminating only non-anchored 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}$ axioms and rules. Actually the most important part of the proof will be the handling of the commutation steps, since this is where the new rules and axioms 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 steps are not straightforward.

    Given a cut rule $c$ in a proof $\pi$, we call  \emph{degree} $\deg( c)$  the number of logical connectives or quantifiers in 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. Let us handle as an example the case where $(S_1)=(\rigrul{\laand})$.

\[

\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}\leq \deg{\pi_i}$. Therefore $\pi'_i$ has non-anchored cuts of degree strictly lower than $\deg(c)$, and thus 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'$. We know that  $A=?A'$ is principal in the conclusion of $(S_2)$: the rule $(S_2)$ thus cannot be a rule $(R)$ because of the condition 2. on $(R)$ rules; 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 ?\Delta$ and 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 principal in the conclusion of $(R)$, here again it is of the form $A=?A'$. So as before we deduce that   $(S_2)=(\lefrul{?})$, and  so the r.h.s. premise is of the shape $?A',!\Gamma \seqar ?\Delta$. We can rename the free variables in the premise sequents of $(S_1)$ such that none of them belongs to $FV(!\Gamma \seqar ?\Delta)$. Then the commutation on the left-hand-side is possible, because we "enlarge" the contexts with formulas starting with a $!$ (on the l.h.s. of $\seqar$) or a $?$  (on the r.h.s. of $\seqar$). The new occurrence of $(R)$ does satisfy conditions 1. and 2.

 \patrick{TODO: I will picture this case} 

\end{itemize}

%\patrick{Check that all cases are ok, taking into account constraints due to: contexts of $\rigrul{!}$, contexts of $\mathcal{T}$ rules (R), condition on free variables of (R).}

    \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 on the l.h.s. it is of the form  $A=?A'$. As $?A'$ is not principal on the r.h.s., $(S_2)$ is not a rule $(R)$. So $(S_2)$ is a logical rule, and so it admits commutation with the cut $c$. 

   \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{!}$.  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 sequence premises of these  $\lefrul{!}$ or $\lefrul{wk}$ with conclusion containing $!A^{j}$.

       Let $\rho'$ be a derivation obtained from $\rho$ by renaming if necessary free variables occurring in premises of rules $\lefrul{\exists}$, $\rigrul{\forall}$, $(R)$  so that none of them belongs to $FV(!\Gamma, ?\Delta)$, where $!\Gamma \seqar ?\Delta,!A$ is the l.h.s. premise of the cut $c$.

  Now, let $\pi'_2$ be the immediate subderivation of $\pi_2$, 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'_2$ on $A^j$ at each leaf which is premise of a rule  $\lefrul{!}$;

  \item add to each sequent coming from $\rho'$  a context $!\Gamma$ on the l.h.s. and a 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}$, $mix$ 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 sub derivation $\rho$ by $\rho''$. The derivation $\pi'$ is a valid one, 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$.

      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}