取得进展：非良基领域中的可归约性候选者与切割消去

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