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

Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$. We use classical logic connectives $\neg$, $\cand$, $\cor$, $\forall$, $\exists$. The formula $A \cimp B$ will be a notation for $\neg A \cor B$.

\forall u^\normal , v^\normal . \safe (u \smsh v)\\

\patrick{\forall u^\normal \safe(u) \; ?}

Notation: if $\vec t=t_0,\dots, t_k$, we will denote as $\safe(\vec t)$ the sequence of formulas $\safe(t_0),\dots, \safe(t_k)$. Similarly for $\normal(\vec t)$.

\patrick{For $\forall \vec x^\normal . \exists  y^\safe .  A$ closed ?} 

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

&

%\vliinf{\lefrul{\cimp}}{}{\Gamma, A \cimp B \seqar \Delta}{\Gamma \seqar A, \Delta}{\Gamma, B \seqar \Delta}

%&

%

%\vlinf{\rigrul{\cimp}}{}{\Gamma \seqar \Delta, A \cimp B}{\Gamma, A \seqar \Delta,  B}

    \vlinf{\rais}{}{  \normal(t_1), \dots, \normal(t_k) \seqar  \exists  y^\normal .  A }{  \normal(t_1), \dots, \normal(t_k) \seqar \exists  y^\safe .  A}

%\patrick{In fact, I think we rather need the following nonlogical rule, which implies the previous one but is I guess more general:

%\[

% \begin{array}{cc}

%    \vlinf{\rais}{}{  \normal(t_1), \dots, \normal(t_k) \seqar  \normal(t) }{  \normal(t_1), \dots, \normal(t_k) \seqar \safe(t)}

%\end{array}

%\]

%}

The $\basic$ axioms are equivalent to the following nonlogical rules, that we will also designate by $\basic$:

\[

\small

\begin{array}{l}

\begin{array}{cccc}

\vlinf{}{}{\seqar \safe (0)}{}&

\vlinf{}{}{\safe(t) \seqar \safe(\succ{} t)}{}&

\vlinf{}{}{ \safe (t)   \seqar 0 \neq \succ{} t}{} &

\vlinf{}{}{\safe (s) , \safe (t)  , \succ{} s = \succ{} t\seqar s = t }{}\\

\end{array}

\\

\vlinf{}{}{\safe (t) \seqar t = 0 \cor \exists y^\safe . t = \succ{} y  }{}

\qquad

\vlinf{}{}{\safe(s), \safe(t) \seqar \safe(s+t) }{}\\

\vlinf{}{}{\normal (s), \safe(t) \seqar \safe(s \times t)  }{}

\qquad

\vlinf{}{}{\normal (s), \normal(t) \seqar \safe(s \smsh t)  }{}\\

\patrick{\vlinf{}{}{\normal(t) \seqar \safe(t)  }{}}

\end{array}

\]

 The sequent calculus for $\arith^i$ is that of Fig. \ref{fig:sequentcalculus} extended with the $\basic$,  $\cpind{\Sigma^\safe_i } $ and $\rais$ nonlogical rules.

 \begin{lemma}

 For any term $t$, its free variables can be split in two sets $\vec{x}$ and $\vec{y}$ such  that the sequent $\normal(\vec x), \safe(\vec y) \seqar \safe(t)$ is provable. 

 \end{lemma}

   [Free-cut elimination]\label{thm:freecutelimination}

   Now we want to deduce from that theorem a normal form property for proofs of certain formulas. But before that let us define some particular classes of sequents and proofs.

   Say that a sequent $\Gamma \seqar \Delta$ is \textit{well-typed} if for any free variable $x$ occurring in $\Gamma$ or $\Delta$, there exists a formula $\safe(x)$ or $\normal(x)$ in $\Gamma$. A proof is well-typed if its sequence are.

   \begin{lemma}\label{lem:welltyped}

   If a well-typed sequent $\Gamma \seqar \Delta$ is provable, then it admits a well-typed proof.

   \end{lemma}

   \begin{proof}

   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 same conclusion and such that, for any sequent, if it is well-typed then its premises are well-typed.

   \patrick{to be finished}

     \end{proof}

     \patrick{ TODO: define integer-positive sequents and proofs.}

 \begin{theorem}

   Assume the $\arith^i$ sequent calculus proves a closed formula $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$. Then there exists a proof $\pi$ of the sequent 

   $\normal(\vec u), \safe(\vec x) \seqar \exists y^\safe . A(\vec u ; \vec x , y)$ satisfying:

   \begin{enumerate}

    \item $\pi$  only contains  $\Sigma^\safe_{i}$ formulas,

    \item $\pi$ is a well-typed and integer-positive proof. 

   \end{enumerate}

   \end{theorem}