2026/07/18 by Jun Suzuki, Charles Grellois, Katsuhiko Sano
Computer Science · #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Formal Methods in Verification
paper · pdf · doi:10.4204/eptcs.449.14
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.