Moss' logic for ordered coalgebras

We present a finitary version of Moss' coalgebraic logic for \(T\)-coalgebras, where \(T\) is a locally monotone endofunctor of the category of posets and monotone maps. The logic uses a single cover modality whose arity is given by the least finitary subfunctor of the dual of the coalgebra fun...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2022-08
Main Authors: Bílková, Marta, Dostál, Matěj
Format: Article
Language:English
Subjects:
Intersections
Logic
Semantics
Set theory
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present a finitary version of Moss' coalgebraic logic for \(T\)-coalgebras, where \(T\) is a locally monotone endofunctor of the category of posets and monotone maps. The logic uses a single cover modality whose arity is given by the least finitary subfunctor of the dual of the coalgebra functor \(T_\omega^\partial\), and the semantics of the modality is given by relation lifting. For the semantics to work, \(T\) is required to preserve exact squares. For the finitary setting to work, \(T_\omega^\partial\) is required to preserve finite intersections. We develop a notion of a base for subobjects of \(T_\omega X\). This in particular allows us to talk about the finite poset of subformulas for a given formula. The notion of a base is introduced generally for a category equipped with a suitable factorisation system. We prove that the resulting logic has the Hennessy-Milner property for the notion of similarity based on the notion of relation lifting. We define a sequent proof system for the logic, and prove its completeness.
ISSN:2331-8422
DOI:10.48550/arxiv.1901.06547