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