A Buchholz rule for modal fixed point logics (Q1942334): Difference between revisions

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.