Provably Total Functions of Arithmetic with Basic Terms
Logic in Computer Science
2012-01-06 v1
Abstract
A new characterization of provably recursive functions of first-order arithmetic is described. Its main feature is using only terms consisting of 0, the successor S and variables in the quantifier rules, namely, universal elimination and existential introduction.
Cite
@article{arxiv.1201.1121,
title = {Provably Total Functions of Arithmetic with Basic Terms},
author = {Evgeny Makarov},
journal= {arXiv preprint arXiv:1201.1121},
year = {2012}
}
Comments
In Proceedings DICE 2011, arXiv:1201.0345