DIMACS TR: 96-49

Ranking Arithmetic Proofs by Implicit Ramification

Author: Stephen J. Bellantoni


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