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

%Todo: $+1$,  

We say that a function $f$ is represented by a formula $A_f$ if the arithmetic can prove (in the forthcoming proof system) a formula of the form $\forall ^{\normal} \vec u, \forall ^{\safe} x, \exists^{\safe}! y. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the result of $f(\vec u; \vec x)$.

Let us give a few examples of formulas representing basic functions.

\begin{itemize}

\item Successor $\succ{}$: $\forall^{\safe} x, \exists^{\safe} y. y=x+1.$ 

\item Conditional $C$: 

$$\begin{array}{ll}

\forall^{\safe} x, y_{\epsilon}, y_0, y_1, \exists^{\safe} y. & ((x=\epsilon)\cand (y=y_{\epsilon})\\

                                                                                                   & \cor( \exists^{\safe}z.(x=\succ{0}z) \cand (y=y_0))\\

                                                                                                   & \cor( \exists^{\safe}z.(x=\succ{1}z) \cand (y=y_1)))\

\end{array}

$$

\end{itemize}

\patrick{to be continued}