BEGIN:VCALENDAR
VERSION:2.0
PRODID:ILLC Website
X-WR-TIMEZONE:Europe/Amsterdam
BEGIN:VTIMEZONE
TZID:Europe/Amsterdam
X-LIC-LOCATION:Europe/Amsterdam
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:/NewsandEvents/Archives/2025/newsitem/15484/3-
 March-2025-Proof-Society-Seminar-Henry-Towsner
DTSTAMP:20250221T150858
SUMMARY:Proof Society Seminar, Henry Towsner
ATTENDEE;ROLE=Speaker:Henry Towsner (University of
  Pennsylvania)
DTSTART;TZID=Europe/Amsterdam:20250303T140000
LOCATION:online
DESCRIPTION:In this talk, we outline an approach t
 o 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 re
 presented by non-well-founded deductions. The Omeg
 a-rule can then be reinterpreted as a rule which t
 akes a function as a premise. The extension to Pi1
 2-comprehension then requires us to work with func
 tionals---that is, functions on functions---and it
 erating through the finite types extends the metho
 d to full second order arithmetic. We will also br
 iefly describe how to assign "ordinals" to non-wel
 l-founded deductions to extract an ordinal analysi
 s from the cut-elimination algorithm.
X-ALT-DESC;FMTTYPE=text/html:\n  <p>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 (&quot;small&quot;) 
 deductions; this method works for systems around t
 he strength of Pi11-comprehension, but breaks down
  approaching Pi12-comprehension.</p>\n  <p>We desc
 ribe an extended sequent calculus in which the cut
 -elimination functions can themselves be represent
 ed 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-compr
 ehension then requires us to work with functionals
 ---that is, functions on functions---and iterating
  through the finite types extends the method to fu
 ll second order arithmetic. We will also briefly d
 escribe how to assign &quot;ordinals&quot; to non-
 well-founded deductions to extract an ordinal anal
 ysis from the cut-elimination algorithm.</p>\n
URL:https://www.proofsociety.org/activities-and-re
 sources/proof-society-seminar/
CONTACT:Marianna Girlando at m.girlando at uva.nl
END:VEVENT
END:VCALENDAR