Ernest Schimmerling

Mid-Atlantic Mathematical Logic Seminar

Jeremy Avigad (CMU)

Update procedures and the 1-consistency of arithmetic

In 1940, Ackermann showed how to use Hilbert's epsilon substitution method to reobtain Gentzen's ordinal analysis of first-order arithmetic. In this talk, I will present an intuitively appealing approach that emphasizes the computational content of the problem. In particular, I will show that the 1-consistency of arithmetic is equivalent to the assertion that certain systems of fixed-point equations are solvable. General continuity considerations show that such systems always have solutions; with some care, the solutions can be obtained by recursion below epsilon_0.