Weak constructive second order arithmetic with extracting polynomial time computable algorithms

A family of weak constructive theories is built in this work. The theories contain arithmetic and a theory of natural valued functions with natural arguments. These functions are polynomially bounded and are computable in a time polynomially bounded in values of their arguments. Theory languages contain functional constants for addition, and multiplication and equality predicate. Other functional constants also may be used if their functions satisfy the polynomial boundedness conditions above. Polynomial time computable (in numeric values of the arguments) witness functions for proved formulas can be algorithmically extracted from the proofs of these theories. If one of the arguments of witness is a function, then this function is used in the witness algorithm as an oracle.