Non-distributive positive logic as a fragment of first-order logic over semilattices
arXiv:2208.11354 · doi:10.1093/logcom/exad003
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.