#матлог #учёба #спецсеминар #не_мехмат #МИАН #ТД

Logic Online Seminar, Monday 16:00 MSK (UTC+3), Room 313 MIAN + Kontur Talk (https://www.mathnet.ru/eng/conf876)

03 March 2025, 13:00 UTC, the Proof Society Seminar

Speaker: Henry Towsner (University of Pennsylvania, https://www.sas.upenn.edu/~htowsner/)

Title: Proofs that Modify Proofs

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

🔗 Seminars "Proof Theory" and "Logic Online Seminar"


➰ ВК