| 4 |
4 |
|
| 5 |
5 |
\begin{theorem}
|
| 6 |
6 |
\label{thm:completeness}
|
| 7 |
|
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))$.
|
|
7 |
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(\vec u , \vec x , f(\vec u ; \vec x))$.
|
| 8 |
8 |
\end{theorem}
|
| 9 |
9 |
|
| 10 |
10 |
The rest of this section is devoted to a proof of this theorem.
|
| 11 |
|
We proceed by structural induction on a $\mubc{i-1} $ program, dealing with each case in the proceeding paragraphs.
|
|
11 |
We proceed by structural induction on a $\mubc^{i-1} $ program, dealing with each case in the proceeding paragraphs.
|
| 12 |
12 |
|
| 13 |
13 |
\paragraph*{Predicative minimisation}
|
| 14 |
14 |
Suppose $f(\vec u ; \vec x)$ is defined as $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$.
|
| ... | ... | |
| 75 |
75 |
\begin{itemize}
|
| 76 |
76 |
\item $\zerobit (u,k)$ (resp. $\onebit(u,k)$). " The $k$th bit of $u$ is 0 (resp. 1)"
|
| 77 |
77 |
\item $\pref(k,x,y)$. "The prefix of $x$ (as a binary string) of length $k$ is $y$"
|
|
78 |
\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$.
|
| 78 |
79 |
\end{itemize}}
|
| 79 |
80 |
Now suppose that $f$ is defined by PRN:
|
| 80 |
81 |
\[
|
| ... | ... | |
| 94 |
95 |
&
|
| 95 |
96 |
%Seq(z) \cand
|
| 96 |
97 |
\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\
|
| 97 |
|
\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}) )\\
|
|
98 |
%\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}) )\\
|
| 98 |
99 |
\cand & \forall k < |u| . \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}) )
|
| 99 |
100 |
\end{array}
|
| 100 |
101 |
\right)
|
| 101 |
102 |
\]
|
|
103 |
where
|
|
104 |
\[
|
|
105 |
B (u , \vec u ; \vec x , y_k , y_{k+1}) = \left(
|
|
106 |
\begin{array}{ll}
|
|
107 |
& \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}) )\\
|
|
108 |
\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}) )
|
|
109 |
\end{array}
|
|
110 |
\right)
|
|
111 |
\]
|
| 102 |
112 |
|
| 103 |
|
%where
|
| 104 |
|
%
|
| 105 |
|
%\[
|
| 106 |
|
%B (u , \vec u ; \vec x , y_k , y_{k+1}) =
|
| 107 |
|
%\begin{array}{ll}
|
| 108 |
|
%& \\
|
| 109 |
|
%\cand &
|
| 110 |
|
%
|
| 111 |
|
%\end{array}
|
| 112 |
|
%
|
| 113 |
|
%\]
|
| 114 |
113 |
%which is $\Sigma^\safe_i$ by inspection, and indeed defines the graph of $f$.
|
| 115 |
114 |
|
| 116 |
115 |
To show totality, let $\vec u \in \normal, \vec x \in \safe$ and proceed by induction on $u \in \normal$.
|
| ... | ... | |
| 118 |
117 |
\[
|
| 119 |
118 |
\exists y^\safe . A_f (u , \vec u ; \vec x , y)
|
| 120 |
119 |
\quad \seqar \quad
|
| 121 |
|
\exists z^\safe . A_f (s_i u, \vec u ; \vec x , y)
|
|
120 |
\exists z^\safe . A_f (s_i u, \vec u ; \vec x , z)
|
| 122 |
121 |
\]
|
| 123 |
122 |
|
|
123 |
So let us assume $\exists y^\safe . A_f (u , \vec u ; \vec x , y) $. Then there exists $w$ such that $\safe(w)$ and
|
|
124 |
$A_f (u , \vec u ; \vec x , w) $.
|
|
125 |
|
|
126 |
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
|
|
127 |
$\addtosequence(w,z,w')$. Observe also that we have $\pref(|u|,s_i u,u)$
|
|
128 |
|
|
129 |
So we have, for $k=|u|$:
|
|
130 |
|
|
131 |
$$ \beta (k, w', y) \cand \beta (k+1 ,w', z) \cand B (u , \vec u ; \vec x , y , z).$$
|
|
132 |
|
|
133 |
and we can conclude that
|
|
134 |
\[
|
|
135 |
\exists w'^\safe . \left(
|
|
136 |
\begin{array}{ll}
|
|
137 |
&
|
|
138 |
%Seq(z) \cand
|
|
139 |
\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w' , y_0) ) \cand \beta(|u|+1, w',z ) \\
|
|
140 |
\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}) )
|
|
141 |
\end{array}
|
|
142 |
\right)
|
|
143 |
\]
|
|
144 |
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,
|
|
145 |
\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.
|
|
146 |
|
| 124 |
147 |
\anupam{here need to `add' element to the computation sequence. Need to do this earlier in the paper.}
|
| 125 |
148 |
|
| 126 |
149 |
\anupam{for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
|