Révision 171 CSL17/arithmetic.tex

arithmetic.tex (revision 171)
1 1 
\section{An arithmetic for the polynomial hierarchy}
2 2 
Our base language is $\{ 0, \succ 0, \succ 1, \pred, + , \times, \smsh , |\cdot| , \leq \}$.
3 3 

  		





  
  4
  
    
The $\basic$ axioms are as follows:


  		





  
  5
  
    
\[


  		





  
  6
  
    
\begin{array}{l}


  		





  
  7
  
    
\safe (0) \\


  		





  
  8
  
    
\succ 0 = 0 \\


  		





  
  9
  
    
\safe (x) \cimp \safe (\succ i x) \\


  		





  
  10
  
    
\end{array}


  		





  
  11
  
    
\]


  		





  4
  12
  
    

  		





  5
  13
  
    
(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers)


  		





  6
  14
  
    

  		












Formats disponibles :
  Unified diff