Révision 166
| CSL17/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 |
|
| CSL17/ph-macros.tex (revision 166) | ||
|---|---|---|
| 12 | 12 |
%\newtheorem{definition}[theorem]{Definition}
|
| 13 | 13 |
|
| 14 | 14 |
\newcommand{\Word}{\mathbb{W}}
|
| 15 |
\newcommand{\Nat}{\mathbb{N}}
|
|
| 15 | 16 |
\newcommand{\arith}{B}
|
| 16 | 17 |
\newcommand{\basic}{\mathit{BASIC}}
|
| 17 | 18 |
|
| ... | ... | |
| 33 | 34 |
\renewcommand{\succ}[1]{s_i}
|
| 34 | 35 |
\newcommand{\cond}{C}
|
| 35 | 36 |
|
| 36 |
\newcommand{\safe}{\sigma}
|
|
| 37 |
\newcommand{\normal}{\nu}
|
|
| 37 |
\newcommand{\safe}{{S}}
|
|
| 38 |
\newcommand{\normal}{N}
|
|
| 38 | 39 |
|
| 39 | 40 |
\newcommand{\pv}{\mathit{PV}}
|
| 40 | 41 |
\newcommand{\pvbci}[1]{\pv^{#1}_{\mathrm{BC}}}
|
| CSL17/conclusions.tex (revision 166) | ||
|---|---|---|
| 11 | 11 |
|
| 12 | 12 |
\anupam{By the way, Cantini asks for the provably total function of arbitrary safe induction. We kind of answer that with `PH'.}
|
| 13 | 13 |
|
| 14 |
\anupam{Also, need some weird dual of Barcan's formula, perhaps: $\Box \exists x . A \cimp \exists x . \Box A$. This is validated by the existence of skolem functions, but syntactically requires a further axiom in the absence of comprehension.}
|
|
| 15 |
|
|
| 14 | 16 |
\subsection{Comparison to PVi and Si2}
|
| 15 | 17 |
We believe our theories can be embedded into their analogues, again generalising results of Bellantoni. |
| CSL17/further.tex (revision 166) | ||
|---|---|---|
| 1 |
\section{Further results}
|
|
| CSL17/completeness.tex (revision 166) | ||
|---|---|---|
| 1 |
\section{Completeness}
|
|
| 2 |
|
|
| 3 |
The main result of this section is the following: |
|
| 4 |
|
|
| 5 |
\begin{theorem}
|
|
| 6 |
\label{thm:completeness}
|
|
| 7 |
For every $\mubci{i-1}$ program $f(\vec u ; \vec x)$ (which is in $\fphi i$), there is a $\Sigma_i$ formula $A_f(\vec u, \vec x)$ such that $\arith^i$ proves $\forall \vec u \in \normal . \forall \vec x \in \safe. \exists ! y \in \safe . A_f(\vec u , \vec x , y )$ and $\Nat \models \forall \vec u , \vec x. A(\vec u , \vec x , f(\vec u ; \vec x))$.
|
|
| 8 |
\end{theorem}
|
|
| CSL17/soundness.tex (revision 166) | ||
|---|---|---|
| 1 |
\section{Soundness}
|
|
| CSL17/main.tex (revision 166) | ||
|---|---|---|
| 58 | 58 |
\input{intro}
|
| 59 | 59 |
\input{preliminaries}
|
| 60 | 60 |
\input{sequence-coding}
|
| 61 |
\input{pv-theories}
|
|
| 62 | 61 |
\input{arithmetic}
|
| 62 |
\input{soundness}
|
|
| 63 |
\input{completeness}
|
|
| 64 |
\input{further}
|
|
| 63 | 65 |
|
| 64 | 66 |
\input{conclusions}
|
| 65 | 67 |
|
| 68 |
\newpage |
|
| 69 |
\appendix |
|
| 70 |
\input{pv-theories}
|
|
| 66 | 71 |
|
| 67 | 72 |
%\subparagraph*{Acknowledgements.}
|
| 68 | 73 |
% |
Formats disponibles : Unified diff