A Buchholz rule for modal fixed point logics
type: Item
instance of: scholarly article
title: A Buchholz rule for modal fixed point logics
zbMATH Open document ID: 1278.03044
author: Gerhard Jäger
author: Thomas Studer
published in: Logica Universalis
publication date: 2013-03-19T00:00:00Z
review text: In [Lect. Notes Math. 897, 189--233 (1981; Zbl 0489.03022)], \textit{W. Buchholz} introduced \(\Omega_{\mu+1}\)-rules for proof-theoretic analysis of arithmetical inductive definitions. Since then, his approach was successfully applied in proof theory, for example as a basis for `ordinal-free' consistency proofs. Buchholz's method is applied in this paper to deal with modal fixed-point logics like temporal logics LTL, CTL or program logics like PDL. All these systems are subsumed by the \(\mu \)-calculus, which is an extension of temporal logic for transition systems with added fixed-point operators. The \(\mu \)-calculus 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} et al. in [J. Log. Algebr. Program. 76, No. 2, 270--292 (2008; Zbl 1156.68013)]. The present study is concerned with the fragment of \(\mu \)-calculus, called \(\mathrm{M}_1\), with non-iterated fixed points of positive formulas. After the presentation of the syntax and semantics of \(\mathrm{M}_1\), the infinitary sequent (Tait-style) system \(\mathrm{M}^\infty_1\) is introduced based on the \(\Omega \)-rule. In Section 4 it is shown how to derive the usual induction rule in \(\mathrm{M}^\infty_1\), hence the embedding of \(\mathrm{M}_1\) in \(\mathrm{M}^\infty_1\) follows. The completeness of cut-free \(\mathrm{M}^\infty_1\) is shown in Section 5 by a semantical canonical counter-model construction. To prove soundness of \(\mathrm{M}^\infty_1\), the authors use the finite model property of \(\mathrm{M}_1\), proved by \textit{D. Kozen} in [Stud. Log. 47, No. 3, 233--241 (1989; Zbl 0667.03019)]. Finally, syntactical cut-elimination and collapsing results are shown which are analogous to Buchholz's results.
reviewed by: Andrzej Indrzejczak
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 6146088
zbMATH Keywords: proof theory
zbMATH Keywords: sequent calculus
zbMATH Keywords: modal fixed-point logics
zbMATH Keywords: omega rule
zbMATH Keywords: modal \({\mu}\)-calculus
zbMATH Keywords: Buchholz rule
MaRDI profile type: Publication
full work available at URL: s11787-010-0022-1
OpenAlex ID: W2066142388
cites work: Induction and inductive definitions in fragments of second order arithmetic
cites work: Q4075450
cites work: Explaining the Gentzen-Takeuti reduction steps: A second-order system
cites work: Q4040375
cites work: Proof-theoretical analysis: Weak systems of functions and classes
cites work: Canonical completeness of infinitary \(\mu \)
cites work: A finite model theorem for the propositional \(\mu\)-calculus
cites work: Elementary induction on abstract structures
cites work: Completeness for Flat Modal Fixpoint Logics
cites work: Ordinal analysis by transformations
cites work: Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
DOI: 10.1007/S11787-010-0022-1
Recommended article: Effective cut-elimination for a fragment of modal mu-calculus
Recommended article: On the proof theory of the modal mu-calculus
Recommended article: Canonical completeness of infinitary \(\mu \)
Recommended article: A focus system for the alternation-free \(\mu \)-calculus
Recommended article: Q5144634
Recommended article: Q5854738
Recommended article: Towards Completeness via Proof Search in the Linear Time μ-calculus
Recommended article: μ-definable sets of integers
Recommended article: An extension of the omega-rule
Recommended article: Q5752561
description: scientific article; zbMATH DE number 6146088