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

\section{Conclusions}

\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.