Kripke forcing relation ($⊩$)

The Kripke forcing relation $w⊩A$ records that formula $A$ holds at world $w$. For intuitionistic implication, $w⊩A\to B$ exactly when every extension of $w$ that forces $A$ also forces $B$.

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

A Kripke countermodel to a formula $A$ is a Kripke model for intuitionistic propositional logic containing a world $w$ such that $w⊮A$.