Syntactic cut-elimination for a fragment of the modal mu-calculus (Q714717): Difference between revisions

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.