Evgeny Makarov (INRIA) |
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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.75.3 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |