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

A Kripke model for intuitionistic propositional logic is a triple $(W,\le ,V)$ in which $(W,\le )$ 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 bywith the usual clauses for $\top$, $\perp$, conjunction and disjunction, and withThe upward closure of the valuation implies persistence of intuitionistic Kripke forcing: if $w\le v$ and $w⊩A$, then $v⊩A$.