| 22 |
22 |
|
| 23 |
23 |
This discipline can be transposed in first-order arithmetic by adding predicates for normal and safe integers and by limiting the induction scheme by allowing induction only on normal integers. The key step we make is to focus our attention on \textit{safe quantifiers} that is to say quantifiers on safe variables. These safe quantifiers will play a r\^ole analogous to bounded quantifiers in bounded arithmetic. In particular we will consider a hierarchy $\Sigma_i^{\safe}$ of formulas according to the number of alternances of safe quantifiers, and we will calibrate the use of induction by restricting the class to which the induction formula can belong. We will finally characterize in this way the levels of the polynomial hierarchy.
|
| 24 |
24 |
|
| 25 |
|
\textit{Outline.} The rest of the paper will proceed as follows. We first give some background on function algebras for FP and FPH respectively. Then we describe an encoding of sequences which will be instrumental in the proof of our result. We present our arithmetical system in Sect. \ref{sect:arithmetic}, prove our soundness result, that is to say the provably total functions are in FPH, in Sect. \ref{sect:soundness}, and our completeness result, all FPH functions are provably total in the arithmetic, in Sect. \ref{sect:completeness}.
|
|
25 |
\textbf{Related work}. To the best of our knowledge, our work is the first characterization of the polynomial hierarchy and its levels in an implicit arithmetic. Our approach is however related to several previous works, and differs either by some of the definitions and/or by the complexity class characterized.
|
|
26 |
|
|
27 |
A first axis of classification between the logics and arithmetics for complexity classes is the way by which they specify functions. The options at stake can be enumerated as follows: (i) \textit{formula specification}, as in first-order bounded arithmetic \cite{Buss86book}, (ii) \textit{equational specification}, as in Leivant's intrinsic theories \cite{Leivant94:intrinsic-theories}, (iii) \textit{combinatory terms} as in applicative theories (e.g. \cite{Strahm03}) or $\lambda$-calculus terms. A second axis, as explained in the introduction, is whether the system is explicit or implicit.
|
|
28 |
|
|
29 |
Our approach in this paper is to use the formula-specification point of view, because it is convenient for the polynomial hierarchy. The arithmetic of \cite{KahOit:13:ph-levels} characterizes PH, but it fits in the explicit approach as it uses axioms defining bounded schemes.
|
|
30 |
Some other works are closer to our methodology in the sense that they are implicit arithmetics and rely on a notion of ramification, but they characterize other complexity classes. Leivant's intrinsic theories \cite{Leivant94:intrinsic-theories} allows to characterize FP, in the equational specification approach, and \cite{Cantini02} obtains an analogous result in the combinatory terms approach. The paper \cite{BelHof:02} also provides a characterization of FP, with two differences: on the one hand induction is on arbitrarily quantified formulas, and on the other hand the underlying logic is not classical logic but a variant of linear logic, with a modality for normal arguments. Finally the paper \cite{OstrinWainer05} also presents an implicit ramified arithmetic, with quantification on safe variables. The difference with our setting is that equational specifications are used instead of formulas, unary integers instead of binary integers, and the class of functions characterized is that of elementary functions.
|
|
31 |
|
|
32 |
|
|
33 |
\textbf{Outline.} The rest of the paper will proceed as follows. We first give some background on function algebras for FP and FPH respectively. Then we describe an encoding of sequences which will be instrumental in the proof of our result. We present our arithmetical system in Sect. \ref{sect:arithmetic}, prove our soundness result, that is to say the provably total functions are in FPH, in Sect. \ref{sect:soundness}, and our completeness result, all FPH functions are provably total in the arithmetic, in Sect. \ref{sect:completeness}.
|
|
34 |
|
|
35 |
|
| 26 |
36 |
% \patrick{
|
| 27 |
37 |
% \begin{itemize}
|
| 28 |
38 |
% \item our goal: design an unbounded arithmetic for FPH.
|