Solution (source code)

= Solution

The <Kripke completeness theorem for intuitionistic propositional logic> states that, for every set of formulae $\Gamma$ and formula $A$,
$$
\Gamma\vdash_{\mathrm{IPC}}A
\quad\Longleftrightarrow\quad
\text{every world of every intuitionistic Kripke model that forces $\Gamma$ also forces $A$}.
$$
The forward implication is <soundness theorem for propositional logic>[soundness], and the reverse implication is completeness.