 Kripke model for intuitionistic propositional logic

A Kripke model is a poset of worlds with a persistent valuation of atoms. Conjunction and disjunction are forced pointwise, while $w⊩\alpha \to \beta$ exactly when every $v\ge 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.