Discrete duality for lattices with modal operators
Chrysafis Hartonas · Journal of Logic and Computation · 2018
It has been argued that in the context of automated theorem proving deduction procedures based on a frame semantics is more efficient than those based on algebraic semantics, for some logics. Frame semantics, for several logics, is specified by means of a representation and Stone-type duality result, involving a topology on the frame which, however, is not relevant in proving soundness of the logic. This has led to the development of a research program on Discrete Dualities, where a number of relevant results have been published over the past decade, but the program seems to have stumbled on the case of frames for non-distributive logics and bounded lattices with operators. In this article, we fill in this gap by presenting discrete dualities for bounded lattices and for lattices with one-place modal operators. Our results are extendible to discrete dualities for any normal lattice expansion.