Syntactic cut-elimination for a fragment of the modal mu-calculus
type: Item
instance of: scholarly article
title: Syntactic cut-elimination for a fragment of the modal mu-calculus
zbMATH Open document ID: 1259.03031
author: Kai Brünnler
author: Thomas Studer
published in: Annals of Pure and Applied Logic
publication date: 2012-10-11T00:00:00Z
review text: 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.
reviewed by: G. E. Mints
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 6092966
zbMATH Keywords: cut elimination
zbMATH Keywords: infinitary sequent system
zbMATH Keywords: nested sequents
zbMATH Keywords: mu-calculus
MaRDI profile type: Publication
full work available at URL: j.apal.2012.04.006
OpenAlex ID: W2020453924
cites work: Least and Greatest Fixed Points in Linear Logic
cites work: The variable hierarchy of the \(\mu\)-calculus is strict
cites work: Modal logics and mu-calculi: An introduction
cites work: Q3509048
cites work: Syntactic cut-elimination for common knowledge
cites work: Syntactic Cut-elimination for Common Knowledge
cites work: Continuous Fragment of the mu-Calculus
cites work: A contraction-free and cut-free sequent calculus for propositional dynamic logic
cites work: Canonical completeness of infinitary \(\mu \)
cites work: Cut-free sequent calculi for some tense logics
cites work: Results on the propositional \(\mu\)-calculus
cites work: A finite model theorem for the propositional \(\mu\)-calculus
cites work: Q5854738
cites work: Games for the \(\mu\)-calculus
cites work: Q3358711
cites work: The Method of Tree-Hypersequents for Modal Propositional Logic
cites work: Proof theory. An introduction
cites work: Q4215633
cites work: Q5538910
cites work: Q4143279
cites work: Cut elimination for a logic with induction and co-induction
cites work: Q4499084
cites work: Q4866992
cites work: Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
DOI: 10.1016/J.APAL.2012.04.006
description: scientific article; zbMATH DE number 6092966