Modal logics over lattices

DOI10.1016/J.APAL.2025.103553MaRDI QIDQ7032977zbMATH OpenFDO

Authors Xiaoyang Wang, Yanjing Wang

Publication date 4 February 2025

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.APAL.2025.103553

zbMATH Keywords

completeness hybrid logic lattices polyadic modal logic step by step tense logic

Mathematics Subject Classification ID

Temporal logic (03B44) Modal logic (including the logic of norms) (03B45)

Review text

The authors consider and axiomatize various systems of temporal logic arising when the underlying Kripke frame is a lattice. In doing so, they continue the line that started in [\textit{J. P. Burgess}, Synth. Libr. 165, 89-133 (1984; Zbl 0875.03046)] with axiomatization of temporal logic over strict preorders with an upper and lower bound for each pair of worlds.\N\NAxiomatizations of such logics are non-trivially influenced by our interpretation of modal accessibility relation which can be given either by the strict or by the non-strict version of the underlying lattice order.\N\NThe authors begin with the strict case and repeat the claim made in [loc. cit.] that the temporal logic over strict preorders with upper and lower bounds coincides with the strict-order temporal logic of unbounded lattices. Their idea is to axiomatize also the logics induced by the classes of bounded lattices and of the arbitrary lattices. Starting with the latter, the authors show that the logic of arbitrary lattices is the extension of the minimal normal temporal logic extended with the transitivity principle (which they assume in the form \(Gp\to GGp\)) plus the principle:\N\begin{align*}\N(M_1p \wedge M_1q) \to M_1((M_2p\wedge M_2q) \vee (p \wedge M_2q) \vee(M_2p\wedge q)\vee (p\wedge q))\N\end{align*}\Nwhere \(\{M_1, M_2\} = \{F, P\}\). The idea behind this axiom is to enforce the Church-Rosser property in the conditions where some nodes might be lacking successors.\N\NThe bounded case is then captured by extending this axiomatization with the principles \(G\bot\vee FG\bot\) and \(H\bot\vee PH\bot\) expressing the existence of a maximal (resp. minimal) node above (resp. below) every given node.\N\NAs for the logics based on the non-strict version of the lattice order, the logic induced by both the general class of lattices and its unbounded subclass is obtained from the logic axiomatized in [loc. cit.] by replacing the seriality axioms with reflexivity. To axiomatize the bounded case one needs the two temporal versions of the so-called McKinsey axioms.\N\NThe authors also observe that the basic language of temporal logic is unable to capture the uniqueness of suprema and infima in a lattice and turn to the language where the basic modalities are the dyadic \(\langle sup\rangle(\phi, \psi)\) and \(\langle inf\rangle(\phi, \psi)\); e.g. \(\langle sup\rangle(\phi, \psi)\) is true in a world iff it is a supremum of some \(\phi\)-world and some \(\psi\)-world and similarly for \(\langle inf\rangle\). The basic temporal modalities are definable in this language e.g. by setting \(P\phi:= \langle sup\rangle(\phi, \top)\) and similarly for \(F\); thus the new language is strictly more expressive than the basic temporal modal language. The authors also add the world nominals which results in getting many expressivity features of hybrid logics.\N\NThis rich language allows the authors to capture both the lattices and many important lattice subclasses, like those of distributive and modular lattices. They proceed by first axiomatizing the logic of lower connected connected frames then extending it to the logic induced by the class of all lattices. While the task seems to present few principled difficulties, the technical work takes up a considerable space and the resulting axiomatization is relatively lengthy partly due to the high expressivity of the chosen language. In fact, once the lattices in general have been described, the principles of distributivity and modularity can be written down quite straightforwardly using the nominals, suprema and infima.

Cites work

Cited in

(1)

Axiomatization and decidability of tense information logic

This page was built for publication: Modal logics over lattices

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7032977)