Projects per year
Abstract
We study the computational expressivity of proof systems with fixed point operators, within the ‘proofs-as-programs’ paradigm. We start with a calculus μLJ (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, μLJ admits a standard extension to a ‘circular’ calculus CμLJ.
Our main result is that, perhaps surprisingly, both μLJ and CμLJ represent the same first-order functions: those provably total in Π12−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 Π12−CA0 (due to Möllerfeld). For the upper bound we construct a novel computability model in order to give a totality argument for circular proofs with fixed points. In fact we formalise this argument itself within Π12−CA0 in order to obtain the tight bounds we are after. Along the way we develop some novel reverse mathematics for the Knaster-Tarski fixed point theorem.
Original language | English |
---|---|
Title of host publication | 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
Publisher | Institute of Electrical and Electronics Engineers (IEEE) |
Number of pages | 13 |
ISBN (Electronic) | 9798350335873 |
ISBN (Print) | 9798350335880 (PoD) |
DOIs | |
Publication status | Published - 14 Jul 2023 |
Event | 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023 - Boston, United States Duration: 26 Jun 2023 → 29 Jun 2023 |
Publication series
Name | Proceedings - Symposium on Logic in Computer Science |
---|---|
Publisher | Institute of Electrical and Electronics Engineers (IEEE) |
ISSN (Print) | 1043-6871 |
ISSN (Electronic) | 2575-5528 |
Conference
Conference | 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023 |
---|---|
Country/Territory | United States |
City | Boston |
Period | 26/06/23 → 29/06/23 |
Bibliographical note
Funding Information:The authors would like to thank Pierre Clairambault and Colin Riba for several illuminating conversations about fixed point types. and This work was supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1.
Publisher Copyright:
© 2023 IEEE.
Keywords
- Circular proofs
- Curry-Howard
- Fixed points
- Higher-order computability
- Proof theory
- Realisability
- Reverse mathematics
ASJC Scopus subject areas
- Software
- General Mathematics
Fingerprint
Dive into the research topics of 'Computational expressivity of (circular) proofs with fixed points'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Structure vs. Invariants in Proofs (StrIP)
Das, A. (Principal Investigator)
1/05/20 → 31/07/24
Project: Research Councils