Intuitionistic formal theories with realizability in subrecursive classes Original Research Article

A family of formal intuitionistic theories is proposed (with each theory equivalent to the Peano arithmetic by expressive power) with realizability of proved formulas in several subrecursive classes, e.g. Grzegorczyk classes, polynomial-time computable functions class, etc. ∀xA(x,f(x)) Algorithm extraction for∀x∃yA(x, y) is shown for various classes of bounded complexity. The results on polynomial computability are closely connected to work on the Bounded Arithmetic by S. Buss.