Révision 236 CSL17/arithmetic.tex

arithmetic.tex (revision 236)
1 1 
\section{An arithmetic for the polynomial hierarchy}\label{sect:arithmetic}
2 2 
%Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$.
3 3 
Our base language consists of constant and function symbols $\{ 0, \succ{} , + , \times, \smsh , |\cdot|, \hlf{}.\}$ and predicate symbols
4 
 $\{\leq, \safe, \normal \}$. The function symbols are interpreted in the intuitive way, with $|x|$ denoting the length of $x$ seen as a binary string, and $\smash(x,y)$ denoting $2^{|x||y|}$, so a string of length $|x||y|+1$.
4 
 $\{\leq, \safe, \normal \}$. The function symbols are interpreted in the intuitive way, with $|x|$ denoting the length of $x$ seen as a binary string, and $x\smsh y$ denoting $2^{|x||y|}$, so a string of length $|x||y|+1$.
5 5 
 We may write $\succ{0}(x)$ for $2\cdot x$, $\succ{1}(x)$ for $\succ{}(2\cdot x)$, and $\pred (x)$ for $\hlf{x}$, to better relate to the $\bc$ setting.
6 6
7 7 
We consider formulas of classical first-order logic, over $\neg$, $\cand$, $\cor$, $\forall$, $\exists$, along with usual shorthands and abbreviations.

Formats disponibles : Unified diff