# Computational expressivity of (circular) proofs with fixed points

## TL;DR

This paper investigates the computational power of proof systems with fixed points, showing they can represent the same complex functions as a strong subsystem of second-order arithmetic, and develops new models and reverse mathematics results.

## Contribution

It establishes the equivalence in computational expressivity between muLJ and CmuLJ proof systems and $ ext{Pi}^1_2$-$ ext{CA}_0$, and introduces novel models and reverse mathematics techniques.

## Key findings

- Both muLJ and CmuLJ represent the same class of provably total functions.
- The proof systems capture functions provably total in $ ext{Pi}^1_2$-$ ext{CA}_0$.
- New reverse mathematics results for the Knaster-Tarski fixed point theorem.

## 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 a standard extension to a 'circular' calculus CmuLJ. Our main result is that, perhaps surprisingly, both muLJ and CmuLJ represent the same first-order functions: those provably total in $\Pi^1_2$-$\mathsf{CA}_0$, 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 $\Pi^1_2$-$\mathsf{CA}_0$ (due to M\"ollerfeld). 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 $\Pi^1_2$-$\mathsf{CA}_0$ 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.