Named Models in Coalgebraic Hybrid Logic

TL;DR

This paper develops a general framework for coalgebraic hybrid logic, establishing criteria for named canonical models and proving completeness results, including for graded hybrid logic with local binding.

Contribution

It introduces generic criteria for the existence of named canonical models in coalgebraic hybrid logic and proves completeness for various extensions, including graded hybrid logic.

Findings

Established criteria for named canonical models in coalgebraic hybrid logic

Proved completeness for pure extensions and local binding extensions

Demonstrated the framework with multiple examples, including graded hybrid logic

Abstract

Hybrid logic extends modal logic with support for reasoning about individual states, designated by so-called nominals. We study hybrid logic in the broad context of coalgebraic semantics, where Kripke frames are replaced with coalgebras for a given functor, thus covering a wide range of reasoning principles including, e.g., probabilistic, graded, default, or coalitional operators. Specifically, we establish generic criteria for a given coalgebraic hybrid logic to admit named canonical models, with ensuing completeness proofs for pure extensions on the one hand, and for an extended hybrid language with local binding on the other. We instantiate our framework with a number of examples. Notably, we prove completeness of graded hybrid logic with local binding.