We characterize computationally the functions provable in second order
logic with set existence restricted to natural classes of
first order formulas.
We showed elsewhere that set existence for first-order formulas
yields precisely the Kalmar-elementary functions.
Here we show that a classification of first-order set-existence
by implicational rank yields
a natural hierarchy of complexity classes:
The functions (over words) constructively provable with set
existence forformulas of implicational rank up to k are
precisely the functions computable in deterministic time exp_k(n),
whereexp_0 is P, and exp_{k+1} is 2 to the power exp_k.
Moreover, set-existence for positive formulas yields exactly PTime,
even if the underlying logic is classical.
Our results can be formulated in a formgeneric to all free algebras.
In particular, we conclude that a function over N computable
by a program over N is provably terminating using set existence
of rank up to k iff it iscomputable in deterministic space E_k(n),
where E_0(n)=n, and E_{k+1} is 2 to the power E_k.
