This paper presents a proof-theoretic analysis of the modal \(\mu \) -calculus. More precisely, we prove a syntactic cut-elimination for the non-wellfounded modal \(\mu \) -calculus, using methods from linear logic. and its exponential modalities. To achieve this, we introduce a new system, \(\mu \textsf {LL}_{\Box }^{\infty }\) , which is a linear version of the modal \(\mu \) -calculus, intertwining the modalities from the modal \(\mu \) -calculus with the exponential modalities from linear logic. Our strategy for proving cut-elimination involves (i) proving cut-elimination for \(\mu \textsf {LL}_{\Box }^{\infty }\) and (ii) translating proofs of the modal mu-calculus into this new system via a “linear translation”, allowing us to extract the cut-elimination result.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

On the cut-elimination of the modal \(\mu \) -calculus: Linear Logic to the rescue

  • Esaïe Bauer,
  • Alexis Saurin

摘要

This paper presents a proof-theoretic analysis of the modal \(\mu \) -calculus. More precisely, we prove a syntactic cut-elimination for the non-wellfounded modal \(\mu \) -calculus, using methods from linear logic. and its exponential modalities. To achieve this, we introduce a new system, \(\mu \textsf {LL}_{\Box }^{\infty }\) , which is a linear version of the modal \(\mu \) -calculus, intertwining the modalities from the modal \(\mu \) -calculus with the exponential modalities from linear logic. Our strategy for proving cut-elimination involves (i) proving cut-elimination for \(\mu \textsf {LL}_{\Box }^{\infty }\) and (ii) translating proofs of the modal mu-calculus into this new system via a “linear translation”, allowing us to extract the cut-elimination result.