Kripke completeness theorem for intuitionistic propositional logic
= Kripke completeness theorem for intuitionistic propositional logic
{c}
A proposition is derivable in intuitionistic propositional logic exactly when it is forced at every world of every intuitionistic Kripke model.