Finitary coalgebraic logics Clemens Kupke Abstract: Finitary coalgebraic logics Clemens Kupke The aim of this thesis is to deepen our understanding of the close connection between modal logic and coalgebras. This connection becomes not only manifest in the fact that Kripke frames are a special type of coalgebras, but more generally in the fact that the relationship between modal logic and coalgebras can be seen to be the categorical dual of the fruitful and well-studied relationship between equational logic and algebras. Various types of modal languages have been proposed in the literature for reasoning about coalgebras. In this thesis we consider the following three approaches: The inductively defined languages for Kripke polynomial functors, which were developed in successive papers by Kurz, Roessiger and Jacobs, Pattinson's coalgebraic modal languages that are given by predicate liftings, and finitary coalgebraic fixed point logics, which were introduced by Venema as a modification of Moss' infinitary coalgebraic logics. Throughout the thesis we hold the view that a useful logical language for reasoning about coalgebras should have finitary syntax. Therefore all languages that we discuss are finitary. Languages with a finitary syntax, however, generally lack the Hennessy-Milner property. It is therefore a natural question whether one can find a class of coalgebras that still allows for logics with finitary syntax that have the Hennessy-Milner property. We propose to resolve this issue by generalizing a well-known concept from modal logic, namely the concept of a descriptive general frame. These descriptive general frames can be represented as coalgebras for the Vietoris functor on the category of Stone spaces. Hence Stone coalgebras, i.e. coalgebras for functors over the category of Stone spaces, are a natural generalization of this concept. One way of increasing the expressivity of a modal language is the use of so-called fixed point operators. Venema's coalgebraic fixed point logics have a finitary syntax and offer the possibility to reason about infinite, ongoing behaviour. These logics can be seen as a generalization of the modal mu-calculus and they allow, similar to the modal mu-calculus, for an automata-theoretic interpretation: there is a one-to-one correspondence between formulas of coalgebraic fixed point logic and the so-called coalgebra automata. In this thesis we prove certain closure properties of coalgebra automata and show that the non-emptiness problem of coalgebra automata is in many cases decidable. Our results can be looked at from two perspectives: Firstly they generalize known results about automata on infinite objects, such as automata on infinite words, trees and graphs. Secondly our results have logical corollaries: we show that coalgebraic fixed point logics all enjoy the finite model property. This yields in particular a proof of the finite model property of the modal mu-calculus. As another consequence we obtain decidability for a large class of coalgebraic fixed point logics. Furthermore we prove the soundness of a certain distributive law for the modal operator of coalgebraic logic. The thesis is structured as follows: After the Introduction in Chapter 1, we give an overview over three types of modal languages which are discussed in this thesis. Chapter 3 contains a first application of the idea of considering coalgebras over Stone spaces. We look at inductively defined logics for Kripke polynomial functors: for every Kripke polynomial functor we define a corresponding functor on the category of Stone spaces and obtain what we call the class of Vietoris polynomial functors. For each of these functors we obtain the final coalgebra using a modified canonical model construction. This construction yields, in particular, that the languages associated with Vietoris polynomial functors have the Hennessy-Milner property. Furthermore we prove that for every Vietoris polynomial functor F and the logic associated to it, there exists an adjunction between the algebraic semantics of the logic, defined as a category of many-sorted algebras, and the category of F-coalgebras. Finally we give a characterization of those many-sorted algebras for which this adjunction turns into an equivalence of categories. In Chapter 4 we turn to coalgebraic modal logics given in terms of a set of predicate liftings and a set of axioms with modal depth 1. Given an endofunctor F on the category of sets or the category of Stone spaces and a logic for F we devise a functor L on the category of Boolean algebras. The category of algebras for this functor constitutes the algebraic semantics for the logic. We use this algebraic semantics to give a categorical analysis of conditions for the logic to be sound and complete with respect to the coalgebraic semantics. This is done by relating soundness and completeness of the logic to properties of a natural transformation that connects the functors L and F. For the case that F is a functor on Stone spaces we obtain the following result: the logic is sound, complete and has the Hennessy-Milner property if L is dual to F. In Chapter 5 we prove closure properties of coalgebra automata and we show how one can effectively solve the non-emptiness problem for a large class of coalgebra automata. The main result of this chapter is the proof that for every coalgebra automaton we can construct an equivalent non-deterministic coalgebra automaton. The proof works uniformly for all types of coalgebra automata, in the special case of tree automata it implies Rabin's complementation lemma.