NOL Seminar with Anupam Das
published: 2021-09-16
event date:
2021-09-27
The Nordic Online Logic 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. 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.
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