A Note on Expressive Coalgebraic Logics for Finitary Set Functors

摘要

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 L_f directly from it, and prove that two points in a coalgebra satisfy the same sentences of L_f iff they are identified by the final coalgebra morphism. The language L_f is very spare, having no boolean connectives. This work on L_f is thus a re-working of coalgebraic logic for finitary functors on sets.