| 1 |
1 |
\section{An arithmetic for the polynomial hierarchy}
|
| 2 |
2 |
%Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$.
|
| 3 |
|
Our base language is defined by the set of functions (and constants) symbols $\{ 0, \succ{} , + , \times, \smsh , |\cdot|\}$ and the set of predicate symbols
|
|
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 |
4 |
$\{\leq, \safe, \normal \}$.
|
| 5 |
5 |
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 |
6 |
We will also use as shorthand notations:
|
| ... | ... | |
| 8 |
8 |
We call \textit{atomic formulas} formulas of the form $(s\leq t)$ or $(s=t)$.
|
| 9 |
9 |
As we are in classical logic, 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 subformula of the form $\neg \neg A$.
|
| 10 |
10 |
|
|
11 |
In the sequel $\succ{0}(x)$ stand for $2\cdot x$ and $\succ{1}(x)$ stand for $\succ{}(2\cdot x)$,
|
| 11 |
12 |
Now, let us describe the axioms we are considering.The $\basic$ axioms are as follows:
|
| 12 |
13 |
\[
|
| 13 |
14 |
\begin{array}{l}
|
| ... | ... | |
| 19 |
20 |
\forall x^\safe, y^\safe . \safe(x+y)\\
|
| 20 |
21 |
\forall u^\normal, x^\safe . \safe(u\times x) \\
|
| 21 |
22 |
\forall u^\normal , v^\normal . \safe (u \smsh v)\\
|
| 22 |
|
\forall u^\normal \safe(u)
|
|
23 |
\forall u^\normal \safe(u) \\
|
|
24 |
\forall u^\normal \safe(\hlf{u})\\
|
|
25 |
\forall x^\safe \safe(|x|)
|
| 23 |
26 |
\end{array}
|
| 24 |
27 |
\]
|
|
28 |
\patrick{did I type writly the 2 last axioms?}
|
|
29 |
|
|
30 |
and the list of axioms of Appendix \ref{appendix:arithmetic}, coming from \cite{Buss86book}.
|
|
31 |
|
| 25 |
32 |
\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.}
|
| 26 |
33 |
|
| 27 |
34 |
|