Provably Total Functions of Arithmetic with Basic Terms
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.
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2012-01-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1201.1121v1 |