Making progress: Reducibility Candidates and Cut Elimination in the Ill-founded Realm
Gianluca Curzi, Graham E. Leigh
TL;DR
Ill-founded proof systems rely on a global progressivity criterion, and maintaining it under infinitary cut elimination is a central challenge. The paper develops two cut-elimination arguments for ill-founded $μ\mathsf{MALL}$ using reducibility candidates: a direct $\mathfrak{N}$-reducibility candidates-based approach tied to cut elimination, and a second approach based on $\mathfrak{E}$-reducibility candidates that uses the topological notion of internally closed sets and external progressivity. The framework does not restrict fixed-point formation beyond positivity and generalizes to other fixed-point logics; it also introduces a multicut-based elimination variant. The results show that progressing proofs are normalisable and that progressivity is preserved along reduction, providing robust, logic-independent methods for infinitary proof theory.
Abstract
Ill-founded (or non-wellfounded) proof systems have emerged as a natural framework for inductive and coinductive reasoning. In such systems, soundness relies on global correctness criteria, such as the progressivity condition. Ensuring that these criteria are preserved under infinitary cut elimination remains a central technical challenge in ill-founded proof theory. In this paper, we present two cut elimination arguments for ill-founded $μ\mathsf{MALL}$ - a fragment of linear logic extended with fixed-points - based on the reducibility candidates technique of Tait and Girard. In both arguments, preservation of progressivity follows directly from the defining properties of the reducibility candidates. In particular, the second argument is based on the topological notion of internally closed set developed in previous work by Leigh and Afshari.