Characterising Modal Formulas with Examples

TL;DR

This paper explores finite characterizations of modal formulas, showing that certain modal languages admit finite characterizations while others do not, depending on their expressive features.

Contribution

It introduces the concept of finite characterizations in modal logic, characterizes when they exist, and demonstrates that positive modal language without certain constants admits finite characterizations.

Findings

Finite characterizations exist for the positive modal language without $ op$ and $ot$.

Finite characterizations are rare for full modal languages unless the logic is locally tabular.

Adding certain constants or negations prevents finite characterizations from existing.

Abstract

We initiate the study of finite characterizations and exact learnability of modal languages. A finite characterization of a modal formula w.r.t. a set of formulas is a finite set of finite models (labelled either positive or negative) which distinguishes this formula from every other formula from that set. A modal language L admits finite characterisations if every L-formula has a finite characterization w.r.t. L. This definition can be applied not only to the basic modal logic K, but to arbitrary normal modal logics. We show that a normal modal logic admits finite characterisations (for the full modal language) iff it is locally tabular. This shows that finite characterizations with respect to the full modal language are rare, and hence motivates the study of finite characterizations for fragments of the full modal language. Our main result is that the positive modal language without the truth-constants $\top$ and $\bot$ admits finite characterisations. Moreover, we show that this result is essentially optimal: finite characterizations no longer exist when the language is extended with the truth constant $\bot$ or with all but very limited forms of negation.