Révision 171
| CSL17/arithmetic.tex (revision 171) | ||
|---|---|---|
| 1 | 1 |
\section{An arithmetic for the polynomial hierarchy}
|
| 2 | 2 |
Our base language is $\{ 0, \succ 0, \succ 1, \pred, + , \times, \smsh , |\cdot| , \leq \}$.
|
| 3 | 3 |
|
| 4 |
The $\basic$ axioms are as follows: |
|
| 5 |
\[ |
|
| 6 |
\begin{array}{l}
|
|
| 7 |
\safe (0) \\ |
|
| 8 |
\succ 0 = 0 \\ |
|
| 9 |
\safe (x) \cimp \safe (\succ i x) \\ |
|
| 10 |
\end{array}
|
|
| 11 |
\] |
|
| 4 | 12 |
|
| 5 | 13 |
(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers) |
| 6 | 14 |
|
| CSL17/ph-macros.tex (revision 171) | ||
|---|---|---|
| 36 | 36 |
\renewcommand{\succ}[1]{s_{#1}}
|
| 37 | 37 |
\newcommand{\cond}{C}
|
| 38 | 38 |
\newcommand{\smsh}{\#}
|
| 39 |
\newcommand{\pair}[3]{\langle ; #1,#2 , #3 \rangle}
|
|
| 39 | 40 |
|
| 41 |
|
|
| 40 | 42 |
\newcommand{\safe}{{S}}
|
| 41 | 43 |
\newcommand{\normal}{N}
|
| 42 | 44 |
|
| CSL17/completeness.tex (revision 171) | ||
|---|---|---|
| 62 | 62 |
So we have proven $\exists z^\safe . A_f(\vec u ; \vec x , z)$, and unicity can be easily verified. |
| 63 | 63 |
|
| 64 | 64 |
\paragraph*{Predicative recursion on notation}
|
| 65 |
|
|
| 66 |
\anupam{Assume access to the following predicates (makes completeness easier, soundness will be okay):
|
|
| 67 |
\begin{itemize}
|
|
| 68 |
% \item $\pair x y z $ . ``$z$ is the sequence that appends $y$ to the sequence $x$'' |
|
| 69 |
\item $\pair x y z$. ``$z$ is the sequence that prepends $x$ to the sequence $y$'' |
|
| 70 |
\item $\beta (i; x ,y)$. ``The $i$th element of the sequence $x$ is $y$.'' |
|
| 71 |
\end{itemize}
|
|
| 72 |
} |
|
| 73 |
|
|
| 65 | 74 |
Now suppose that $f$ is defined by PRN: |
| 66 | 75 |
\[ |
| 67 | 76 |
\begin{array}{rcl}
|
| CSL17/soundness.tex (revision 171) | ||
|---|---|---|
| 7 | 7 |
If $\arith^i$ proves $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; \vec x)$ such that $\Nat \models A(\vec u ; \vec x , f(\vec u ; \vec x))$.
|
| 8 | 8 |
\end{theorem}
|
| 9 | 9 |
|
| 10 |
For this we will use length-bounded witnessing. |
|
| 11 |
|
|
| CSL17/main.tex (revision 171) | ||
|---|---|---|
| 87 | 87 |
\input{pv-theories}
|
| 88 | 88 |
|
| 89 | 89 |
\end{document}
|
| 90 |
\grid |
|
Formats disponibles : Unified diff