Effective cut-elimination for a fragment of modal mu-calculus (Q454366): Difference between revisions
From MaRDI portal
Set OpenAlex properties. |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: Syntactic cut-elimination for common knowledge / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Explaining the Gentzen-Takeuti reduction steps: A second-order system / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A Buchholz rule for modal fixed point logics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Canonical completeness of infinitary \(\mu \) / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A finite model theorem for the propositional \(\mu\)-calculus / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An extension of the omega-rule / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Proof theory. The first step into impredicativity / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Proof theory. 2nd ed / rank | |||
Normal rank |
Latest revision as of 18:24, 5 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Effective cut-elimination for a fragment of modal mu-calculus |
scientific article |
Statements
Effective cut-elimination for a fragment of modal mu-calculus (English)
0 references
1 October 2012
0 references
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, e.g., \textit{J. Bradfield} and \textit{C. Stirling}'s survey in [``Modal mu-calculus'', in: Handbook of modal logic. Amsterdam: Elsevier. 721--756 (2007; Zbl 1114.03001)].
0 references
modal mu-calculus
0 references
cut elimination
0 references