Révision 253 CSL17/tech-report/appendix-completeness.tex

appendix-completeness.tex (revision 253)
38 38 
	%\begin{proof}
39 39 
	%\end{proof}
40 40 
	\begin{proof}
41 
	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).
41 
	This Lemma is proved by using the same method as for the proof of the analogous result in the bounded arithmetic $S_2^{i}$ (see \cite{Buss86book}, Thm 20, p. 58).
42 42
43 43 
	Let $A(x)$ be a  $\Sigma^\safe_{i-1}$ formula, with $x$ in $\safe$. We define the formula $B(a,b,c)$ as:
44 44 
	$$ \forall x^{\safe}. (x < |a| \moins b \cimp \zerobit(x,c)) \cand \forall y^{\safe}<c. \neg A(y) \cand \exists y^{\safe} < 2^{|a|\moins b}.A(c+y)$$
......
60 60 
Moreover we have: $A(a) \cand B(a,b,c) \cimp c\leq a$.
61 61 
From these three statements we deduce:
62 62 
$$(A(a) \cand a \neq 0 \cand b<|a| \cand \exists x^{\safe} \leq a. B(a,b,x)) \cimp \exists x^{\safe } \leq a.B(a,\succ{} b,x).$$
63 
Note that here we have used the fact that we are in classical logic.
64 

  		





  63
  65
  
    
The formula $\exists x\leq a. B(a,b,c)$ is in $\Sigma^{\safe}_{i}$, so by $\Sigma^{\safe}_{i}$-LIND on the formula $\exists x\leq a. B(a,b,c)$, with the variable $b$ which is in $\normal$,  we obtain:


  		





  64
  66
  
    
$$(A(a) \cand a \neq 0 ) \cimp \exists x^{\safe } \leq a.B(a,|a|,x).$$


  		





  65
  
  
    
\patrick{Anupam, is it a valid instance of LIND? I think it is.}


  		





  66
  
  
    

  		





  67
  67
  
    
But $B(a,|a|,x)$ implies $(\forall y^{\safe}<x. \neg A(y))\cand A(x)$, so we have proven:


  		





  68
  68
  
    
$$(A(a) \cand a \neq 0 ) \cimp (\exists x^{\safe } \leq a. (\forall y^{\safe}<x. \neg A(y))\cand A(x))$$


  		





  69
  69
  
    
which is the $\Sigma_{i-1}^{\safe}$ axiom for $A$.


  		





  70
  70
  
    
	\end{proof}


  		





  71
  
  
    
%	\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.}


  		





  72
  71
  
    
	


  		





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


  		





  74
  73
  
    
	\[


  		












Formats disponibles :
  Unified diff