Computational expressivity of (circular) proofs with fixed points

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

• Gianluca Curzi (University of Birmingham)
• Friday 02 June 2023, 14:00-14:50
• LG23, Computer Science // Zoom.

If you have a question about this talk, please contact George Kaye.

Zoom details

• Link: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09
• Meeting ID: 818 7333 5084
• Passcode: 217

Abstract

We study the computational expressivity of proof systems with fixed point operators, within the ‘proofs-as-programs’ paradigm. We start with a calculus muLJ (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, muLJ admits an extension to a ‘circular’ calculus CmuLJ in a standard way.

Our main result is that, perhaps surprisingly, both muLJ and CmuLJ represent the same first-order functions: those provably total in Pi12-CA0, a subsystem of second-order arithmetic beyond the ‘big five’ of reverse mathematics and one of the strongest theories for which we have an ordinal analysis (due to Rathjen). This solves various questions in the literature on the computational strength of (circular) proof systems with fixed points.

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 Pi12-CA0 (due to Möllerfeld). For the upper bound we give a novel totality argument for circular proofs with fixed points. In fact we must formalise this argument itself within Pi12-CA0 in order to obtain the tight bounds we are after, requiring a choice of higher computability model distinct from usual type structures for second-order systems (such as Girard-Reynolds’ F). Along the way we develop some novel reverse mathematics for the Knaster-Tarski fixed point theorem.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, Computer Science // Zoom
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.