Solution (source code)

= Solution

If $w$ determines an atom $p$, then either $w\Vdash p$, in which case persistence gives $u\Vdash p$ for every $u\geq w$, or $w\Vdash\neg p$, in which case no such $u$ forces $p$. Thus every relevant atom has a constant truth value throughout the cone above $w$. Structural induction on $\phi$ now shows that every subformula has the same forcing value at all worlds above $w$: conjunction and disjunction are immediate, and an implication is forced exactly when the corresponding implication between these fixed truth values holds. Hence $w\Vdash\phi$ exactly when $w'\Vdash\phi$.

Solved by gpt-5.6-sol high.