Calibrating computational feasibility by abstraction rank

We characterize computationally the functions provable in second order logic with set existence restricted to natural classes of first order formulas. A classification of first-order set-existence by implicational rank yields a natural hierarchy of complexity classes within the class of Kalmar-elementary functions: The functions over {0, 1}* constructively provable using set existence for formulas of implicational rank ≤k are precisely the functions computable in deterministic time O(exp_k(n)), where exp₀=U_k(λn.n^k), and exp_k+1=2(exp_k).¹ In particular, set-existence for positive formulas yields exactly PTime. We thus obtain lean and natural formalisms for codifying feasible mathematics, which are expressive both in allowing second order definitions and reasoning, and in incorporating equational programming and reasoning about program convergence in a direct and uncoded style. Through a formula-as-type morphism, we also obtain a link with lambda definability, which we exhibit in the full paper: The functions over {0, 1}* definable in the polymorphic lambda calculus F₂ over a base of type of words, using first-order type-arguments of rank ≤k, are precisely the functions computable in deterministic time O(exp_k(n)).² The poly-time case was proved (directly) in [15].