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. For accessible/weak-pullback-preserving functors the final coalgebra exists and bisimilarity coincides with behavioral equivalence. Coalgebraic modal logics are sound and complete (rank-1 axiomatizations via predicate liftings), have the Hennessy–Milner property (logical equivalence = bisimilarity for image-finite systems), and admit generic decidability and coalgebraic bisimulation-up-to techniques. Duality (Stone/Vietoris) connects coalgebras and their logics.

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. Requires the system to be presented as a functor coalgebra; some behaviors need elaborate functors. Final coalgebras may fail to exist for functors that are not accessible (e.g., full powerset on Set). Bisimulation and behavioral equivalence diverge when the functor does not preserve weak pullbacks (notably some probabilistic cases). Expressiveness of the induced logic depends on having enough separating predicate liftings.

© 2026 Lingenic LLC