Temporal aspects of the modal logic of subset spaces (Q1960421)

A logic of knowledge and time is presented in the paper. It seems that a combination of knowledge and time in the frame of modal logic provides a powerful tool for applications in computer science and artificial intelligence. The author starts off with the so-called topological modal logic of Moss and Parikh. The logic describes the situations in which the knowledge of an agent increases if computational effort is spent. The increasing of knowledge amounts to a successive shrinking of the set of states the agent considers possible in the course of time. In this way a topological component comes into play. Formally, the logic is a bimodal system with two operators, \(K\) representing knowledge and \(\square\) representing effort. Heinemann's logic makes more explicit the temporal content of the effort operator by adding a nextstep operator to the Moss-Parikh formalism. A language \(LK\) is defined. It is based on a set \(PV\) of propositional variables. Formulas are defined as usual, using propositional connectives and modal operators. The basic modal operators are \(K\), \(\circ\) (nextstep), and \(\square\). The semantical structures are triples \((X, d, \sigma)\) (called subset tree models). \(X\) is a non-empty set. From the viewpoint of topological reasoning \(d\) is a crucial component: is is a sequence \(\langle E_{1}, \dots, E_{n}, \dots \rangle\) of equivalence relations on X such that for each \(j\) every class of \(E_{j}\) splits into some classes of \(E_{j+1}\) (the knowledge leads to a more detailed ability to distinguish). The pair \({\mathcal F} = (X, d)\) is called a subset tree frame. Finally, \(\sigma\) is a valuation (a mapping from \(PV \times X\) to \(\{ 0, 1 \}\)). A common satisfiability relation is defined and a set of axioms is proposed. It is proved that the axiomatization is sound and complete. Moreover, the set of \(LK\)-formulas holding in every subset tree model is decidable. The paper contains also some complexity results. The satisfiability problem of certain classes of prefix formulas is feasible. A small hierarchy (of formulas of a multiagent version of the language \(LK\) w.r.t. the complexity of the satisfiability problem) is constructed.