$\Pi^0_2$ Induction and Exponential Time

Stan Wainer


This is an extension of work with G. Ostrin which I've spoken about before. If the induction variables are separated from the quantified variables in arithmetic, then the provably recursive functions become much more feasible. The $\Sigma_1$ inductive fragment corresponds to polynomial time (but of course in "unary" notation) and the next level of induction corresponds to exponential time. The whole theory only proves totality of elementary functions. Exponential time is particularly interesting because it includes good, informative examples (from the proof theoretic viewpoint). Factorial, suggested by H. Jervell, is a specially good one, and I'll use it to illustrate how our theory (closely related to earlier work of Leivant) ticks.
Tuesday 27th November 2001, 14:00
Robert Recorde Room
Department of Computer Science