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

\begin{definition}\label{def:LLsequentcalculus}

\vlinf{\rigrul{\laor}}{}{\Gamma \seqar \Delta, A_1\laor A_2}{\Gamma \seqar \Delta, A_i}

\vlinf{\rigrul{!}}{}{!\Gamma \seqar ?\Delta, !A}{!\Gamma \seqar ?\Delta, A}

  We will consider extensions of linear logic with a \textit{theory}  $\mathcal T$ consisting in a finite set of additional axioms and rules, depicted as:

 \[

 \begin{array}{cc}

  \vlinf{(ax)}{}{ \seqar A}{}  &  \vlinf{(R)}{}{ !\Gamma , \Sigma' \seqar \Delta' , ? \Pi  }{ \{!\Gamma , \Sigma_i \seqar \Delta_i , ? \Pi \}_{i \in I} }

\end{array}

\]

 where in rule (R), $I$ is a finite set (indicating the number of premises) and we assume the following condition:

  \textit{for any $i\in I$, formulas in $\Sigma_i, \Delta_i$ do not share any free variable with   $\Gamma, \Pi$.} 

  In the following we will be interested in an example of theory  $\mathcal T$ which is a form of arithmetic.

  A proof in this system will be called a \textit{ $\mathcal T$-proof}, or just \textit{proof} when there is no risk of confusion.

   The rules of Def. \ref{def:LLsequentcalculus} are called \textit{logical rules} while the rules (ax) and (R) of $\tau$ are called \textit{non-logical}.

  As usual rules come with a notion of \textit{active formulas}, which are a subset of the rules in the conclusion, e.g.:

  $A \lor B$ in rule $\lefrul{\lor}$ (and similarly for all rules for connectives); $?A$ in rule $\rigrul{\cntr}$; all conclusion formulas in axiom rules;

   $\Sigma', \Delta'$ in rule (R).

  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 $\tau$. For this reason we need now to define the kind of cuts that  will remain in proofs after reduction.

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

  So for instance a cut on an (active) 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.

   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}

%$$

%	\vliiinf{}{}{ \seqar A}{ \seqar C}

%	$$

%\[

%	\vliiinf{R}{}{ !\Gamma , \Sigma' \seqar \Delta' , ? \Pi  }{ \{!\Gamma , \Sigma_i \seqar \Delta_i , ? \Pi \}_{i \in I} }

%	\]