Effective cut-elimination for a fragment of modal mu-calculus
type: Item
instance of: scholarly article
title: Effective cut-elimination for a fragment of modal mu-calculus
zbMATH Open document ID: 1254.03110
author: G. E. Mints
published in: Studia Logica
publication date: 2012-10-01T00:00:00Z
review text: The mu-calculus is an extension of temporal logic for transition systems with added fixpoint operators which appeared particularly useful for specification and verification of temporal properties. An infinitary system adequate for the whole mu-calculus was proved cut-free in a non-constructive way by \textit{G. Jäger}, \textit{M. Kretz} and \textit{T. Studer} in [J. Log. Algebr. Program. 76, No. 2, 270--292 (2008; Zbl 1156.68013)]. A constructive proof of cut elimination for the fragment of mu-calculus, called \(\mathrm{M}_1\), with non-iterated fixpoints and omega-rule was offered by \textit{W. Buchholz} in [Arch. Math. Logic 40, No. 4, 255--272 (2001; Zbl 1007.03051)], but only for positive formulas. In this paper, G. Mints provides another constructive proof of cut elimination for \(\mathrm{M}_1\) which improves Buchholz's result in two ways. First, it is not restricted to proofs of positive formulas. Second, the omega-rule is only an intermediate tool for obtaining a cut-free calculus. In order to remove cut from \(\mathrm{M}_1\), the system \(\mathrm{M}^\prime\) is introduced, which is cut-free but uses instead of the (finitary) rule (ind) of \(\mathrm{M}_1\) some infinitary rule. Next, the auxiliary system \(\mathrm{M}^\Omega \) is introduced which adds to \(\mathrm{M}^\prime\) two omega-rules and a form of cut. It is shown that every derivation in \(\mathrm{M}_1\) is transformed into a derivation in \(\mathrm{M}^\Omega \), and every derivation in \(\mathrm{M}^\Omega \) is transformed into a derivation in \(\mathrm{M}^\prime\). Although this result by itself does not imply cut admissibility for \(\mathrm{M}_1\), there are simple sufficient conditions satisfied by Mints's proof which recovers provability in the finitary system from provability in the infinitary one. As a result, cut admissibility for \(\mathrm{M}_1\) follows. The text is rather dense and technical, hence the reader not acquainted with the mu-calculus should first consult some introductory paper…
reviewed by: Andrzej Indrzejczak
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 6088846
zbMATH Keywords: modal mu-calculus
zbMATH Keywords: cut elimination
MaRDI profile type: Publication
full work available at URL: s11225-012-9378-y
OpenAlex ID: W2032188971
cites work: Syntactic cut-elimination for common knowledge
cites work: Explaining the Gentzen-Takeuti reduction steps: A second-order system
cites work: A Buchholz rule for modal fixed point logics
cites work: Canonical completeness of infinitary \(\mu \)
cites work: A finite model theorem for the propositional \(\mu\)-calculus
cites work: An extension of the omega-rule
cites work: Proof theory. The first step into impredicativity
cites work: Proof theory. 2nd ed
DOI: 10.1007/S11225-012-9378-Y
Recommended article: A Buchholz rule for modal fixed point logics
Recommended article: A focus system for the alternation-free \(\mu \)-calculus
Recommended article: On the proof theory of the modal mu-calculus
Recommended article: Q4417913
Recommended article: On the universal and existential fragments of the \(\mu\)-calculus
Recommended article: On model checking for the \(\mu\)-calculus and its fragments
Recommended article: Q5854738
Recommended article: Q5144634
Recommended article: Logic for Programming, Artificial Intelligence, and Reasoning
Recommended article: Q4484479
description: scientific article; zbMATH DE number 6088846