Cyclic cut elimination for the stratified fragment of the modal μ-calculus
Armand Feuilleaubois
Authors: Armand Feuilleaubois and Thomas Studer
Kloibhofer and Afshari presented in [1] a new cut elimination procedure for annotated cyclic proofs of a temporal modal logic using only the eventually operator, \(F\). This method has the advantage of preserving the regularity of the proof throughout the cut elimination process. We present a cut elimination procedure for the stratified fragment of the modal \(\mu\)-calculus, based on the method of Kloibhofer and Afshari in [1]. The stratified fragment of the modal \(\mu\)-calculus, as defined by Jäger, Kretz, and Studer in [2], is the fragment such that formulas \(\mu X.\mathcal{A}[X]\), \(\nu X.\mathcal{A}[X]\), with \(\mathcal{A}[X]\) positive in the variable \(X\), may only contain subformulas \(\mu Y.\mathcal{B}[Y]\), \(\nu Y.\mathcal{B}[Y]\) where \(X\) does not appear as a free variable. Thus, the meaning of an inner nested fixed point will not depend on the outer fixed point within which it is nested. This fragment itself contains as fragments CTL, PDL, and the logic of common knowledge. Thus, we also obtain cut elimination for these fragments.
Bibliography
- Afshari, Bahareh, and Kloibhofer, Johannes,Cut elimination for Cyclic Proofs: A case study in temporal logic,Proceedings of the 12th International Workshop on Fixed Points in Computer Science(Naples),EPTCS Proceedings,2024.
- Jaeger, Gerhard, and Kretz, Mathis, and Studer, Thomas,Cut–Free Axiomatizations for Stratified Modal Fixed Point Logic,Proceedings of Methods for Modalities 4(H. Schlingloff, editor),2005,pp. 125–143.