A Buchholz Rule for Modal Fixed Point Logics

Buchholz’s Ω _μ+1-rules provide a major tool for the proof-theoretic analysis of arithmetical inductive definitions. The aim of this paper is to put this approach into the new context of modal fixed point logic. We introduce a deductive system based on an Ω-rule tailored for modal fixed point logic and develop the basic techniques for establishing soundness and completeness of the corresponding system. In the concluding section we prove a cut elimination and collapsing result similar to that of Buchholz (Iterated inductive definitions and subsystems of analysis: recent proof theoretic studies. Lecture notes in mathematics, vol. 897, pp. 189–233, Springer, Berlin, 1981).