一句话：证明带最小/最大正不动点的 muLJ 与其循环扩展 CmuLJ 具有相同计算表达力，均对应 Π^1_2-CA_0 中可证全的函数。
本文在“证明即程序”范式下考察带不动点算子的证明系统的计算表达力。作者以 Clairambault 的 muLJ（用最小/最大正不动点扩展直觉主义逻辑的相继式演算）及其循环扩展 CmuLJ 为对象。核心结果出人意料：二者表示相同的首阶函数类，即 Π^1_2-CA_0 中可证全的函数；该二阶算术子系统强于逆向数学“五大”，且是可做序数分析的最强理论之一。下界用带不动点 Peano 算术扩展的 realizability 解释获得；上界构造新可计算性模型证明循环证明的全性，并在 Π^1_2-CA_0 内形式化该论证。途中还发展了 Knaster-Tarski 不动点定理的逆向数学。
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.
@article{paperbot3352,
title = {Computational expressivity of (circular) proofs with fixed points},
author = {Gianluca Curzi and Anupam Das},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:18)2025}
}