Game semantics for lattice-based modal μ-calculus

Abstract

In this paper, we generalize modal $\hat{I}¼$-calculus to the non-distributive (lattice-based) modal $\hat{I}¼$-calculus and formalize some scenarios regarding categorization using it. We also provide a game semantics for the developed logic. The proof of adequacy of this game semantics proceeds by generalizing the unfolding games on the power-set algebras to the arbitrary lattices and showing that these games can be used to determine the least and the greatest fixed points of a monotone operator on a lattice. Finally, we define a notion of bisimulations on the polarities and show invariance of non-distributive modal $\hat{I}¼$-calculus under them.