Polynomially bounded recursive realizability (Q817959)

The strength of a theory can be measured by characterizing its provably total functions. Those of Heyting Arithmetic (HA), for example, are known to be specified as recursive according to Kleene's recursive realizability. The author proved in his earlier work that provably total functions of Basic Arithmetic (BA) are primitive recursive, where BA was introduced by Ruitenburg in a similar way as HA by featuring his Basic Logic in place of intuitionistic logic. In this paper the author introduces a polynomially bounded recursive realizability by restricting the recursive functions used in Kleene's realizability to the polynomially bounded ones, and proves that the earlier result is sharpened by them, where the polynomially bounded ones are primitive recursive. It is also shown that a polynomially bounded schema of Church's Thesis is realizable in the polynomially bounded sense. The schema, therefore, is consistent with BA, whereas it is inconsistent with HA.