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

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

\section{Proof of completeness}

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.

The property is easily verified for the class of initial functions of  $\mubci{i-1}$: constant, projections, (binary) successors, predecessor, conditional, as already shown in Sect. \ref{sect:graphsbasicfunctions}. Now let us examine the three constructions: predicative minimisation, predicative (safe) recursion and composition. 

\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^{\safe}_{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^{\safe}_{i-1}$, since $A_g$ is $\Sigma^{\safe}_{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^{\safe}_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}

	% see Thm 20 p. 58 in Buss' book.

	%\begin{proof}

	%\end{proof}

	This Lemma is proved by using the same method as for the proof of the analogous result in the bounded arithmetic $S_2^{i+1}$ (see \cite{Buss86book}, Thm 20, p. 58).

	\patrick{Examining it superficially, I think indeed the proof of Buss can be adapted to our setting. But we should probably look again at that with more scrutiny.}

	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}

			}

			\patrick{I also assume access to the following predicates:

				\begin{itemize}

					%   \item $\zerobit (u,k)$ (resp. $\onebit(u,k)$). " The $k$th bit of $u$ is 0 (resp. 1)"

					%   \item $\pref(k,x,y)$. "The prefix of $x$ (as a binary string) of length $k$ is $y$" 

					\item $\addtosequence(w,y,w')$. "$w'$ represents the sequence obtained by adding $y$ at the end of the sequence represented by $w$". Here we are referring to sequences which can be decoded with predicate $\beta$.

					\end{itemize}}

					In the following we will use the predicates $\zerobit (u,k)$, $\onebit(u,k)$, $\pref(k,x,y)$ which have been defined in Sect. \ref{sect:graphsbasicfunctions}.

					Suppose that $f$ is defined by predicative recursion on notation:

					\[

					\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^{\safe} 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_k) \cand \beta (k+1 ,w, y_{k+1})  \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )\\

					\cand & \forall^{\normal}  k < |u| . \exists^{\safe} y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1})  \cand B (u , \vec u ; \vec x , y_k , y_{k+1}) )

					\end{array}

					\right)

					\]

					where 

					\[

					B (u , \vec u ; \vec x , y_k , y_{k+1}) = \left(

					\begin{array}{ll}

					& \zerobit(u,k+1) \cimp  \exists v .(\pref(k,u,v)  \cand A_{h_0}(v,\vec u ; \vec x, y_k, y_{k+1}) )\\

					\cand &  \onebit(u,k+1) \cimp  \exists v .(\pref(k,u,v)  \cand A_{h_1}(v,\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 , z)

					\]

					So let us assume $\exists y^\safe . A_f (u , \vec u ; \vec x , y) $. Then there exists $w$ such that $\safe(w)$ and 

					$A_f (u , \vec u ; \vec x , w) $.

					We know that there exists a $z$ such that $A_{h_i}(u,\vec u ; \vec x, y, z)$. Let then $w'$ be such that

					$\addtosequence(w,z,w')$. Observe also that we have $\pref(|u|,s_i u,u)$

					So we have, for $k=|u|$:

					$$  \beta (k, w', y) \cand \beta (k+1 ,w', z)  \cand B (u , \vec u ; \vec x , y , z).$$

					and we can conclude that

					\[

					\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|+1, w',z ) \\

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

					\end{array}

					\right)

					\]

					So $\exists z^{\safe} . A_f (s_i u, \vec u ; \vec x , z)$ has been proven. So by induction we have proven $\forall^{\normal} u,  

					\forall^{\normal} \vec u, \exists^{\safe} y. A_f (u ,\vec u ; \vec x , y)$. Moreover one can also check the unicity of $y$, and so we have proved the required formula. 

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

					The proof of Thm \ref{thm:completeness} is thus completed.