Révision 172 CSL17/arithmetic.tex
| arithmetic.tex (revision 172) | ||
|---|---|---|
| 1 | 1 |
\section{An arithmetic for the polynomial hierarchy}
|
| 2 |
Our base language is $\{ 0, \succ 0, \succ 1, \pred, + , \times, \smsh , |\cdot| , \leq \}$.
|
|
| 2 |
Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$.
|
|
| 3 | 3 |
|
| 4 | 4 |
The $\basic$ axioms are as follows: |
| 5 | 5 |
\[ |
| 6 | 6 |
\begin{array}{l}
|
| 7 | 7 |
\safe (0) \\ |
| 8 |
\succ 0 = 0 \\ |
|
| 9 |
\safe (x) \cimp \safe (\succ i x) \\ |
|
| 8 |
\forall x^\safe . \safe (\succ{} x) \\
|
|
| 9 |
\forall x^\safe . 0 \neq \succ{} (x) \\
|
|
| 10 |
\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\
|
|
| 11 |
\forall x^\safe . (x = 0 \cor \exists y^\safe.\ x = \succ{} y )
|
|
| 10 | 12 |
\end{array}
|
| 11 | 13 |
\] |
| 14 |
\anupam{in fact, we use essentially the same language, so just take Buss' Basic axioms after proper typing. Should also add the symbol $\hlf{\cdot}$ for binary predecessor then we have the full language of bounded arithmetic.}
|
|
| 12 | 15 |
|
| 16 |
|
|
| 17 |
|
|
| 18 |
\begin{definition}
|
|
| 19 |
[Derived functions and notations] |
|
| 20 |
We write $1,2,3,\dots$ for the terms $\succ{} 0, \succ{} \succ{} 0, \succ{} \succ{} \succ{} 0 \dots$, and frequently omit the $\times$ symbol.
|
|
| 21 |
We define the functions $\succ 0 x , \succ 1 x$ as $2 x$ and $2x +1$ respectively. |
|
| 22 |
\end{definition}
|
|
| 23 |
|
|
| 13 | 24 |
(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers) |
| 14 | 25 |
|
| 15 | 26 |
Use base theory + sharply bounded quantifiers. |
| 16 | 27 |
|
| 17 |
\anupam{Perhaps use prefix quantifier instead of sharply bounded (a la Ignatovic?), since plays nicer with sharply bounded lemma?}
|
|
| 18 | 28 |
|
| 19 | 29 |
|
| 20 | 30 |
|
Formats disponibles : Unified diff