Non-distributive positive logic as a fragment of first-order logic over semilattices

TL;DR

This paper characterizes non-distributive positive logic as a fragment of first-order logic over semilattices, introducing meet-simulations to understand model preservation and establishing a Hennessy-Milner theorem with meet-compactness.

Contribution

It introduces meet-simulations for non-distributive positive logic and characterizes this logic as a fragment of first-order logic over semilattices, extending model-theoretic tools.

Findings

Meet-simulations distinguish models by relating pairs of states to single states.

A Hennessy-Milner theorem is proved using meet-compactness.

Non-distributive positive logic is characterized as a first-order fragment preserved by meet-simulations.

Abstract

We characterise non-distributive positive logic as the fragment of a single-sorted first-order language that is preserved by a new notion of simulation called a meet-simulation. Meet-simulations distinguish themselves from simulations because they relate pairs of states from one model to single states from another. En route to this result we use a more traditional notion of simulations and prove a Hennessy-Milner style theorem for it, using an analogue of modal saturation called meet-compactness.