
SEMINARS 
Seminars
"Proof Theory" and "Logic Online Seminar"



Computational expressivity of (circular) proofs with fixed points A. Das^{} ^{} University of Birmingham 

Abstract: We study the computational expressivity of proof systems with fixed point operators, within the ‘proofsasprograms’ paradigm. We start with a calculus μ𝖫𝖩 (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, μ𝖫𝖩 admits a standard extension to a ‘circular’ calculus 𝖢μ𝖫𝖩. Our main result is that, perhaps surprisingly, both μ𝖫𝖩 and 𝖢μ𝖫𝖩 represent the same firstorder functions: those provably total in For the lower bound we give a realisability interpretation from an extension of Peano Arithmetic by fixed points that has been shown to be arithmetically equivalent to Along the way we develop some novel reverse mathematics for the KnasterTarski fixed point theorem. Based on joint work with Gianluca Curzi, https://arxiv.org/abs/2302.14825 Language: English 