| 1 |
1 |
\section{Completeness}\label{sect:completeness}
|
| 2 |
|
|
|
2 |
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.
|
| 3 |
3 |
The main result of this section is the following:
|
| 4 |
4 |
|
| 5 |
5 |
\begin{theorem}
|
| 6 |
6 |
\label{thm:completeness}
|
| 7 |
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 |
|
\begin{proof}[Sketch](A more detailed proof can be found in Appendix \ref{appendix:completeness})
|
| 10 |
|
|
| 11 |
|
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. The two key cases are thus those of predicative recursion and predicative minimisation.
|
|
9 |
\begin{proof}[Proof sketch]
|
|
10 |
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.
|
|
11 |
Naturally, the interesting cases are predicative recursion and predicative minimisation.
|
| 12 |
12 |
|
| 13 |
|
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 to have a decoding predicate $\beta (k, w, y)$ (the $k$th element of the sequence represented by $w$ is $y$) 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$.
|
|
13 |
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$.
|
|
14 |
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)$'').
|
|
15 |
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:bounded-minimisation}, to find appropriate length bounds.
|
|
16 |
% 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$.
|
| 14 |
17 |
|
| 15 |
18 |
|
| 16 |
|
For predicative minimisation finally, assume $f$ is defined by $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$. 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:
|
|
19 |
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).
|
|
20 |
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:
|
| 17 |
21 |
\[
|
| 18 |
22 |
\begin{array}{rl}
|
| 19 |
23 |
&\left(
|
| ... | ... | |
| 28 |
32 |
\right)
|
| 29 |
33 |
\end{array}
|
| 30 |
34 |
\]
|
| 31 |
|
As in the bounded arithmetic $S_2$ (\cite{Buss86book}, Thm 20, p. 58), $\arith^i$ can prove a minimisation principle for $\cmin{\Sigma^\safe_{i-1}}$ formulas, which we apply to the formula $\exists x^\safe , y^\safe . (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$. From that we can prove the totality of $A_f(\vec u ; \vec x , z)$ as required.
|
|
35 |
As for the analogous bounded arithmetic theory $S^i_2$ (\cite{Buss86book}, Thm 20, p. 58), $\arith^i$ can prove a minimisation principle for $\cmin{\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.
|
| 32 |
36 |
|
| 33 |
37 |
\end{proof}
|
| 34 |
38 |
|