Proofs that Modify Proofs

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 $\Pi^1_1$-comprehension, but breaks down approaching $\Pi^1_2$-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 $\Pi^1_2$-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.