root / CSL17 / conclusions.tex @ 157
Historique | Voir | Annoter | Télécharger (1 ko)
| 1 |
\section{Conclusions}
|
|---|---|
| 2 |
|
| 3 |
\subsection{Why not modal?}
|
| 4 |
We have used a two-sorted approach, although we believe that this can be implemented as a modal approach. |
| 5 |
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. |
| 6 |
|
| 7 |
\anupam{One problem: how to deal formally with something like $\Box N (\succ i (;x^N)) $, i.e.\ where $x$ is safe.}
|
| 8 |
\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)$.}
|
| 9 |
|
| 10 |
\anupam{Also, maybe no clear free-cut elimination result? Well no, can probably use Cantini as example.}
|
| 11 |
|
| 12 |
\anupam{By the way, Cantini asks for the provably total function of arbitrary safe induction. We kind of answer that with `PH'.}
|
| 13 |
|
| 14 |
\subsection{Comparison to PVi and Si2}
|
| 15 |
We believe our theories can be embedded into their analogues, again generalising results of Bellantoni. |