Soundness ($\mathbf{K} \vdash \varphi \implies \models_K \varphi$): All axioms of $\mathbf{K}$ are valid in all Kripke frames, and the rules (modus ponens, necessitation) preserve validity.

Completeness ($\models_K \varphi \implies \mathbf{K} \vdash \varphi$): We prove the contrapositive: if $\mathbf{K} \not\vdash \varphi$, then $\neg \varphi$ is $\mathbf{K}$-consistent, so $\{\neg \varphi\}$ can be extended to a maximally $\mathbf{K}$-consistent set $w_0$ (by Lindenbaum's lemma).

Construct the canonical model $\mathcal{M} = (W, R, V)$:

• $W$: all maximally $\mathbf{K}$-consistent sets of formulas.
• $R$: $w R v$ iff $\{\psi : \Box \psi \in w\} \subseteq v$.
• $V$: $V(p) = \{w \in W : p \in w\}$.

Truth Lemma: By induction on formula complexity, $\mathcal{M}, w \models \psi \iff \psi \in w$. The modal case: $\mathcal{M}, w \models \Box \psi \iff$ for all $v$ with $wRv$, $\psi \in v \iff \Box \psi \in w$. The right-to-left direction uses: if $\Box \psi \in w$ and $wRv$, then $\psi \in v$ by definition of $R$. The left-to-right direction uses: if $\Box \psi \notin w$, construct $v$ with $\{\chi : \Box \chi \in w\} \cup \{\neg \psi\}$ consistent, extend to maximal, giving $wRv$ and $\psi \notin v$.

Since $\neg \varphi \in w_0$, we have $\mathcal{M}, w_0 \models \neg \varphi$, so $\varphi$ is not valid. $\square$