= Solution
Write $A=\operatorname{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\in2^{AP}$. For a <state> $s$, let $\operatorname{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 $\operatorname{Post}(s)\subseteq X$. By transitivity of <set inclusion>, $\operatorname{Post}(s)\subseteq Y$, so $s\in H(Y)$. Since this applies to every member of $H(X)$,
$$
\boxed{X\subseteq Y\ \Longrightarrow\ H(X)\subseteq H(Y).}
$$
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>.
Back to article page
