It is shown that all the provably total functions of Basic Arithmetic BA, a theory introduced by Ruitenburg based on Predicate Basic Calculus, are primitive recursive. Along the proof a new kind of primitive recursive realizability to which BA is sound, is introduced. This realizability is similar to Kleene's recursive realizability, except that recursive functions are restricted to primitive recursives.

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. (shrink)

We study Basic Arithmetic BA, which is the basic logic BQC equivalent of Heyting Arithmetic HA over intuitionistic logic IQC, and of Peano Arithmetic PA over classical logic CQC. It turns out that The Friedman translation is applicable to BA. Using this translation, we prove that BA is closed under a restricted form of the Markov rule. Moreover, it is proved that all nodes of a finite Kripke model of BA are classical models of , a fragment of PA with (...) Induction restricted to the formulas made up of ∃, ∧ and/or ∨. We also study an interesting extension of BQC, called EBQC, which is the extension by the axiom schema ⊤ → ⊥ ⇒ ⊥. We show that this extension behaves very like to IQC, and the corresponding arithmetic, EBA shows similarities to HA. (shrink)