Kripke model for intuitionistic propositional logic
= Kripke model for intuitionistic propositional logic
{c}
A Kripke model is a poset of worlds with a persistent valuation of atoms. Conjunction and disjunction are forced pointwise, while $w\Vdash\alpha\to\beta$ exactly when every $v\geq w$ that forces $\alpha$ also forces $\beta$.
The forcing relation is the intuitionistic instance of <Kripke semantics>; persistence and the order on worlds determine its implication clause.