Hilbert's Program aimed to give an axiom system for all of mathematics, together with a proof that this system of axioms was consistent - that is, could not prove a contradiction. After the full version of this program was shown impossible by Gödel's Incompleteness Theorems, some of the key goals were salvaged in the program of ordinal analysis, a "relativized Hilbert's Program". This program continues Hilbert's goal of securing the consistency of theories of mathematics which involve abstract, infinitary objects while using only concrete, largely (though perhaps not entirely) finitistic reasoning.

The original ordinal analysis was Gentzen's analysis of Peano arithmetic using the ordinal epsilon_0. One of the original goals of the field of proof theory, as it coalesced into a distinct subfield of mathematics after Getzen's work, was to extend this result to the theory called second order arithmetic; Hilbert had specifically called for a consistency proof of this theory in the 2nd Hlibert's Problem.

 

In this talk, I will introduce some of the main ideas used in ordinal analysis and explain how they can be extended to give an ordinal analysis of second order arithmetic - that is, an explicit description of the proofs of second order arithmetic which constructively demonstrates that it is consistent.