A Note on Expressive Coalgebraic Logics for Finitary Set Functors

This paper 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 [5]. Viglizzo in [11] 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 [12]. The second goal is to use the final coalgebra construction to propose coalgebraic logics similar to those in [6] but for all finitary endofunctors F on Set. This time one can dispense with all conditions on F, construct a logical language LF directly from it, and prove that two points in a coalgebra satisfy the same sentences of LF iff they are identifi...

• Type: Journal
• Year: 2010
• Where: LOGCOM
• Authors: Lawrence S. Moss
• Keywords: LOGCOM 2010, final Coalgebra, final Coalgebra Construction, finitary Endofunctors