A Buchholz Rule for Modal Fixed Point Logics

Logica Universalis 5 (1):1-19 (2011)
  Copy   BIBTEX


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).



    Upload a copy of this work     Papers currently archived: 94,517

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

On the Proof Theory of the Modal mu-Calculus.Thomas Studer - 2008 - Studia Logica 89 (3):343-363.
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Syntactic cut-elimination for a fragment of the modal mu-calculus.Kai Brünnler & Thomas Studer - 2012 - Annals of Pure and Applied Logic 163 (12):1838-1853.
Ordinal analysis by transformations.Henry Towsner - 2009 - Annals of Pure and Applied Logic 157 (2-3):269-280.
An intensional fixed point theory over first order arithmetic.Gerhard Jäger - 2004 - Annals of Pure and Applied Logic 128 (1-3):197-213.


Added to PP

73 (#222,992)

6 months
13 (#282,360)

Historical graph of downloads
How can I increase my downloads?