root / CSL17 / appendix-arithmetic.tex @ 187
Historique | Voir | Annoter | Télécharger (2,56 ko)
| 1 | 187 | pbaillot | \section{An arithmetic for the polynomial hierarchy}\label{appendix:arithmetic}
|
|---|---|---|---|
| 2 | 187 | pbaillot | |
| 3 | 187 | pbaillot | We give here the list of remaining axioms of $\basic$, which are directly inspired by the $\basic$ theory of Buss's bounded arithmetic \cite{Buss86book}:
|
| 4 | 187 | pbaillot | %$\succ{0}(x)$ stand for $2\cdot x$ and $\succ{1}(x)$ stand for $\succ{}(2\cdot x)$,
|
| 5 | 187 | pbaillot | |
| 6 | 187 | pbaillot | $$ |
| 7 | 187 | pbaillot | %\begin{equation}
|
| 8 | 187 | pbaillot | \begin{array}{l}
|
| 9 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}. (y\leq x) \cimp (y \leq \succ{} x) \\
|
| 10 | 187 | pbaillot | \forall x^{\safe}. x \neq \succ{} x\\
|
| 11 | 187 | pbaillot | \forall x^{\safe}.0 \leq x\\
|
| 12 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}.(x\leq y \cand x \neq y) \leftrightarrow \succ{} x \leq y\\
|
| 13 | 187 | pbaillot | \forall x^{\safe}. x\neq 0 \cimp \succ{0}x \neq 0\\
|
| 14 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}. y\leq x \cor x \leq y\\
|
| 15 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}. x\leq y \cand y\leq x \cimp x=y\\
|
| 16 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}, z^{\safe}. x\leq y \cand y\leq z \cimp x\leq z\\
|
| 17 | 187 | pbaillot | |0|=0\\ |
| 18 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}.x\neq 0 \cimp |\succ{0}x|=\succ{}( |x|) \cand |\succ{0}x|= \succ{}(|x|) \\
|
| 19 | 187 | pbaillot | |\succ{}0|=\succ{} 0\\
|
| 20 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}. x\leq y \cimp |x|\leq |y|\\
|
| 21 | 187 | pbaillot | \forall x^{\safe}, y^{\normal}. |x\smsh y|=\succ{}( |x|\cdot |y|)\\
|
| 22 | 187 | pbaillot | \forall y^{\normal}. 0 \smsh y=\succ{} 0\\
|
| 23 | 187 | pbaillot | \forall x^{\safe}. x\neq 0 \cimp 1 \smsh(\succ{0}x)=\succ{0}(1\smsh x) \cand 1 \smsh(\succ{1}x)=\succ{0}(1\smsh x)\\
|
| 24 | 187 | pbaillot | \forall x^{\normal}, y^{\normal}. x \smsh y = y \smsh x\\
|
| 25 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}, z^{\normal}. |x|= |y| \cimp x\smsh z = y\smsh z\\
|
| 26 | 187 | pbaillot | \forall x^{\safe}, u^{\safe}, v^{\safe}, y^{\normal}. |x|= |u|+ |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y)\\
|
| 27 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}. x\leq x+y\\
|
| 28 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}. x\leq y \cand x\neq y \cimp \succ{}(\succ{0}x) \leq \succ{0}y \cand \succ{}(\succ{0}x) \neq \succ{0}y\\
|
| 29 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}. x+y=y+x\\
|
| 30 | 187 | pbaillot | \forall x^{\safe}. x+0=x\\
|
| 31 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}. x+\succ{}y=\succ{}(x+y)\\
|
| 32 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}, z^{\safe}. (x+y)+z=x+(y+z)\\
|
| 33 | 187 | pbaillot | \forall x^{\safe}, y^{\safe}, z^{\safe}. x+y \leq x+z \leftrightarrow y\leq z\\
|
| 34 | 187 | pbaillot | \forall x^{\normal} x\cdot 0=0\\
|
| 35 | 187 | pbaillot | \forall x^{\normal}, y^{\safe}. x\cdot(\succ{}y)=(x\cdot y)+x\\
|
| 36 | 187 | pbaillot | \forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x\\
|
| 37 | 187 | pbaillot | \forall x^{\normal}, y^{\safe}, z^{\safe}. x\cdot(y+z)=(x\cdot y)+(x\cdot z)\\
|
| 38 | 187 | pbaillot | \forall x^{\normal}, y^{\safe}, z^{\safe}. x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \leftrightarrow y\leq z)\\
|
| 39 | 187 | pbaillot | \forall x^{\normal} x\neq 0 \cimp |x|=\succ{}(\hlf{x})\\
|
| 40 | 187 | pbaillot | \forall x^{\safe}, y^{\normal}. x= \hlf{y} \leftrightarrow (\succ{0}x=y \cor \succ{}(\succ{0}x)=y)
|
| 41 | 187 | pbaillot | \end{array}
|
| 42 | 187 | pbaillot | %\end{equation}
|
| 43 | 187 | pbaillot | $$ |