We study the computational expressivity of proof systems with fixed point operators, within the `proofs-as-programs' paradigm. We start with a calculus $\mu\mathsf{LJ}$ (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, $\mu\mathsf{LJ}$ admits a standard extension to a `circular' calculus $\mathsf{C}\mu\mathsf{LJ}$. Our main result is that, perhaps surprisingly, both $\mu\mathsf{LJ}$ and $\mathsf{C}\mu\mathsf{LJ}$ 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.

翻译：在“证明即程序”范式下，我们研究带不动点算子的证明系统的计算表达力。我们从$\mu\mathsf{LJ}$微积分（归功于Clairambault）出发，该微积分通过最小和最大正不动点扩展了直觉主义逻辑。基于矢列演算的$\mu\mathsf{LJ}$可标准扩展为“循环”微积分$\mathsf{C}\mu\mathsf{LJ}$。我们的主要结果是，或许令人惊讶的是，$\mu\mathsf{LJ}$与$\mathsf{C}\mu\mathsf{LJ}$表示相同的一阶函数：这些函数是$\Pi^1_2$-$\mathsf{CA}_0$中可证明全的。$\Pi^1_2$-$\mathsf{CA}_0$是二阶算术的一个子系统，超越了逆数学的“五大理论”，且是我们拥有序数分析的最强理论之一（归功于Rathjen）。这解答了文献中关于带不动点的（循环）证明系统计算强度的若干问题。下界方面，我们通过不动点算术扩展（已被证明在算术上等价于$\Pi^1_2$-$\mathsf{CA}_0$，归功于M\"ollerfeld）给出可实现性解释。上界方面，我们构造了一个新颖的可计算性模型，以对带不动点的循环证明进行全体性论证。实际上，我们自身在$\Pi^1_2$-$\mathsf{CA}_0$内形式化了该论证，从而获得所需的紧界。在此过程中，我们为Knaster-Tarski不动点定理发展了一些新颖的逆数学结果。