Projects per year
Abstract
We study the computational expressivity of proof systems with fixed point operators, within the ‘proofsasprograms’ 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 firstorder functions: those provably total in Π^{1}_{2}−CA_{0}, a subsystem of secondorder 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 Π^{1}_{2}−CA_{0} (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 Π^{1}_{2}−CA_{0} in order to obtain the tight bounds we are after. Along the way we develop some novel reverse mathematics for the KnasterTarski 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)  10436871 
ISSN (Electronic)  25755528 
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
 CurryHoward
 Fixed points
 Higherorder 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