Completeness for Coalgebraic Fixpoint Logic

We introduce an axiomatization for the coalgebraic fixed point logic which was introduced by Venema as a generalization, based on Moss\u27 coalgebraic modality, of the well-known modal mu-calculus. Our axiomatization can be seen as a generalization of Kozen\u27s proof system for the modal mu-calculus to the coalgebraic level of generality. It consists of a complete axiomatization for Moss\u27modality, extended with Kozen\u27s axiom and rule for the fixpoint operators. Our main result is a completeness theorem stating that, for functors that preserve weak pullbacks and restrict to finite sets, our axiomatization is sound and complete for the standard interpretation of the language in coalgebraic models. Our proof is based on automata-theoretic ideas: in particular, we introduce the notion of consequence game for modal automata, which plays a crucial role in the proof of our main result. The result generalizes the celebrated Kozen-Walukiewicz completeness theorem for the modal mu-calculus, and our automata-theoretic methods simplify parts of Walukiewicz\u27 proof