Coalgebraic Logic

Origin. Coalgebra as a general theory of state-based systems: Aczel (non-well-founded sets, 1988), Rutten (universal coalgebra, 2000). Coalgebraic modal logic: Moss (1999), Pattinson, Kupke, Cîrstea. The uniform framework in which transition systems, automata, streams, and probabilistic systems are all coalgebras, and modal logics are their specification languages.

Models. Dynamical, observable, possibly infinite behavior — the categorical dual of algebra. Where an algebra F(X) → X builds values, a coalgebra X → F(X) unfolds a state into its one-step observations. The functor F fixes the system type (labeled transitions, probabilities, streams); behavior is captured up to bisimulation by the final coalgebra.

Formalism.

Coalgebra: Fix an endofunctor F on a category (usually Set). An F-coalgebra is (X, γ) with γ : X → F(X); X is the state space, γ the transition/observation map. Homomorphism (X,γ) → (Y,δ): f with δ ∘ f = F(f) ∘ γ.

Examples by functor: F(X) = 𝒫(X): unlabeled transition systems (Kripke frames). F(X) = 𝒫(X)^A: labeled transition systems. F(X) = 2 × X^A: deterministic automata (output × next on input). F(X) = A × X: streams. F(X) = 𝒟(X): probabilistic (distribution functor) — Markov chains.

Behavior and finality: The final F-coalgebra, if it exists, is the space of all behaviors. Unique map [[·]] : (X,γ) → final coalgebra assigns each state its behavior. Coinduction: two states equal iff bisimilar; proofs by exhibiting a bisimulation. Bisimulation = span of coalgebra homomorphisms (Aczel–Mendler).

Coalgebraic modal logic: Modalities interpreted by predicate liftings λ : 2^(−) ⇒ 2^(F(−)). Moss's ∇ operator: one polymorphic modality parametric in F. Semantics: x ⊨ ♡φ iff γ(x) ∈ [♡]. Recovers ◇/□ for F = 𝒫, graded modalities for multiset functor, probabilistic modalities for 𝒟.

Symbols.

Metatheory. Lambek's lemma states that the structure map of a final coalgebra is an isomorphism, so F(Z) ≅ Z, and Cantor's argument then shows the full powerset functor has no final coalgebra. Every accessible — equivalently, bounded — endofunctor on Set does have one, and Worrell (2005) proved that for a finitary functor the terminal sequence converges at ω + ω, giving the final coalgebra as an explicit limit. Bisimilarity in the Aczel–Mendler sense coincides with behavioural equivalence whenever F preserves weak pullbacks, and can be strictly finer when it does not. On the logical side, Pattinson (2003) showed that a modal logic presented by predicate liftings with rank-1 axioms is sound and complete for the corresponding class of coalgebras, one-step completeness lifting to full completeness; Schröder (2008) proved expressiveness — logical equivalence coincides with behavioural equivalence — exactly when the set of predicate liftings is separating. Schröder and Pattinson established a generic PSPACE upper bound for rank-1 coalgebraic logics, recovering Ladner's bound for K as an instance, and Cîrstea, Kupke and Pattinson gave EXPTIME tableaux for the coalgebraic μ-calculus. Kupke, Kurz and Venema's Stone coalgebras identify descriptive general frames with coalgebras for the Vietoris functor, which is the coalgebraic form of Jónsson–Tarski duality.

Applies to. Uniform semantics of transition systems, automata, and probabilistic systems. Stream and infinite-data programming (coinductive definitions). Modal and description logic generalization. Process equivalence and minimization. Reasoning about state-based components.

Limitations. Coalgebras for a functor validate exactly its rank-1 theory, so the generic completeness theorem does not reach axioms of higher rank: reflexivity □p → p and transitivity □p → □□p are conditions on a subclass of coalgebras rather than properties of the functor, and S4 and S5 fall outside the uniform treatment. Final coalgebras fail to exist for non-accessible functors, the full powerset on Set being the standard case. Moss's ∇ needs the functor to preserve weak pullbacks so that relation lifting is functorial; where preservation fails, as for the monotone neighbourhood functor, bisimilarity is strictly finer than behavioural equivalence. Expressiveness requires a separating set of predicate liftings, which not every functor admits. Finality yields branching-time behaviour only, so trace equivalence must be recovered in a Kleisli or Eilenberg–Moore category instead. Combining system types is obstructed: there is no distributive law of the powerset monad over the distribution monad, so probabilistic nondeterminism has no canonical coalgebraic type.

© 2026 Lingenic LLC