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

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