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

   If a well-typed sequent $\Gamma \seqar \Delta$ is provable, then there exists $\vec u$  such that

 the sequent $\normal(\vec u), \Gamma \seqar \Delta$ admits a well-typed proof.

   \patrick{It seems to me the statement had to be modified so as to prove the lemma. Maybe I misunderstand something.}

   \begin{proof}[Proof sketch]

   First by Thm \ref{thm:freecutelimination} we know that $\Gamma \seqar \Delta$ admits a proof $\pi$ without any free-cut. Let us then prove that $\pi$ can be transformed in a proof $\pi'$ of conclusion of the form  $\normal(\vec u), \Gamma \seqar \Delta$ and such that, for any sequent, if it is well-typed then its premises are well-typed.

   Observe first that by definition of $\arith^i$ and the absence of free cut, all quantifiers occurring in a formula of the proof are of one of the forms

   $\forall^{\safe}$,   $\exists^{\safe}$,  $\forall^{\normal}$,   $\exists^{\normal}$, and for the last two ones they are sharply bounded.

  Then, one can check that for all rules but the quantifier rules and the cut rule, if the conclusion is well-typed, then so are the two premises.  For the remaining rules, $\forall-r$ and $\exists-l$ are unproblematic, because of the observation above. Let us now examine the case of $\exists-r$, with a $\safe$ label, and the other rules can be treated in the same way. In the premise we get a formula $\safe(t) \cand A(t)$. Then what we do is that, if  $\vec u$ denote the free variables of $t$, we add to the context of all sequents of the proof $\normal(\vec u)$. We obtain in this way a valid proof new proof,  and the premises of the rule have become well-typed.

       \end{proof}