Definition Discrete one-step modal operator [efr-002E]

Consider the theory of discrete dynamical systems, and let \xi : TS \leftrightarrows A = {\bar {A} \choose A} be a system. Let \phi : S \to \{\bot ,\top \} be a predicate on S, and let {\bar {U} \choose U} \subseteq {\bar {A} \choose A} be a subobject of A (that is, \bar {U} \subset \bar {A} and U \subset A, and if (a,a') \in \bar {U} then a \in A).

Then write \nabla _{U}(\phi ) for the predicate on S which is true if and only if the following hold: \xi (s) \in U, and if a' \in \bar {U} \times _A S, then \xi ^\#(s,a') satisfies \phi . In other words---the output is in U, and if the input is further in \bar {U}, then the next step will satisfy \phi .

Note that by taking U = A, \bar {U} = \bar {A} this encodes a simple next-step modality.

Observe also that, if A,\bar {A} are both finite, we can encode all the classical covering modality operators as (finite) conjunctions of \nabla _{\{(a,a_i)\}}\phi _i, and hence the logic built up of these modal operators and Boolean operations will enjoy the Hennessy-Milner property.