取得进展：在非良基领域中的可约候选者与切消
Making progress: Reducibility Candidates and Cut Elimination in the Ill-founded Realm
AI总结：
本文提出两种基于可约候选者技术的非良基μMALL切消论证，通过定义性质保证进步性，利用拓扑内部闭集概念完成第二个论证。
摘要：
非良基（或非良序）证明系统已逐渐成为归纳和共归纳推理的自然框架。在这些系统中，正确性依赖于全局正确性标准，如进步性条件。确保这些标准在无穷切消下得以保持仍然是非良基证明论中的核心技术挑战。在本文中，我们基于Tait和Girard的可约候选者技术，提出了两个针对非良基μMALL（线性逻辑的一个扩展片段）的切消论证。在两个论证中，进步性的保持直接来自于可约候选者的定义性质。特别是，第二个论证来源于Afshari和Leigh在先前工作中发展出的拓扑内部闭集的概念。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
