Révision 198 CSL17/completeness.tex

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)


  		












Formats disponibles :
  Unified diff