Part II: 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 14 October 2021, 13:00-14:00
• 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 14/10/2021 Time: Oct 14, 2021 12:45 PM London

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

Meeting ID: 874 5016 5491 Passcode: 203048 One tap mobile +442080806591,,87450165491#,,,,203048# United Kingdom +442080806592,,87450165491#,,,,203048# 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: 874 5016 5491 Passcode: 203048 Find your local number: https://bham-ac-uk.zoom.us/u/kTxCB4rXD

Join by SIP 87450165491@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: 874 5016 5491 Passcode: 203048

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• Lab Lunch
• Zoom (see abstract for link)

Note that ex-directory lists are not shown.