Computational expressivity of (circular) proofs with fixed points

TL;DR

The paper characterises the computational expressivity of fixed-point proof systems by showing that μLJ and its circular version CμLJ represent exactly the functions provably total in $Π^1_2$-$CA_0$. The authors develop a dual approach: a lower bound via a realisability interpretation from μPA/μHA, and an upper bound via a novel higher-order computability model interpreted within $Π^1_2$-$CA_0$, together with a reduction to a negative fragment and a reverse-mathematics analysis of Knaster–Tarski. A key technical feature is a detailed treatment of circular derivations (codderivations), their cut-reductions, and a totality criterion based on progressing threads and ordinal approximants, extended through a transfinite-type system. The results connect circular fixed-point proof systems to strong subsystems of second-order arithmetic, comparable to classical correspondences between PA and T, and demonstrate the tightness of the bounds via arithmetised totality arguments. The work also opens avenues for further exploration of systems with only strictly positive fixed points and the higher-order reverse mathematics of fixed-point theorems.

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 $Π^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 $Π^1_2$-$\mathsf{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$-$\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.

Figures (22)

• Figure 1: Summary of the main 'grand tour' of this work. All arrows indicate inclusions of representable functions.
• Figure 2: Sequent calculus rules for $\mathsf{LJ}$.
• Figure 3: Some unfolding rules for $\mu$ and $\nu$.
• Figure 4: '(Co)iteration' rules for $\mu$ and $\nu$.
• Figure 5: Cut-reduction rules for $\mu$ and $\nu$ in $\mu\mathsf{LJ}$.

Theorems & Definitions (133)

• Definition 2: Types and polarity
• Remark 3: Positivity vs strict positivity
• Definition 4: System $\mu\mathsf{LJ}$
• Remark 5: General identity and substitutions
• Remark 6: $\mu\mathsf{LJ}$ as a fragment of second-order logic
• Remark 7: Why sequent calculus?
• Remark 8: Variations of the fixed point rules
• Definition 1: Functors
• Example 9: Post-fixed point
• Definition 10: Cut-reduction for fixed points