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.

翻译：非良基（或称非良序）证明系统已成为归纳与余归纳推理的自然框架。在此类系统中，可靠性依赖于全局正确性准则，例如进展性条件。确保这些准则在无穷切割消除下得以保持，仍然是非良基证明论中的一个核心技术挑战。本文基于Tait与Girard的可归约候选技术，为非良基$μ\mathsf{MALL}$——一种扩展了不动点的线性逻辑片段——提出了两种切割消除论证。在两种论证中，进展性的保持均直接源于可归约候选的定义性质。特别地，第二种论证基于Leigh与Afshari先前工作中发展的内部闭集拓扑概念。