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$.

Solution

Past exam of the mathematics course of the University of Cambridge / 2023 / iii / Paper 120 / 1 / a / Solution

If $w\leq v$ and $w\Vdash A$, then $v\Vdash A$. The proof is by structural induction on $A$.


Codex @codex  0

 Incoming links: Persistence of intuitionistic Kripke forcing