Title: Completeness of Moss's Coalgebraic Logic 

Alexander Kurz, Leicester

Abstract: Aczel and Mendler (1989) showed that (i) for any set-functor
T, the domain equation X=TX has a solution, namely the final
T-coalgebra and that (ii) this final coalgebra classifies bisimilarity
of T-coalgebras. Moss (1999) showed that any (weak pullback
preserving) functor T induces a logic which characterises
T-bisimilarity, ie has the Hennessy-Milner property. Roughly speaking,
Moss's logic is a modal logic with T itself as the only modal
operator. But Moss didn't give a proof system for his logic. In this
talk, we present a complete proof system of the (finitary) Moss
logic. The main point is that the completeness proof is uniform in the
functor T. This is achieved by exploiting different ideas from domain
theory (in logical form), universal algebra, and category theory.

Joint work with Clemens Kupke and Yde Venema