Révision 176 CSL17/arithmetic.tex

arithmetic.tex (revision 176)
8 8 
\forall x^\safe . \safe (\succ{} x) \\
9 9 
\forall x^\safe . 0 \neq \succ{} (x) \\
10 10 
\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\
11 
\forall x^\safe . (x = 0 \cor \exists y^\safe.\  x = \succ{} y   )
11 
\forall x^\safe . (x = 0 \cor \exists y^\safe.\  x = \succ{} y   )\\
12 
\forall x^\safe, y^\safe . \safe(x+y)\\
13 
\forall u^\normal, x^\safe . \safe(u\times x) \\
14 
\forall u^\normal , v^\normal . \safe (u \smsh v)
12 15 
\end{array}
13 16 
\]
14 17 
\anupam{in fact, we use essentially the same language, so just take Buss' Basic axioms after proper typing. Should also add the symbol $\hlf{\cdot}$ for binary predecessor then we have the full language of bounded arithmetic.}
......
19 22 
[Derived functions and notations]
20 23 
We write $1,2,3,\dots$ for the terms $\succ{} 0, \succ{} \succ{} 0, \succ{} \succ{} \succ{} 0 \dots$, and frequently omit the $\times$ symbol.
21 24 
We define the functions $\succ 0 x , \succ 1 x$ as $2 x$ and $2x +1$ respectively.
25 

  		





  
  26
  
    
Need $bit$, $\beta$ , $\pair{}{}{}$.


  		





  22
  27
  
    
\end{definition}


  		





  23
  28
  
    

  		





  24
  29
  
    
(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers)


  		





  ......




  30
  35
  
    

  		





  31
  36
  
    
\begin{definition}


  		





  32
  37
  
    
[Quantifier hierarchy]


  		





  33
  
  
    
We define:


  		





  34
  
  
    
\begin{itemize}


  		





  35
  
  
    
	\item $\Sigma^\safe_0 = \Pi^\safe_0 $ = sharply bounded formulae. 


  		





  36
  
  
    
	\item (Increase with predicative quantifiers)


  		





  37
  
  
    
\end{itemize}	


  		





  
  38
  
    
$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded.


  		





  
  39
  
    
We define $\Sigma^\safe_{i+1}$ as the closure of $\Pi^\safe_i $ under $\cor, \cand $, safe existentials and sharply bounded quantifiers.


  		





  
  40
  
    
We define $\Pi^\safe_{i+1}$ as the closure of $\Sigma^\safe_i $ under $\cor, \cand $, safe universals and sharply bounded quantifiers.


  		





  38
  41
  
    
\end{definition}


  		





  39
  42
  
    

  		





  40
  43
  
    

  		












Formats disponibles :
  Unified diff