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

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

We now turn to proving the converse result to the last section, that our theories $\arith^i$ are strong enough to represent any $\fphi i $ function.

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}[Proof sketch]

 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 and simply combines previously defined graphs by \emph{modus ponens} (or, equivalently, $\cut$) and logical steps. 

 Naturally, the interesting cases are 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 the representation of (de)coding functions $\beta (k, x)$ (``the $k$th element of the sequence $x$'') and $\langle x,y \rangle$ (``the pair $(x,y)$'').

 For this we represent instead the length-bounded variants of these functions given towards the end of Sect.~\ref{sect:prelims}, relying on the bounded minimisation and polychecking results, Lemmas~\ref{lem:bounded-minimisation} and \ref{lem:polychecking}, to find appropriate length bounds.

%  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, assume $f$ is defined as  $\succ 1 \mu x .( g(\vec u ; \vec x , x) =_2 0)$ (or $0$ if no such $x$ exists).

  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 for the analogous bounded arithmetic theory $S^i_2$ (\cite{Buss86book}, Thm 20, p. 58),  $\arith^i$ can prove a \emph{minimisation} principle for $\Sigma^\safe_{i-1}$ formulas, allowing us to extract the \emph{least} witness of a safe existential, which we apply to $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$. From here we are able to readily prove the totality of $A_f(\vec u ; \vec x , z)$, notably relying crucially on classical reasoning.

\end{proof}