Kripke model for intuitionistic propositional logic
= Kripke model for intuitionistic propositional logic
{c}
{wiki=Kripke_semantics#Semantics_of_intuitionistic_logic}
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$.