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

 We have presented a ramified arithmetic parameterized by the formulas on which induction is allowed. The hierarchy of induction formulas 

$\Sigma_i^{\safe}$ is defined by the number of alternances of safe (unbounded) quantifiers. 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 analog 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.

 Several natural and interesting questions remain open. First we have   used a two-sorted logic, but we believe that this approach could be implemented with a modal logic, as in \cite{BelHof:02}. The exposition would be more complicated, but arguably more elegant.

 Second this work has provided an indirect comparison between $\arith^i$ and the bounded arithmetic $S_2^i$. We think a direct relationship could also be established, by defining an embedding of  $\arith^i$  into  $S_2^i$. This is left for 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.

@inproceedings{Lasson11,
+  author    = {Marc Lasson},
+  title     = {Controlling Program Extraction in Light Logics},
+  booktitle = {Proceedings of Typed Lambda Calculi and Applications - 10th International Conference,
+               {TLCA} 2011},
+  pages     = {123--137},
+  series    = {LNCS},
+  volume    = {6690},
+  publisher = {Springer},
+  year      = {2011}
+ }
+