## Paper: Calibrating computational feasibility by abstraction rank (at LICS 2002)

**Daniel Leivant**

### Abstract

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.

### BibTeX

@InProceedings{Leivant-Calibratingcomputat, author = {Daniel Leivant}, title = {Calibrating computational feasibility by abstraction rank}, booktitle = {Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS 2002)}, year = {2002}, month = {July}, pages = {345--354}, location = {Copenhagen, Denmark}, publisher = {IEEE Computer Society Press} }