A proof theoretic approach to feasible computation
Résumé
We introduce a first order calculus which is a syntactic restriction of Peano arithmetic. We establish that the set of functions which is provable in this calculus is exactly the set of polynomial time functions.