= Solution
A <Kripke model for intuitionistic propositional logic> is a triple $(W,\leq,V)$ in which $(W,\leq)$ is a <partially ordered set> of worlds and $V(p)\subseteq W$ is upward closed for every propositional variable $p$. The <Kripke forcing relation> is defined recursively by
$$
w\Vdash p\iff w\in V(p),
$$
with the usual clauses for $\top$, $\bot$, conjunction and disjunction, and with
$$
w\Vdash A\to B
\iff
\text{for every }v\geq w,\ v\Vdash A\Longrightarrow v\Vdash B.
$$
The upward closure of the valuation implies <persistence of intuitionistic Kripke forcing>: if $w\leq v$ and $w\Vdash A$, then $v\Vdash A$.
Back to article page
