Révision 234 CSL17/completeness.tex

completeness.tex (revision 234)
32 32 
\right)
33 33 
\end{array}
34 34 
\]
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.
35 
As for the analogous bounded arithmetic theory $S^i_2$ (\cite{Buss86book}, Thm 20, p. 58),  $\arith^i$ can prove a \emph{minimisation} principle for $\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.
36 36 

  		





  37
  37
  
    
\end{proof}


  		





  38
  38
  
    

  		












Formats disponibles :
  Unified diff