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 derived from the topological notion of internally closed set developed in previous work by Afshari and Leigh.

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