Computational expressivity of (circular) proofs with fixed points

Gianluca Curzi*, Anupam Das

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publication2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages13
ISBN (Electronic)9798350335873
ISBN (Print)9798350335880 (PoD)
DOIs
Publication statusPublished - 14 Jul 2023
Event38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023 - Boston, United States
Duration: 26 Jun 202329 Jun 2023

Publication series

NameProceedings - Symposium on Logic in Computer Science
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
ISSN (Print)1043-6871
ISSN (Electronic)2575-5528

Conference

Conference38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023
Country/TerritoryUnited States
CityBoston
Period26/06/2329/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.

Cite this