There is no recursive axiomatization for feasible functionals of type 2

The author shows a class of type-two feasible functionals, C ₂, that satisfies Cook´s conditions, (1990) and cannot be expressed as the lambda closure of type-one poly-time functions and any recursively enumerable set of type-two feasible functionals. Further, no class of total type-two functionals containing this class is representable as the lambda closure of a recursively enumerable set of type-two total computable functionals and type-one poly-time functions. The definition of C₂ provides a clear computational procedure for functionals of C₂. Using functionals of class C₂ a more general notion of polynomial-time reducibility between two arbitrary type-one functions can be introduced