Semantics of Coalgebraic Logic

(draft)

We first review the definitions and results that make sense for the general setting of coalgebraic logic.

Syntax and Semantics¶

one-step syntax

syntax is the initial algebra

one-step semantics

semantics wrt $X\to TX$

For the next result we assume that $\mathcal X$ is a concrete category. Various generalisations to abstract categories are also possible.

Proposition: Formulas are invariant under bisimilarity.

Proof: Follows from the naturality of $LP \to PT$.

The Logic Functor Induced by the Coalgebra Functor¶

The definitions above are parametric in $L$ and $LP\to PT$.

On the other hand, from a coalgebraic point of view, $T$ is given and we should ask how to derive $L$ from $T$.

If $\mathcal A$ is a variety in the sense of universal algebra, then we can define a functor by its action on the free algebras. Moreover, if the variety has a presentation by operations of finite arity, then we can restrict attention to finitely generated free algebras and define $L$ as

where $n$ ranges over finite sets.

(to be continued)