| 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^{\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))$.
|
|
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_f(\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 |
11 |
We proceed by structural induction on a $\mubc^{i-1} $ program, dealing with each case in the proceeding paragraphs.
|
| 12 |
12 |
|
| 13 |
|
The property is easily verified for the class of initial functions of $\mubci{i-1}$: constant, projections, (binary) successors, predecessor, conditional. Now let us examine the three constructions: predicative minimisation, predicative (safe) recursion and composition.
|
|
13 |
The property is easily verified for the class of initial functions of $\mubci{i-1}$: constant, projections, (binary) successors, predecessor, conditional. \patrick{Maybe we can refer here to Sect. \ref{sect:graphsbasicfunctions}.} Now let us examine the three constructions: predicative minimisation, predicative (safe) recursion and composition.
|
| 14 |
14 |
\paragraph*{Predicative minimisation}
|
| 15 |
15 |
Suppose $f(\vec u ; \vec x)$ is defined as $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$.
|
| 16 |
16 |
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,
|
| ... | ... | |
| 175 |
175 |
|
| 176 |
176 |
\todo{elaborate}
|
| 177 |
177 |
|
| 178 |
|
\paragraph*{Other cases}
|
| 179 |
|
\todo{}
|
|
178 |
The proof of Thm \ref{thm:completeness} is thus completed.
|
| 180 |
179 |
|
| 181 |
180 |
|
| 182 |
181 |
|
| ... | ... | |
| 200 |
199 |
|
| 201 |
200 |
|
| 202 |
201 |
|
| 203 |
|
|