DIMACS TR: 96-49
Ranking Arithmetic Proofs by Implicit Ramification
Author: Stephen J. Bellantoni
ABSTRACT
Proofs in an arithmetic system are ranked according to a ramification
hierarchy based on occurrences of induction. It is shown that this
ranking of proofs corresponds exactly to a natural ranking of the
primitive recursive functions based on occurrences of recursion.
A function is provably convergent using a rank $r$ proof, if and
only if it is a rank $r$ function. The result is of interest to complexity
theorists, since rank one corresponds to polynomial time. Remarkably, this
characterization of polynomial-time provability admits induction over
formulas having arbitrary quantifier complexity.
Paper Available at:
ftp://dimacs.rutgers.edu/pub/dimacs/TechnicalReports/TechReports/1996/96-49.ps.gz
DIMACS Home Page