Syntactic cut-elimination for a fragment of the modal mu-calculus (Q714717): Difference between revisions
From MaRDI portal
Latest revision as of 18:53, 5 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Syntactic cut-elimination for a fragment of the modal mu-calculus |
scientific article |
Statements
Syntactic cut-elimination for a fragment of the modal mu-calculus (English)
0 references
11 October 2012
0 references
Ordinary finite axiomatization of the propositional modal \(\mu\)-calculus contains an induction rule to guarantee that \(\mu XA\) denotes a least fixed point. For an infinitary reformulation \(G_\mu\) where induction is replaced by an infinitary rule (saying that the greatest fixpoint \(\nu XB\) is a limit of finite approximations \(\nu^kXB\)) cut elimination was proved semantically by \textit{G. Jäger} et al. [J. Log. Algebr. Program. 76, No. 2, 270--292 (2008; Zbl 1156.68013)]. In the present paper a syntactic cut-elimination proof of a traditional kind is presented for a ``deep inference'' reformulation \(D_\mu\) of the ``continuos'' fragment consisting of formulas where a \(\lozenge\) does not occur between \(\nu\) and its bound variable and \(\square\) does not occur between \(\mu\) and its bound variable. This fragment is sufficient for embedding of such systems as PDL and the logic of common knowledge. \(D_\mu\) is obtained from \(G_\mu\) by replacing the closure rule corresponding to an implication \(A(\mu XA)\to\mu XA\) by a rule corresponding to \(\mu^kXA\to\mu XA\) and permitting application of all inference rules inside any (iterated) combination of \(\vee\) and \(\square\). This roughly corresponds to rules for a semantic tableau formulation of S4. Since all cut ranks are below \(\omega^2\), standard bounds for elementary cut-elimination steps yield an estimate \(\phi_2\alpha\) for a cut-free form of a derivation of size \(\alpha\). The system \(D_\mu\) is sound for finite approximations to a fixpoint and hence is not complete since a valid formula \(\square(\mu X\square X)\to\mu \square X\) is not valid for finite approximations. However, \(D_\mu\) and \(G_\mu\) prove the same continuous formulas.
0 references
cut elimination
0 references
infinitary sequent system
0 references
nested sequents
0 references
mu-calculus
0 references