Révision 218 CSL17/arithmetic.tex
| arithmetic.tex (revision 218) | ||
|---|---|---|
| 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 is defined by the set of functions (and constants) symbols $\{ 0, \succ{} , + , \times, \smsh , |\cdot|, \hlf{}.\}$ and the set of predicate symbols
|
| 4 |
$\{\leq, \safe, \normal \}$.
|
|
| 4 |
$\{\leq, \safe, \normal \}$. The intended meaning of $|x|$ is the length of $x$ seen as a binary string, and that of $\smash(x,y)$ is $2^{|x||y|}$, so a string of length $|x||y|+1$.
|
|
| 5 |
|
|
| 5 | 6 |
We use classical logic connectives $\neg$, $\cand$, $\cor$, $\forall$, $\exists$. The formula $A \cimp B$ will be a notation for $\neg A \cor B$. |
| 6 | 7 |
We will also use as shorthand notations: |
| 7 | 8 |
$$ (s=t) = (s\leq t) \cand (t\leq s), \quad (s\neq t) = \neg(s=t).$$ |
Formats disponibles : Unified diff