Logic Colloquium 2008

Michael Rathjen

Infinitary proof theory and its uses

rathjen@maths.leeds.ac.uk Department of Pure Mathematics, University of Leeds, Leeds, United Kingdom

Proof theory was the technical area of logic instituted by Hilbert in the early 20th century in order to carry out his programme: to lay to rest all worries about the foundations of mathematics once and for all by securing mathematics via an absolute proof of consistency. Strong restrictions were placed on the methods to be applied in consistency proofs of axiom systems for mathematics: namely, these methods were to be completely finitistic in character. Hilberts Programme is a reductive enterprise with the aim of showing that whenever a real proposition can be proved by ideal means, it can also be proved by real, finitistic means. However, Hilbert's so-called formalism was not intended to eliminate nonconstructive existence proofs in the practice of mathematics, but to vindicate them.

In the 1920s, Ackermann and von Neumann, in pursuit of Hilberts Programme, were working on consistency proofs for arithmetical systems, but already with the infusion of an infinitary concept. Ackermann's 1924 dissertation gives a consistency proof for a second-order version of primitive recursive arithmetic which explicitly uses a finitistic version of transfinite induction up to the ordinal \omega^{{\omega^{\omega}}}. The employment of transfinite induction on ordinals in consistency proofs came explicitly to the fore in Gentzen's 1936 consistency proof for Peano arithmetic. His proof became the paradigm for an ordinal analysis of a theory by assigning a proof-theoretic ordinal to a theory which calibrates its logical power.

Beginning in the 1950s, proof theory began to employ infinitary methods more frankly, first with the use of infinitary rules of inference (such as the omega rule) and then with the use of infinitely long formulas. At first, these rules, formulas and the resulting derivations were all countable, but eventually proof theory moved on to make use of prima facie uncountably long rules of inference and/or formulas, thence uncountably long derivations. These countably and uncountably long derivations have been applied to treat various formal systems for parts of analysis and set theory, by translating their finite derivations into corresponding infinite ones of a more purely logical character. By then applying the process of cut-elimination or other forms of normalization, the latter are transformed into detour-free derivations whose associated ordinals give a measure of complexity to the systems thus treated. For example, they can be used to classify their provably recursive functions. Cut-free derivations are easily shown not to end in a contradiction, so one also concludes consistency from such analyses. The more that such infinitary methods were employed, the closer did proof theory come to ongoing developments in recursion theory, particularly as generalized to admissible sets; in both one makes use of analogues of regular cardinals, as well as "large" cardinals (inaccessible, Mahlo, etc.).

The lectures will trace the remarkable transformation of proof theory up to developments in recent years. Notwithstanding that it employs infinitary derivations, proof theory provides finitistic reductions between theories, especially \Pi^{0}_{2} conservation results. Moreover, the lectures will explore its applications in logic, combinatorics, computer science and constructivism. If time permits, we will also take up the question of where the boundaries of current ordinal-theoretic proof theory lie and what are the main obstacles to be overcome.