Révision 198

CSL17/completeness.tex (revision 198)
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
  14
  
    
\paragraph*{Predicative minimisation}


  		





  14
  15
  
    
Suppose $f(\vec u ; \vec x)$ is defined as $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$. 


  		





  15
  
  
    
By definition $g$ is in $\mubci{i-2}$, and so by the inductive hypothesis there is a $\Sigma_{i-1}$ formula $A_g (\vec u , \vec x , x , y)$ computing the graph of $g$ such that,


  		





  
  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,


  		





  16
  17
  
    
\[


  		





  17
  18
  
    
\arith^i \proves \forall \vec u^\normal . \forall \vec x^\safe , x^\safe . \exists ! y^\safe . A_g(\vec u , \vec x , x , y)


  		





  18
  19
  
    
\]


  		





  ......




  31
  32
  
    
\right)


  		





  32
  33
  
    
\end{array}


  		





  33
  34
  
    
\]


  		





  34
  
  
    
Notice that $A_f$ is $\Pi_{i-1}$, since $A_g$ is $\Sigma_{i-1}$ and occurs only in negative context above, with additional safe universal quantifiers occurring in positive context.


  		





  35
  
  
    
In particular this means $A_f$ is $\Sigma_i$.


  		





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


  		





  
  36
  
    
In particular this means $A_f$ is $\Sigma^{\safe}_i$.


  		





  36
  37
  
    

  		





  37
  38
  
    
Now, to prove totality of $A_f$, we rely on $\Sigma^\safe_{i-1}$-minimisation, which is a consequence of $\cpind{\Sigma^\safe_i}$:


  		





  38
  39
  
    

  		





  ......




  41
  42
  
    
$\arith^i \proves \cmin{\Sigma^\safe_{i-1}}$.	


  		





  42
  43
  
    
\end{lemma}


  		





  43
  44
  
    
% see Thm 20 p. 58 in Buss' book.


  		





  44
  
  
    
\begin{proof}


  		





  45
  
  
    
\todo{}


  		





  46
  
  
    
\end{proof}


  		





  
  45
  
    
%\begin{proof}


  		





  
  46
  
    
%\end{proof}


  		





  
  47
  
    
 This Lemma is proved by using the same method as for the proof of the analogous result in the bounded arithmetic $S_2^{i+1}$ (see \cite{Buss86book}, Thm 20, p. 58).


  		





  47
  48
  
    

  		





  
  49
  
    
\patrick{Examining it superficially, I think indeed the proof of Buss can be adapted to our setting. But we should probably look again at that with more scrutiny.}


  		





  
  50
  
    

  		





  48
  51
  
    
Now, working in $\arith^i$, let $\vec u \in \normal , \vec x \in \safe$ and let us prove:


  		





  49
  52
  
    
\[


  		





  50
  53
  
    
\exists !z^\safe  . A_f(\vec u ; \vec x , z)


  		












  

    
      CSL17/preliminaries.tex	(revision 198)
    
  






  156
  156
  
    

  		





  157
  157
  
    
where $\mu y.h(\vec u; \vec x , y)\mod 2 = 0$ is the least $y$ such that the equality holds.


  		





  158
  158
  
    

  		





  
  159
  
    
We will denote this function $f$ as $\mu y^{+1} . h(\vec u ; \vec x , y) =_2 0$.


  		





  
  160
  
    

  		





  159
  161
  
    
If $\Phi$ is a class of functions, we denote by $\mubc(\Phi)$ the class obtained as $\mubc$ but adding $\Phi$ to the set of initial functions.


  		





  160
  162
  
    
 


  		





  161
  163
  
    
\item For each $i\geq 0$, $\mubc^i$ is the set of $\mubc$ functions obtained by at most $i$ applications of predicative minimization. So $\mubc^0=BC$ and $\mubc =\cup_i \mubc^i$.


  		





  ......




  163
  165
  
    
 \end{definition}


  		





  164
  166
  
    
 One then obtains:


  		





  165
  167
  
    
 \begin{theorem}[\cite{BellantoniThesis, Bellantoni95}]


  		





  166
  
  
    
 The class of functions representable by $\mubc$ programs is $\fph$, and for each $i$ the class representable by $\mubc^i$ programs is $\fphi{i}$.


  		





  
  168
  
    
 The class of functions representable by $\mubc$ programs is $\fph$, and for each $i\geq 1$ the class representable by $\mubc^{i-1}$ programs is $\fphi{i}$.


  		





  167
  169
  
    
 \end{theorem}


  		





  168
  170
  
    
 We will also need an intermediary lemma, also proved in \cite{BellantoniThesis}.


  		





  169
  171
  
    
 \begin{definition}


  		












Formats disponibles :
  Unified diff