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

%}

%\]

%  Here $cut_1$ is anchored in this sense, but not $cut_2$.   Therefore we propose a more general definition:

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

(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.

  \end{itemize}

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

   \begin{theorem}

   [Free-cut elimination]

   \label{thm:free-cut-elim}

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

     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}

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

 \[

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

    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}

      \[

     \vlinf{(R)}{}{ !\Gamma', !\Gamma,  \Sigma'   \seqar \Delta', ?\Pi, ?\Pi'}

                                 { \vliinf{cut}{}{\{!\Gamma', !\Gamma, \Sigma_i  \seqar \Delta_i, ?\Pi,?\Pi' \}_{i\in I}} {

?A, !\Gamma' \seqar  ?\Pi'

                                 		  } }

                                 \]

     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.

    Now we can prove the main free-cut elimination result:

    \begin{proof}[Proof sketch of Thm.~\ref{thm:free-cut-elim}]

\[    

     \vliinf{c \; \; \cut}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \vlinf{S_1}{}{\Gamma \seqar \Delta, A}{} }{\vlinf{S_2}{}{\Sigma, A \seqar \Pi}{}}

\]