Hennessy-Milner Properties via Topological Compactness

TL;DR

This paper extends Hennessy-Milner properties to various intuitionistic and modal logics using topological compactness, providing new semantic tools for understanding model saturation.

Contribution

It introduces topological compactness-based methods to establish Hennessy-Milner properties for multiple intuitionistic and modal logics.

Findings

Hennessy-Milner classes characterized for intuitionistic and dual-intuitionistic logics

Generalization of results to modal and bi-intuitionistic logics

Introduction of image-compact and pre-image-compact relations as semantic tools

Abstract

We give Hennessy-Milner classes for intuitionistic, dual-intuitionistic and bi-intuitionistic logic interpreted in intuitionistic Kripke models, and generalise these results to modal (dual- and bi-)intuitionistic logics. Our main technical tools are image-compact and pre-image-compact relations that provide a semantical description of modal saturation properties.