Révision 233 CSL17/intro.tex
| intro.tex (revision 233) | ||
|---|---|---|
| 54 | 54 |
%Then we describe an encoding of sequences which will be instrumental in the proof of our result. |
| 55 | 55 |
We present our arithmetic theories $\arith^i$ in Sect.~\ref{sect:arithmetic} and prove our soundness result, that the provably total functions of $\arith^i$ are in $\fph_i$, in Sect.~\ref{sect:soundness}. Finally, we prove the completeness result, that all $\fph_i$ functions have a representation provably total in $\arith^i$, in Sect.~\ref{sect:completeness}, and present conclusions in Sect.~\ref{sect:conclusion}.
|
| 56 | 56 |
|
| 57 |
We are able to include only brief outlines of our technical results in this paper, in particular for our soundness and completeness results, Thms.~\ref{sect:soundness} and \ref{thm:completeness} respectively.
|
|
| 58 |
More detailed proofs can be found in the technical report \cite{BaiDas17:fph-techreport}.
|
|
| 57 | 59 |
|
| 60 |
|
|
| 58 | 61 |
% \patrick{
|
| 59 | 62 |
% \begin{itemize}
|
| 60 | 63 |
% \item our goal: design an unbounded arithmetic for FPH. |
Formats disponibles : Unified diff