Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\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 $\fphi{i}$. 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.