A Note on Expressive Coalgebraic Logics for Finitary Set Functors
Lawrence S. Moss · Journal of Logic and Computation · 2008
This article has two purposes. The first is to present a final coalgebra construction for finitary endofunctors on Set that uses a certain subset L* of the limit L of the first ω terms in the final sequence. L* is the set of points in L which arise from all coalgebras using their canonical morphisms into L, and it was used earlier for different purposes in Kurz and Pattinson (2005, Mathematical Structures in Computer Science, 15, 543–473). Viglizzo (2005, PhD Dessertation, Indiana University) showed that the same set L* carried a final coalgebra structure for functors in a certain inductively defined family. Our first goal is to generalize this to all finitary endofunctors; the result is implicit in Worrell (2005, Theoritical Computer Science, 338, 184–199). The second goal is to use the final coalgebra construction to propose coalgebraic logics similar to those in Lawrence S. Moss (1999, Annals of Pure and Applied Logic, 96, 277–317) but for all finitary endofunctors F on Set. This time one can dispense with all conditions on F, construct a logical language ℒF directly from it, and prove that two points in a coalgebra satisfy the same sentences of ℒF iff they are identified by the final coalgebra morphism. The language ℒF is very spare, having no boolean connectives. This work on ℒF is thus a re-working of coalgebraic logic for finitary functors on sets.