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}

\begin{proof}

	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 by predicative minimisation from $g$ (we then denote $f$ as 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}

	\begin{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}$ (see \cite{Buss86book}, Thm 20, p. 58).

		Let $A(x)$ be a  $\Sigma^\safe_{i-1}$ formula, with $x$ in $\safe$. We define the formula $B(a,b,c)$ as:

		$$ \forall x^{\safe}. (x < |a| \moins b \cimp \zerobit(x,c)) \cand \forall y^{\safe}<c. \neg A(y) \cand \exists y^{\safe} < 2^{|a|\moins b}.A(c+y)$$

		where $a$ is in $\normal$, $b$ in $\normal$ and $c$ in $\safe$.  $B(a,b,c)$ is in $\Sigma^\safe_{i}$.

		The intuitive idea of the proof is to observe that, if $A(a)$ is true for $a\neq 0$, then  $\exists x^{\safe}\leq a. B(a,b,x)$ holds for $b=0$, and to try to prove it for $b=|a|$, by using a length induction on $b$.

		First, one can prove:

		$$ (A(a) \cand a \neq 0) \cimp B(a,0,0).$$ 

		And thus:

		$$ (A(a) \cand a \neq 0) \cimp \exists x^{\safe}\leq a .B(a,0,x).$$ 

		We then can check that the two following statements are provable:

		$$

		\begin{array}{rcl}

		(b<|a| \cand B(a,b,c)\cand \exists y^{\safe}<2^{|a| \moins (b+1)}.A(c+y)) &\cimp& B(a,\succ{} b,c)\\

		(b<|a| \cand B(a,b,c)\cand \forall y^{\safe}<2^{|a| \moins(b+1)}.  A(c+y)) &\cimp & B(a,\succ{} b, c+2^{|a| \moins (b+1)})

		\end{array}

		$$

		Moreover we have: $A(a) \cand B(a,b,c) \cimp c\leq a$.

		From these three statements we deduce:

		$$(A(a) \cand a \neq 0 \cand b<|a| \cand \exists x^{\safe} \leq a. B(a,b,x)) \cimp \exists x^{\safe } \leq a.B(a,\succ{} b,x).$$

		Note that here we have used the fact that we are in classical logic.

		The formula $\exists x\leq a. B(a,b,c)$ is in $\Sigma^{\safe}_{i}$, so by $\Sigma^{\safe}_{i}$-LIND on the formula $\exists x\leq a. B(a,b,c)$, with the variable $b$ which is in $\normal$,  we obtain:

		$$(A(a) \cand a \neq 0 ) \cimp \exists x^{\safe } \leq a.B(a,|a|,x).$$

		But $B(a,|a|,x)$ implies $(\forall y^{\safe}<x. \neg A(y))\cand A(x)$, so we have proven:

		$$(A(a) \cand a \neq 0 ) \cimp (\exists x^{\safe } \leq a. (\forall y^{\safe}<x. \neg A(y))\cand A(x))$$

		which is the $\Sigma_{i-1}^{\safe}$ axiom for $A$.

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

	}

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

\end{proof}