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 
.
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 
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.