No label defined (Q4215596)

Topological nexttime logic (TNL) is a bimodal logic with two modalities -- \(\bigcirc\), the nexttime operator, and \(K\), the knowledge operator. The (propositional) language of TNL is defined as usual. The semantical domains of TNL are triples \((X, d, \sigma)\), where \(X\) is a non-empty set, \(d\) is a mapping from an initial segment \(I\) of the set of natural numbers into the powerset of \(X\) such that \(i \leq j\) implies \(d(i) \supseteq d(j)\) for all \(i, j \in I\), and \(d(i) \not = \emptyset\) for all \(i \in I\), \(\sigma : PV \times X \rightarrow \{0, 1 \}\), where \(PV\) is a recursively enumerable set of propositional variables. The semantics of TNL is defined as follows. Let \({\mathcal M} = (X, d, \sigma)\), \(I\) be the domain of \(d\) and \({\mathcal O} := d(I)\). Then \[ X \otimes {\mathcal O} := \{ (x, d(i)) : i \in I,\;d(i) \in {\mathcal O},\;x \in d(i) \} \] is called the set of neighborhood situations. The validity relation is defined for neighborhood situations; for example, if \(A\) is a propositional variable, then \(x, d(i) \models_{\mathcal M} A\) iff \(\sigma(A, x) = 1\), \(x, d(i) \models_{\mathcal M} K \alpha\) iff \((\forall y \in d(i)) y, d(i) \models_{\mathcal M} \alpha\), \(x, d(i) \models_{\mathcal M} \bigcirc \alpha\) iff \(i+1 \in I, x \in d(i+1)\), and \(x, d(i+1) \models_{\mathcal M} \alpha\). A set of axioms and rules is presented. Soundness, completeness, and decidability results are proven. Finally, it is shown that the TNL-satisfiability problem is NP-complete. For the entire collection see [Zbl 0897.00022].