Part III: Some musings on circular proofs and the metamathematical approach to proof mining and higher-order computability

Add to your list(s) Download to your calendar using vCal

• Anupam Das, University of Birmingham
• Thursday 21 October 2021, 13:00-14:00
• LG23, SoCS and Zoom (see abstract for link).

If you have a question about this talk, please contact Anupam Das.

Many of you will have seen me speak about circular/cyclic proofs before, hopefully with at least some interest. In this lab lunch organised at the last minute, I want to Zoom into the so-called ‘progressing criterion’ underlying non-wellfounded proofs from the viewpoint of constructivity. In particular, over however many sessions it takes (<=3), I would like to communicate the difficulty of constructivising such soundness/termination arguments, in the sense of mining concrete moduli of convergence/continuity, and advocate for the metamathematical approach. I have at least one question for the group: can techniques from proof mining, higher-order computability and/or constructive mathematics help find alternative, more direct treatments of the progressing criterion? Note that I have included several buzzwords in the title to pique your interest.

=== ZOOM DETAILS ===

Topic: Lab Lunch – Anupam Das Time: Oct 21, 2021 12:45 PM London

Join Zoom Meeting https://bham-ac-uk.zoom.us/j/82680896133?pwd=NnlDVG5Kb1daNFk2c3RnUkhGRENrUT09

Meeting ID: 826 8089 6133 Passcode: 738179 One tap mobile +442080806591,,82680896133#,,,,738179# United Kingdom +442080806592,,82680896133#,,,,738179# United Kingdom

Dial by your location +44 208 080 6591 United Kingdom +44 208 080 6592 United Kingdom +44 330 088 5830 United Kingdom +44 131 460 1196 United Kingdom +44 203 481 5237 United Kingdom +44 203 481 5240 United Kingdom +44 203 901 7895 United Kingdom Meeting ID: 826 8089 6133 Passcode: 738179 Find your local number: https://bham-ac-uk.zoom.us/u/kog5rWU78

Join by SIP 82680896133@zoomcrc.com

Join by H.323 162.255.37.11 (US West) 162.255.36.11 (US East) 115.114.131.7 (India Mumbai) 115.114.115.7 (India Hyderabad) 213.19.144.110 (Amsterdam Netherlands) 213.244.140.110 (Germany) 103.122.166.55 (Australia Sydney) 103.122.167.55 (Australia Melbourne) 149.137.40.110 (Singapore) 64.211.144.160 (Brazil) 149.137.68.253 (Mexico) 69.174.57.160 (Canada Toronto) 65.39.152.160 (Canada Vancouver) 207.226.132.110 (Japan Tokyo) 149.137.24.110 (Japan Osaka) Meeting ID: 826 8089 6133 Passcode: 738179

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• LG23, SoCS and Zoom (see abstract for link)
• Lab Lunch

Note that ex-directory lists are not shown.