Nordic Online Logic Seminar: talk by Anupam Das on 27 September 2021

[Graham Leigh]

The Nordic Online Logic Seminar (NOL Seminar) is organised monthly over Zoom, with expository talks on topics of interest for the broader logic community. The seminar is open for professional or aspiring logicians and logic aficionados worldwide.
 
See the announcement for the next talk below. If you wish to receive the Zoom ID and password for it, as well as further announcements, please subscribe here: https://listserv.gu.se/sympa/subscribe/nordiclogic .
 
Val Goranko and Graham Leigh
NOL seminar organisers

------------------------------------
Nordic Online Logic Seminar
Next talk: Monday, September 27, 16.00-17.30 CEST (UTC+2), on Zoom (details will be provided to the subscribers)

Title: On the proof theoretic strength of cyclic reasoning
Speaker: Anupam Das, School of Computer Science, University of Birmingham

Abstract:
Cyclic (or circular) proofs are now a common technique for demonstrating metalogical properties of systems incorporating (co)induction, including modal logics, predicate logics, type systems and algebras. Inspired by automaton theory, cyclic proofs encode a form of self-dependency of which induction/recursion comprise special cases. An overarching question of the area, the so-called 'Brotherston-Simpson conjecture', asks to what extent the converse holds.
 
In this talk I will discuss a line of work that attempts to understand the expressivity of circular reasoning via forms of proof theoretic strength. Namely, I address predicate logic in the guise of first-order arithmetic, and type systems in the guise of higher-order primitive recursion, and establish a recurring theme: circular reasoning buys precisely one level of 'abstraction' over inductive reasoning.
 
This talk will be based on the following works:
https://arxiv.org/abs/1807.10248
https://arxiv.org/abs/2012.14421