AI 中文总结
研究具有最小和最大不动点的直觉主义命题乘加线性逻辑（$\mu$IMALL）的消去切割定理，通过定义相位语义，证明其可靠性与无切割完全性，改进前人论证方法来达成该定理的证明。
AI 中文摘要
本文借助相位语义学建立了具有最小和最大不动点的直觉主义命题乘加线性逻辑（$\mu$IMALL）的消去切割定理。Baelde和Miller（2007年）引入了具有最小和最大不动点的经典一阶乘加线性逻辑系统，其直觉主义片段在Baelde（2012年）中被讨论，但该片段的消去切割定理尚未得到证明。我们引入了该系统的一个命题片段$\mu$IMALL并建立了消去切割定理。为证明该定理，我们为$\mu$IMALL定义了相位语义，并证明了两点：（1）可靠性：若一个公式在$\mu$IMALL中可证，则它在所有相位模型中为真；（2）无切割完全性：若一个公式在所有相位模型中为真，则它在无切割的$\mu$IMALL中可证。我们改进并应用Okada（1999年、2002年）以及De等人（2022年）的论证来证明$\mu$IMALL的消去切割定理。
英文摘要
This paper establishes the cut-elimination theorem for intuitionistic propositional multiplicative-additive linear logic with the least and greatest fixpoints ($μ$IMALL) by means of its phase semantics. A classical first-order multiplicative-additive linear logic system with the least and greatest fixpoints was introduced by Baelde and Miller (2007). Its intuitionistic fragment was discussed in Baelde (2012), but the cut-elimination theorem for this fragment has not yet been proved. We introduce a propositional fragment of this system, $μ$IMALL, and establish the cut-elimination theorem. To prove the theorem, we define phase semantics for $μ$IMALL and show the following two statements: (1) Soundness: if a formula is provable in $μ$IMALL, then it is true in all phase models, and (2) Cut-free Completeness: if a formula is true in all phase models, then it is provable in $μ$IMALL without Cut. Okada (1999, 2002) employed a phase semantic method to prove the cut-elimination theorems for classical and intuitionistic linear logic systems. De et al. (2022) applied this method to a propositional fragment of classical propositional multiplicative-additive linear logic with the least and greatest fixpoints. We refine and apply their arguments to prove the cut-elimination theorem for $μ$IMALL.
CommentsIn Proceedings LSFA 2026, arXiv:2607.15904
Journal refEPTCS 449, 2026, pp. 221-238
