Past exam of the computer science course of the University of Oxford / 2015 / Computer aided formal verification / 3 / a / Solution

Write $A=\mathrm{Sat}(\Phi )\subseteq S$. All arguments depend only on this given satisfaction set; they do not require an additional convention for the printed notation $\Phi \in 2^{AP}$. For a state $s$, let $\mathrm{Post}(s)=\{t:s\to t\}$. The power set $2^S$ is ordered by set inclusion.

Take $X\subseteq Y\subseteq S$ and any $s\in H(X)$. By the definition of $H$, we have both $s\in A$ and $\mathrm{Post}(s)\subseteq X$. By transitivity of set inclusion, $\mathrm{Post}(s)\subseteq Y$, so $s\in H(Y)$. Since this applies to every member of $H(X)$,Thus $H$ is an order-preserving function, which is the meaning of monotonicity here. This proof does not need either finiteness or the absence of terminal states.