Loading [MathJax]/jax/output/SVG/config.js
Seminars
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
Calendar
Search
Add a seminar

RSS
Forthcoming seminars




Seminars "Proof Theory" and "Logic Online Seminar"
March 3, 2025 16:00, Moscow, Steklov Mathematical Institute (8 Gubkina), room 313 + online
 


Proofs that Modify Proofs

H. Towsner

University of Pennsylvania

Number of views:
This page:52

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 $\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.

Language: English
 
  Contact us:
 Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2025