Abstract:  Bounded arithmetic theories are first order theories
of arithmetic which are strongly connected to low level
complexity.  E.g., it is possible to capture the polynomial time
computable functions as a class of definable functions in some
bounded arithmetic theory (cf. [1]).  The dynamic ordinals of
theories of bounded arithmetic have been introduced to
characterize the provability strength of the underlying theory
(cf. [2]), in analogy to prooftheoretic ordinals for "usual"
theories of arithmetic (e.g. Peano Arithmetic).

In this talk we will discuss how dynamic ordinals of bounded
arithmetic theories also describe the computational content of
the underlying theories.  To this end we will illustrate how
proofs in bounded arithmetic theories can directly be viewed as
programs, and why dynamic ordinals of bounded arithmetic theories
immediately give upper bounds on the complexity of such
functions.

[1]  S. Buss: Bounded Arithmetic.  Studies in Proof Theory.
     Lecture Notes, 3. Bibliopolis, Naples, 1986.

[2]  A. Beckmann: Dynamic ordinal analysis.  Arch. Math. Logic
     2003, 42: 303-334.