Semantics of formulas

We define the relation $\models$ between states and formulas (where $s\models \phi$ means: in state s formula $\phi$ holds) inductively on the structure of formulas as the least relation satisfying:

$$\begin{array} {lll} s\models \true;\\ s\models \phi \land \p... ...\models R \sees Y ~$implies$~s\models S \oncesaid X.\end{array}$$

The notation $\phi[x \becomes u]$ above means: $\phi$ with u substituted for the free occurrences of x . If $\psi = (\forall \phi :: \phi)$, the whole formula $\psi$ may be substituted for $\phi$, and since $\phi[\phi \becomes \psi] = \psi$, the ``recursion'' in the definition of $\models$ is unbounded, whence the appeal above to ``least relation''.

Note that the relation $\models$ is not monotonic in its left argument, i.e., when $s \subseteq s'$, $s \models {\cal A}$ does in general not imply $s' \models {\cal A}$.