\section{Conclusions}
\label{sect:conclusion}

 We have presented a ramified arithmetic parameterized by the number of alternations of safe (unbounded) quantifiers allowed in induction formulae. We have proved that the system $\arith^i$ with 
$\Sigma_i^{\safe}$-induction corresponds to the $i$th level $\fphi{i}$ of the polynomial hierarchy. This result brings an implicit complexity analogue of Buss' bounded arithmetic in which $S_2^i$ captures  $\fphi{i}$, and suggests that implicit arithmetics can provide fine-grained characterizations of hierarchies of complexity classes.
 
We have used a two-level ramified logic, but we believe that this approach could be implemented with a modal logic, setting $\normal = \Box \safe$, as in \cite{BelHof:02}. The exposition would be more complicated due to the lack of a developed proof theory for first-order modal logic, but arguably more elegant.
At the same time, we could consider \emph{second-order} theories that characterise $\fph$, analogous to the bounded arithmetic theories $V^i$ from \cite{Cook:2010:LFP:1734064}, since the treatment of sequence (de)coding might be more natural, using function symbols. However it seems that delineating the levels of $\fph$ might be more difficult in such a setting.
 
 
 This work has provided an indirect comparison between $\arith^i$ and the bounded arithmetic $S_2^i$. However, we think that a direct relationship could also be established, in particular in the form of an embedding of  $\arith^i$  into  $S_2^i$. This is left to future work.

%\subsection{Why not modal?}
%We have used a two-sorted approach, although we believe that this can be implemented as a modal approach.
%The exposition is a little more complicated, since we will need to rely on proof theory more than local syntax where all variables have declared sorts, however the reasoning in such a theory is likely more elegant.
%
%\anupam{One problem: how to deal formally with something like $\Box N (\succ i (;x^N)) $, i.e.\ where $x$ is safe.}
%\anupam{Actually, not a problem after all. What we actually have is $N(x) \seqar N(\succ i (;x))$, so we can only have $\Box N(\succ i (;x))$ if $\Box N(x)$.}
%
%\anupam{Also, maybe no clear free-cut elimination result? Well no, can probably use Cantini as example.}
%
%\anupam{By the way, Cantini asks for the provably total function of arbitrary safe induction. We kind of answer that with `PH'.}
%
%\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.}
%
%\subsection{Comparison to PVi and Si2}
%We believe our theories can be embedded into their analogues, again generalising results of Bellantoni.