Révision 199 CSL17/completeness.tex

completeness.tex (revision 199)
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
  
  
    

  		












Formats disponibles :
  Unified diff