Révision 166 CSL17/arithmetic.tex
| arithmetic.tex (revision 166) | ||
|---|---|---|
| 1 |
\section{A two-sorted arithmetic for the polynomial hierarchy}
|
|
| 1 |
\section{An arithmetic for the polynomial hierarchy}
|
|
| 2 | 2 |
|
| 3 | 3 |
(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers) |
| 4 | 4 |
|
| ... | ... | |
| 16 | 16 |
\end{definition}
|
| 17 | 17 |
|
| 18 | 18 |
\begin{definition}
|
| 19 |
Define the theory $\arith^i$ as $\basic + \cpind{\Sigma^\safe_i }$
|
|
| 19 |
Define the theory $\arith^i$ consisting of the following axioms: |
|
| 20 |
\begin{itemize}
|
|
| 21 |
\item $\basic$; |
|
| 22 |
\item $\cpind{\Sigma^\safe_i } $:
|
|
| 23 |
\item $\forall \vec x \in \normal . \exists y \in \safe . A \cimp \forall \vec x \in \normal .\exists y\in \normal . A$ (raising) . |
|
| 24 |
\end{itemize}
|
|
| 20 | 25 |
\end{definition}
|
| 21 | 26 |
|
| 22 | 27 |
|
Formats disponibles : Unified diff