Proof theory for fragments of the modal mu-calculus
Lukas Zenger

Abstract:
In this thesis we investigate the proof theory of the fragment Σ_1^μ ∪ Π_1^μ of the modal mu-calculus. This fragment consists of formulas which have syntactic fixed point alternation depth of at most one. Σ_1^μ ∪ Π_1^μ contains the building blocks for interesting concepts such as common knowledge. Moreover, it is computationally important in view of applications in database theory. We define a circular proof system and a circular tableaux system for Σ_1^μ ∪ Π_1^μ and prove soundness and completeness. We then use these systems to establish key properties of Σ_1^μ ∪ Π_1^μ such as the finite model property and Craig interpolation. Furthermore, we define infinitary proof systems for the whole modal mu-calculus and show that they are sound and complete. The main contribution of the thesis is an axiomatization of Σ_1^μ ∪ Π_1^μ as well as novel proofs of the finite model property and Craig interpolation.