Solution (source code)

= Solution

A <Kripke model for intuitionistic propositional logic> for a propositional language is a poset $(S,\leq)$ together with a persistent forcing relation on atoms: if $w\Vdash p$ and $w\leq v$, then $v\Vdash p$. Extend forcing by
$$
w\Vdash\alpha\wedge\beta\iff w\Vdash\alpha\text{ and }w\Vdash\beta,
$$
$$
w\Vdash\alpha\vee\beta\iff w\Vdash\alpha\text{ or }w\Vdash\beta,
$$
and
$$
w\Vdash\alpha\to\beta\iff
\text{for every }v\geq w, v\Vdash\alpha\Longrightarrow v\Vdash\beta.
$$
No world forces $\bot$. Induction proves persistence for every proposition.