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

          % sizes

          \newcommand{\height}[1]{\mathit{h}(#1)}

%[Sequent calculus for linear logic]

[Sequent calculus for affine linear logic]

\patrick{2Anupam: is there a reason for considering only axioms on atomic formulas $p$?}

\patrick{Note that here I changed the system to consider directly affine linear logic}

%\vlinf{\lefrul{\wk}}{}{\Gamma, !A \seqar \Delta}{\Gamma \seqar \Delta}  %% linear logic weakening

\vlinf{\lefrul{\wk}}{}{\Gamma, A \seqar \Delta}{\Gamma \seqar \Delta}

%\vlinf{\rigrul{\wk}}{}{\Gamma \seqar \Delta, ?A }{\Gamma \seqar \Delta}   %% linear logic weakening

\vlinf{\rigrul{\wk}}{}{\Gamma \seqar \Delta, A }{\Gamma \seqar \Delta}

\vlinf{\rigrul{\forall}}{}{\Gamma \seqar \Delta, \forall x . A(x)}{ \Gamma \seqar \Delta, A(a) } \\

\noalign{\bigskip}

 \vliinf{mix}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta}{\Sigma \seqar \Pi} &&&

 Note that this system is \textit{affine} in the sense that it includes general weakening rules $\rigrul{\wk}$ and  $\lefrul{\wk}$, while in linear logic   $\rigrul{\wk}$ (resp. $\lefrul{\wk}$) is restricted to formulas of the form $?A$ (resp. $!A$). The rule $mix$ is included so that this system admits cut elimination. In the following though by linear logic we will mean affine linear logic.

    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.

   \begin{proof}

   \patrick{The proof below is still in progress...}

    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.

    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$. We distinguish 3 cases for $c$:

    \begin{itemize}

    \item \textbf{First case}: the cut $c$ is non principal for its left premise. 

     Call (S) the last rule above the left premise of $c$. We perform a commutation step between (S) and $c$. We examine here the case where (S)=($\rigrul{\laand}$). 

     \[

\vlderivation{

\vliin{c}{}{ \Gamma,\Delta,A\vlan B }{ \vliin{\vlan}{}{\Gamma,A\vlan B,C}{ \vlhy{\Gamma,A,C} }{\vlhy{\Gamma,B,C}}}{ \vlhy{\Delta, C^\bot} }

}

\quad\to\quad

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

}

}

\]

\patrick{TODO: adapt to two-sided sequents here}

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}$. Therefor $\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 easier and described in the Appendix. 

    \item \textbf{Second case}: the cut $c$ is non principal for its right premise. 

    This is similar to the first case, by proceeding with a commutation case on the right. 

     \item \textbf{Third case}: the cut $c$ is principal for its left and right premises. Then we consider the following sub-cases, in order:

     \begin{itemize}

      \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$. Assume w.l.o.g. that it is the right premise, so a rule $\lefrul{\cntr}$ or $\lefrul{!}$ on $!A$.  We will use here a global rewriting step. For that consider in $\pi$ 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}$.

      Now examine the left premise of $c$, with principal formula $!A$.

      \patrick{to be continued...}

      \item \textbf{logical sub-case}: assume 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.

      \item \textbf{weakening sub-case}: the remaining case is when one of the premises of $c$ is a $wk$ rule and the other one is a rule distinct from $cntr$, $\rigrul{?}$ or $\lefrul{!}$. W.l.o.g. assume that the left premise of $c$ is conclusion of $\lefrul{\wk}$. If the right premise is conclusion of say rule $\rigrul{\land}$ on a formula $A_1\land A_2$, then $c$ is replaced by two cuts $c_i$ ($i=1,2$) on a formula $A_i$ obtained (on the left) by a $\lefrul{\wk}$ rule. These two cuts are of strictly lower degree than $c$, so we are done. We proceed in a similar way in the cases of rules introducing connectives $\lor$, $\laand$, $\laor$, $\forall$, $\exists$. Now,there remains the case where the right premise is a $\rigrul{\wk}$: then the cut can be eliminated by erasing the two $wk$ rules and using instead a $mix$ rule. In this case also the degree has decreased.

      \patrick{Display the rewriting step here}.

     \end{itemize}

    \end{itemize}

   \end{proof}