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}

\todo{Add proof sketch. Cut and paste main proof to appendix.}