Révision 231 CSL17/arithmetic.tex

arithmetic.tex (revision 231)
12 12 
 We will assume, without loss of generality, that formulas are in \textit{De Morgan normal form}, that is to say that in formulas negation can only occur on atomic formulas, and that there is not any occurrence of a subformula of the form $\neg \neg A$.
13 13
14 14
15 
 We write $\exists x^{N_i} . A$ or $\forall x^{N_i} . A$ for $\exists x . (N_i (x) \cand A)$ and $\forall x . (N_i (x) \cimp A)$ respectively. We refer to these as \emph{safe} quantifiers.
15 
 We write $\exists x^{N_i} . A$ or $\forall x^{N_i} . A$ for $\exists x . (N_i (x) \cand A)$ and $\forall x . (N_i (x) \cimp A)$ respectively. We refer to  $\exists x^{N_0}$,  $\forall x^{N_0}$ as \emph{safe} quantifiers.
16 16 
 We also write $\exists x^\normal \leq |t| . A$ for $\exists x^\normal . ( x \leq |t| \cand A )$ and $\forall x^\normal \leq |t|. A $ for $\forall x^\normal. (x \leq |t| \cimp A )$. We refer to these as \emph{sharply bounded} quantifiers, as in bounded arithmetic.
17 17 

  		





  18
  18
  
    

  		












Formats disponibles :
  Unified diff