Révision 197 CSL17/completeness.tex
| completeness.tex (revision 197) | ||
|---|---|---|
| 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.}
|
Formats disponibles : Unified diff