Proofs, programs and abstract complexity

Photograph of Arnold Beckmann

Arnold Beckmann


A meanwhile classical theme in mathematical logic is, that proving forall-exists-statements and defining recursive functions are related concepts. For "classical" theories of arithmetic and corresponding classes of sub-recursive functions, such connections can be obtained, for example, by proof theoretic means.

In my talk, I will speak about similar connections between weak theories of arithmetic (called bounded arithmetic [1]) and low level complexity functions (like the polynomial time hierarchy of functions). I will point out how these connections are related to certain abstract measures (called dynamic ordinals [2]) of the provability strength of such theories. In particular, I will mention connections to an enterprise called "Cook's NP versus coNP programme" of proving lower bounds to propositional proof systems.

[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.
Tuesday 20th September 2005, 14:00
Robert Recorde Room
Department of Computer Science