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

\section{Completeness}\label{sect:completeness}

The main result of this section is the following:

\begin{theorem}

	\label{thm:completeness}

	For every $\mubci{i-1}$ program $f(\vec u ; \vec x)$ (which is in $\fphi i$), there is a $\Sigma^{\safe}_i$ formula $A_f(\vec u, \vec x)$ such that $\arith^i$ proves $\forall^{\normal} \vec u, \forall^{\safe} \vec x, \exists^{\safe} ! y. A_f(\vec u , \vec x , y )$ and $\Nat \models \forall \vec u , \vec x. A_f(\vec u , \vec x , f(\vec u ; \vec x))$.

\end{theorem}

\begin{proof}[Sketch](A more detailed proof can be found in Appendix \ref{appendix:completeness})

 The proof proceeds by induction on the construction of $\mubci{i-1}$ program $f(\vec u ; \vec x)$ to construct a suitable formula $A_f(\vec u, \vec x)$ .  The case of initial functions is easy, by using the formulas we gave in Sect. \ref{sect:graphsbasicfunctions}. The case of safe composition is also simple, and makes use of the $\rais$ rule. The two key cases are thus those of predicative recursion and predicative minimisation. 

 For predicative recursion, the basic idea is to follow the classical simulation of primitive recursion in arithmetic, adapted to recursion on notation, by encoding the sequence of recursive calls as an integer $w$. The main technical difficulty is to have a decoding predicate $\beta (k, w, y)$ (the $k$th element of the sequence represented by $w$ is $y$) which is sorted in a suitable way so that the formula $A_f$  is in the same class $\Sigma^{\safe}_i$ as $A_g$,  $A_{h_0}$ and $A_{h_1}$.  This can be obtained by defining  the predicate $\beta (k, w, y)$ with $k$ in $\normal$ and $w$, $y$ in $\safe$.

 For predicative minimisation finally, assume $f$ is defined by  $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$. By induction hypothesis we have a $\Sigma^{\safe}_{i-1}$ formula $A_g (\vec u , \vec x , x , y)$  satisfying the property. We then define $A_f(\vec u ; \vec x , z)$ as the following $\Sigma^{\safe}_{i}$ formula:

\[

\begin{array}{rl}

&\left(

z=0 \  \cand \ \forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)

\right) \\

\cor & \left(

\begin{array}{ll}

z\neq 0 

& \cand\   \forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) \\

& \cand\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) 

\end{array}

\right)

\end{array}

\]

As in the bounded arithmetic $S_2$ (\cite{Buss86book}, Thm 20, p. 58),  $\arith^i$ can prove a minimisation principle for $\cmin{\Sigma^\safe_{i-1}}$ formulas, which we apply to the formula  $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$. From that we can prove the totality of $A_f(\vec u ; \vec x , z)$ as required.

\end{proof}