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

\section{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_i$ formula $A_f(\vec u, \vec x)$ such that $\arith^i$ proves $\forall \vec u \in \normal . \forall \vec x \in \safe. \exists ! y \in \safe . A_f(\vec u , \vec x , y )$ and $\Nat \models \forall \vec u , \vec x. A(\vec u , \vec x , f(\vec u ; \vec x))$.

\end{theorem}

The rest of this section is devoted to a proof of this theorem.

We proceed by structural induction on a $\mubc{i-1} $ program, dealing with each case in the proceeding paragraphs.

\paragraph*{Predicative minimisation}

Suppose $f(\vec u ; \vec x)$ is defined as $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$.

By definition $g$ is in $\mubci{i-2}$, and so by the inductive hypothesis there is a $\Sigma_{i-1}$ formula $A_g (\vec u , \vec x , x , y)$ computing the graph of $g$ such that,

\[

\arith^i \proves \forall \vec u^\normal . \forall \vec x^\safe , x^\safe . \exists ! y^\safe . A_g(\vec u , \vec x , x , y)

\]

Let us define $A_f(\vec u ; \vec x , z)$ as:

\[

\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}

\]

Notice that $A_f$ is $\Pi_{i-1}$, since $A_g$ is $\Sigma_{i-1}$ and occurs only in negative context above, with additional safe universal quantifiers occurring in positive context.

In particular this means $A_f$ is $\Sigma_i$.

Now, to prove totality of $A_f$, we rely on $\Sigma^\safe_{i-1}$-minimisation, which is a consequence of $\cpind{\Sigma^\safe_i}$:

\begin{lemma}

[Minimisation]

$\arith^i \proves \cmin{\Sigma^\safe_{i-1}}$.

\end{lemma}

\begin{proof}

\todo{}

\end{proof}

Now, working in $\arith^i$, let $\vec u \in \normal , \vec x \in \safe$ and let us prove:

\[

\exists !z^\safe  . A_f(\vec u ; \vec x , z)

\]

Suppose that $\exists x^\safe , y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$.

We can apply minimisation due to the lemma above to find the least $x\in \safe$ such that $\exists y^\safe .  (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$, and we set $z = \succ 1 x$. So $x= p z$.

%\todo{verify $z\neq 0$ disjunct.}

Then $z \neq 0$ holds. Moreover we had  $\exists ! y^\safe . A_g(\vec u , \vec x , x , y)$. So we deduce that

 $\forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) $. Finally, as $p z$ is the least element such that

  $\exists y^\safe .  (A_g (\vec u ,\vec x , p z , y) \cand y=_2 0)$, we deduce

 $\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) $. We conclude that the second member of the disjunction

 $A_f(\vec u ; \vec x , z)$ is proven.

 Otherwise, we have that $\forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)$, so we can set $z=0$ and the first member of the disjunction $A_f(\vec u ; \vec x , z)$ is proven.

So we have proven $\exists z^\safe  . A_f(\vec u ; \vec x , z)$, and unicity can be easily verified.

\paragraph*{Predicative recursion on notation}

\anupam{Assume access to the following predicates (makes completeness easier, soundness will be okay):

	\begin{itemize}

	%	\item $\pair x y z $ . ``$z$ is the sequence that appends $y$ to the sequence $x$''

		\item $\pair x y z$. ``$z$ is the sequence that prepends $x$ to the sequence $y$''

		\item $\beta (i; x ,y)$. ``The $i$th element of the sequence $x$ is $y$.''

	\end{itemize}

	}

Now suppose that $f$ is defined by PRN:

\[

\begin{array}{rcl}

f(0 , \vec u ; \vec x) & \dfn & g(\vec u ; \vec x) \\

f(\succ i u, \vec u ; \vec x) & \dfn & h_i( u , \vec u ; \vec x , f(u , \vec u ; \vec x))

\end{array}

\]

\anupam{using $\beta(i,x,y)$ predicate for sequences: ``$i$th element of $x$ is $y$''. Provably total in $\arith^1$.}

Suppose we have $\Sigma^\safe_i$ formulae $A_g (\vec u ; \vec x,y)$ and $A_{h_i} (u , \vec u ; \vec x , y , z)$ computing the graphs of $g$ and $h_i$ respectively, provably total in $\arith^i$.

We define $A_f (u ,\vec u ; \vec x , y)$ as,

\[

\exists w^\safe . \left(

\begin{array}{ll}

&

%Seq(z) \cand

\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\

\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_i) \cand \beta (k+1 ,w, y_{k+1})  \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )

\end{array}

\right)

\]

which is $\Sigma^\safe_i$ by inspection, and indeed defines the graph of $f$.

To show totality, let $\vec u \in \normal, \vec x \in \safe$ and proceed by induction on $u \in \normal$.

The base case, when $u=0$, is immediate from the totality of $A_g$, so for the inductive case we need to show:

\[

\exists y^\safe . A_f (u , \vec u ; \vec x , y)

\quad \seqar \quad

\exists z^\safe . A_f (s_i u, \vec u ; \vec x , y)

\]

\anupam{here need to `add' element to the computation sequence. Need to do this earlier in the paper.}

\anupam{for inductive cases, need $u\neq 0$ for $\succ 0$ case.}

\paragraph*{Safe composition}

Now suppose that $f$ is defined by safe composition:

\[

f(\vec u ; \vec x) \quad \dfn \quad g( \vec h(\vec u;) ; \vec h' (\vec u ; \vec x) )

\]

By the inductive hypothesis, let us suppose that we have $\Sigma^\safe_i $ definitions $A_g , A_{h_i} , A_{h_j'} $ of the graphs of $g , h_i , h_j'$ respectively, which are provably total etc.

In particular, by Raising, we have that $\forall \vec u^\normal . \exists v^\normal . A_{h_i} (\vec u , v)$.

We define $A_f (\vec u , \vec x , z)$ defining the graph of $f$ as follows:

\[

\exists \vec v^\normal . \exists \vec y^\safe .

\left(

\bigwedge\limits_i A_{h_i} (\vec u , v_i)

\wedge

\bigwedge\limits_j A_{h_j'} (\vec u ; \vec x , y_j)

\wedge

A_g ( \vec v , \vec y , z )

\right)

\]

The provable totality of $A_f$ follows from simple first-order reasoning, mostly cuts and basic quantifier manipulations.

\todo{elaborate}

\paragraph*{Other cases}

\todo{}