Cycles with annotations Non-wellfounded proof theory of modal fixpoint logics

This thesis studies non-wellfounded proof theory. In this setting, proofs may contain infinitely long branches or cycles.
In order to disallow absurd reasoning, a so-called soundness condition is formulated on those infinite branches and cycles.
The main challenge in non-wellfounded proof theory is to handle this soundness condition.
This thesis addresses several kinds of soundness conditions and is organized around two main themes.
First, we show how to employ annotations to obtain infinitary proof systems with simple path-based soundness conditions;
and we transform the latter into cyclic systems with local soundness conditions.
Second, we demonstrate how to use such annotated cyclic proof systems to derive results about their underlying logics.
The logics we consider are modal fixpoint logics.
The central logic studied is the modal μ-calculus, which extends basic modal logic with explicit least and greatest fixpoint operators.
We also investigate various extensions and fragments of the modal μ-calculus.
In Chapter 3 we develop determinization methods for ω-automata.
Chapter 4 focuses on non-wellfounded proof systems for the modal μ-calculus.
Using the automata-theoretic results established in Chapter 3, we add annotations to construct cyclic proof systems with local soundness conditions.
Additionally, we establish that the proof system Clo, introduced by Afshari and Leigh, is incomplete.
In Chapter 5 we introduce several proof systems for the two-way modal μ-calculus and use them to establish the Craig interpolation property.
Chapter 6 is devoted to Converse Propositional Dynamic Logic. We introduce an annotated cyclic proof system and employ it to prove that the logic satisfies Craig interpolation.
Finally, Chapter 7 addresses cut elimination for annotated cyclic proof systems. This result is obtained within the Focus system, defined by Marti and Venema for the alternation-free modal μ-calculus.