The main tool for showing lower bounds on proof heights is a variant of an iteration principle studied by Takeuti. This reformulation might be of independent interest, as it allows for polynomial size formulae in the relativised language that require proofs of exponential height.

An arithmetical formulation of the iteration principle yields a strength measure for theories in the language of relativised two-sorted Bounded Arithmetic. This measure provides all the separations Dynamic Ordinal Analysis provides, but extends to theories where the latter fails to produce any separation, due to the overhead of first-order (i.e., sharply-bounded) cut elimination. The new measure can also be used to investigate relativised theories for small complexity classes that are not necessarily based on restricted forms of induction. In particular, it can be used for theories that axiomatise computations, most prominently, deterministic and non-deterministic space computations, and the evaluation of circuits. Before studying relativised versions of these theories it is necessary to define relativised versions of the corresponding complexity classes. This can be done in such a way that the known inclusions are preserved.

Robert Recorde Room

Department of Computer Science