3 March 2025, Proof Society Seminar, Henry Towsner

In this talk, we outline an approach to cut-elimination for full second order arithmetic using a modified form of the Buchholz Omega-rule. The usual Buchholz Omega-rule is a rule branching over ("small") deductions; this method works for systems around the strength of Pi11-comprehension, but breaks down approaching Pi12-comprehension.

We describe an extended sequent calculus in which the cut-elimination functions can themselves be represented by non-well-founded deductions. The Omega-rule can then be reinterpreted as a rule which takes a function as a premise. The extension to Pi12-comprehension then requires us to work with functionals---that is, functions on functions---and iterating through the finite types extends the method to full second order arithmetic. We will also briefly describe how to assign "ordinals" to non-well-founded deductions to extract an ordinal analysis from the cut-elimination algorithm.