= Solution
Let $X$ be any <fixed point> of $H$. Then
$$
X=H(X)=A\cap\{s:\operatorname{Post}(s)\subseteq X\},
$$
so $X\subseteq A$ and every successor of every member of $X$ belongs to $X$. Take $s_0\in X$ and an arbitrary infinite <path in a transition system> $s_0s_1s_2\cdots$ from $s_0$. By <mathematical induction>, every $s_i$ belongs to $X$: the base case is the choice of $s_0$, and $s_i\in X$ implies $s_{i+1}\in\operatorname{Post}(s_i)\subseteq X$.
Since $X\subseteq A$, the whole <path in a transition system> stays in $A$. The <path in a transition system> was arbitrary, so $s_0\models\forall\square\Phi$. Thus $s_0\in G_\Phi$, and since $s_0$ was arbitrary in $X$,
$$
X\subseteq G_\Phi.
$$
Part (b) proves that $G_\Phi$ itself is a <fixed point>. Therefore
$$
\boxed{\operatorname{Sat}(\forall\square\Phi)=\nu X.\,H(X),}
$$
the <greatest fixed point> with respect to <set inclusion>. In fact the same induction works for every $X\subseteq H(X)$, showing why a successor-closed <set> of good <states> certifies this universal property.
Back to article page
