Polynomially Bounded Recursive Realizability
Salehi, Saeed
Notre Dame J. Formal Logic, Tome 46 (2005) no. 3, p. 407-417 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
A polynomially bounded recursive realizability, in which the recursive functions used in Kleene's realizability are restricted to polynomially bounded functions, is introduced. It is used to show that provably total functions of Ruitenburg's Basic Arithmetic are polynomially bounded (primitive) recursive functions. This sharpens our earlier result where those functions were proved to be primitive recursive. Also a polynomially bounded schema of Church's Thesis is shown to be polynomially bounded realizable. So the schema is consistent with Basic Arithmetic, whereas it is inconsistent with Heyting Arithmetic.
Publié le : 2005-10-14
Classification:  provably total function,  Basic Arithmetic,  Basic Logic,  realizability,  03F30,  03F50 
@article{1134397659,
     author = {Salehi, Saeed},
     title = {Polynomially Bounded Recursive Realizability},
     journal = {Notre Dame J. Formal Logic},
     volume = {46},
     number = {3},
     year = {2005},
     pages = { 407-417},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1134397659}
}

Salehi, Saeed. Polynomially Bounded Recursive Realizability. Notre Dame J. Formal Logic, Tome 46 (2005) no. 3, pp.  407-417. http://gdmltest.u-ga.fr/item/1134397659/