[proofplan] We prove the contrapositive. Assuming $\nvdash_{\mathrm{IPC}} A$, we construct the canonical Kripke model whose nodes are prime intuitionistic theories ordered by inclusion, with atomic forcing defined by membership. The key point is the truth lemma: at every prime theory $\Gamma$, forcing of a formula is exactly membership of that formula in $\Gamma$. Once the truth lemma is proved by induction on formulas, a prime theory omitting $A$ gives a node of the canonical model that does not force $A$, so $A$ is not valid in all Kripke models. [/proofplan] [step:Fix the language, theories, and the canonical order] Let $\operatorname{Form}(\mathcal{L})$ denote the set of formulas of the countable propositional language $\mathcal{L}$. For a set of formulas $\Sigma \subset \operatorname{Form}(\mathcal{L})$ and a formula $B \in \operatorname{Form}(\mathcal{L})$, write $\Sigma \vdash B$ to mean $\Sigma \vdash_{\mathrm{IPC}} B$. A set $\Gamma \subset \operatorname{Form}(\mathcal{L})$ is called an intuitionistic theory if it is deductively closed: whenever $\Gamma \vdash B$, one has $B \in \Gamma$. A theory $\Gamma$ is proper if $\bot \notin \Gamma$. A proper theory $\Gamma$ is prime if, for all formulas $B,C \in \operatorname{Form}(\mathcal{L})$, \begin{align*} B \vee C \in \Gamma \implies B \in \Gamma \text{ or } C \in \Gamma. \end{align*} Define the set of canonical nodes $W$ by \begin{align*} W := \{\Gamma \subset \operatorname{Form}(\mathcal{L}) : \Gamma \text{ is a prime intuitionistic theory}\}. \end{align*} Define the relation $\leq$ on $W$ by inclusion: for $\Gamma,\Delta \in W$, \begin{align*} \Gamma \leq \Delta \iff \Gamma \subset \Delta. \end{align*} This relation is a partial order because inclusion of sets is reflexive, transitive, and antisymmetric. For each atomic proposition $P$ of $\mathcal{L}$, define the valuation $V(P) \subset W$ by \begin{align*} V(P) := \{\Gamma \in W : P \in \Gamma\}. \end{align*} The valuation is monotone: if $\Gamma \leq \Delta$ and $\Gamma \in V(P)$, then $P \in \Gamma \subset \Delta$, hence $\Delta \in V(P)$. Therefore $(W,\leq,V)$ is a Kripke frame with a monotone valuation. Define the forcing relation $\Vdash \subset W \times \operatorname{Form}(\mathcal{L})$ recursively as follows. For each atomic proposition $P$, set $\Gamma \Vdash P$ iff $\Gamma \in V(P)$. No node forces falsity: $\Gamma \nVdash \bot$ for every $\Gamma \in W$. For formulas $B,C \in \operatorname{Form}(\mathcal{L})$, set $\Gamma \Vdash B \wedge C$ iff $\Gamma \Vdash B$ and $\Gamma \Vdash C$; set $\Gamma \Vdash B \vee C$ iff $\Gamma \Vdash B$ or $\Gamma \Vdash C$; and set $\Gamma \Vdash B \to C$ iff for every $\Delta \in W$ with $\Gamma \leq \Delta$, if $\Delta \Vdash B$, then $\Delta \Vdash C$. With these clauses, $(W,\leq,V)$ is a Kripke model for $\mathcal{L}$. [/step] [step:Construct prime theories that omit a prescribed formula] We need the following Lindenbaum-style extension fact. [claim:Prime extension omitting a formula] Let $\Sigma \subset \operatorname{Form}(\mathcal{L})$ and let $D \in \operatorname{Form}(\mathcal{L})$. If $\Sigma \nvdash D$, then there exists a prime intuitionistic theory $\Gamma$ such that $\Sigma \subset \Gamma$ and $D \notin \Gamma$. [/claim] [proof] Let $\mathbb{N} := \{1,2,3,\dots\}$. Because $\mathcal{L}$ is countable, enumerate all formulas of the form $B \vee C$ as a sequence $(E_n \vee F_n)_{n \in \mathbb{N}}$, where $E_n,F_n \in \operatorname{Form}(\mathcal{L})$, in such a way that every disjunction formula occurs infinitely many times in the sequence. Define an increasing sequence $(\Sigma_n)_{n \in \mathbb{N}}$ of sets of formulas as follows. Set $\Sigma_1 := \Sigma$. Having defined $\Sigma_n$ with $\Sigma_n \nvdash D$, consider the formula $E_n \vee F_n$. If $\Sigma_n \nvdash E_n \vee F_n$, set $\Sigma_{n+1} := \Sigma_n$. If $\Sigma_n \vdash E_n \vee F_n$, we claim that at least one of $\Sigma_n \cup \{E_n\} \nvdash D$ or $\Sigma_n \cup \{F_n\} \nvdash D$ holds. Indeed, suppose both failed. Then $\Sigma_n \cup \{E_n\} \vdash D$ and $\Sigma_n \cup \{F_n\} \vdash D$. By the [deduction theorem](/theorems/1452) for intuitionistic propositional calculus, $\Sigma_n \vdash E_n \to D$ and $\Sigma_n \vdash F_n \to D$. Since $\Sigma_n \vdash E_n \vee F_n$, [disjunction elimination](/theorems/4625) in intuitionistic propositional calculus gives $\Sigma_n \vdash D$, contradicting the induction hypothesis $\Sigma_n \nvdash D$. Thus choose one of $E_n$ and $F_n$ whose addition preserves non-derivability of $D$, and define $\Sigma_{n+1}$ to be $\Sigma_n$ together with that chosen formula. Let $\Sigma_\infty := \bigcup_{n=1}^{\infty} \Sigma_n$, and define \begin{align*} \Gamma := \{B \in \operatorname{Form}(\mathcal{L}) : \Sigma_\infty \vdash B\}. \end{align*} Then $\Sigma \subset \Gamma$, and $\Gamma$ is deductively closed by the transitivity of derivability. Also $D \notin \Gamma$: if $D \in \Gamma$, then $\Sigma_\infty \vdash D$, so by finitariness of intuitionistic proofs there is some $n \in \mathbb{N}$ with $\Sigma_n \vdash D$, contradicting the construction. The theory $\Gamma$ is proper. Indeed, if $\bot \in \Gamma$, then $\Sigma_\infty \vdash \bot$; since intuitionistic propositional calculus derives $D$ from $\bot$ by ex falso, we get $\Sigma_\infty \vdash D$, and finitariness again gives some $n \in \mathbb{N}$ with $\Sigma_n \vdash D$, contradicting the construction. It remains to prove primeness. Suppose $B \vee C \in \Gamma$. Then $\Sigma_\infty \vdash B \vee C$, so by finitariness there is $n_0 \in \mathbb{N}$ such that $\Sigma_{n_0} \vdash B \vee C$. Choose $m \in \mathbb{N}$ such that $E_m = B$ and $F_m = C$, and replace $m$ by a larger occurrence if necessary so that $m \geq n_0$. Since the sequence is increasing, $\Sigma_m \vdash B \vee C$. At stage $m$, the construction adds either $B$ or $C$ while preserving non-derivability of $D$. Hence $B \in \Sigma_{m+1} \subset \Sigma_\infty$ or $C \in \Sigma_{m+1} \subset \Sigma_\infty$. Therefore $B \in \Gamma$ or $C \in \Gamma$. Thus $\Gamma$ is a proper prime intuitionistic theory omitting $D$. [/proof] [/step] [step:Prove the truth lemma for the canonical Kripke model] For $\Gamma \in W$ and $B \in \operatorname{Form}(\mathcal{L})$, we prove \begin{align*} \Gamma \Vdash B \iff B \in \Gamma. \end{align*} The proof is by structural induction on $B$. For an atomic proposition $P$, the equivalence follows from the definition of $V(P)$: $\Gamma \Vdash P$ iff $\Gamma \in V(P)$ iff $P \in \Gamma$. For $\bot$, no node forces $\bot$ by the forcing clause for falsity, and no prime theory contains $\bot$ by properness. Hence $\Gamma \Vdash \bot$ iff $\bot \in \Gamma$. For $B \wedge C$, the induction hypothesis gives $\Gamma \Vdash B$ iff $B \in \Gamma$ and $\Gamma \Vdash C$ iff $C \in \Gamma$. The forcing clause gives $\Gamma \Vdash B \wedge C$ iff both $\Gamma \Vdash B$ and $\Gamma \Vdash C$ hold. Deductive closure gives $B \wedge C \in \Gamma$ iff both $B \in \Gamma$ and $C \in \Gamma$. Thus $\Gamma \Vdash B \wedge C$ iff $B \wedge C \in \Gamma$. For $B \vee C$, the forcing clause gives $\Gamma \Vdash B \vee C$ iff $\Gamma \Vdash B$ or $\Gamma \Vdash C$. By the induction hypothesis, this is equivalent to $B \in \Gamma$ or $C \in \Gamma$. Since $\Gamma$ is prime and deductively closed, this is equivalent to $B \vee C \in \Gamma$. It remains to handle implication. Suppose first that $B \to C \in \Gamma$. Let $\Delta \in W$ satisfy $\Gamma \leq \Delta$, and suppose $\Delta \Vdash B$. Since $\Gamma \subset \Delta$, one has $B \to C \in \Delta$. By the induction hypothesis applied at $\Delta$, $\Delta \Vdash B$ gives $B \in \Delta$. Since $\Delta$ is deductively closed and intuitionistic propositional calculus derives $C$ from $B \to C$ and $B$ by modus ponens, we get $C \in \Delta$. By the induction hypothesis again, $\Delta \Vdash C$. Therefore $\Gamma \Vdash B \to C$. Conversely, suppose $\Gamma \Vdash B \to C$ and $B \to C \notin \Gamma$. Since $\Gamma$ is deductively closed, $\Gamma \nvdash B \to C$. By the deduction theorem, $\Gamma \cup \{B\} \nvdash C$. Applying the prime extension claim with $\Sigma := \Gamma \cup \{B\}$ and $D := C$, obtain a prime theory $\Delta \in W$ such that $\Gamma \cup \{B\} \subset \Delta$ and $C \notin \Delta$. Then $\Gamma \leq \Delta$ and $B \in \Delta$, so by the induction hypothesis $\Delta \Vdash B$. Also $C \notin \Delta$, so by the induction hypothesis $\Delta \nVdash C$. This contradicts $\Gamma \Vdash B \to C$. Hence $B \to C \in \Gamma$. [guided] The only delicate connective is implication, because Kripke forcing for implication quantifies over all stronger nodes. We prove the equivalence \begin{align*} \Gamma \Vdash B \to C \iff B \to C \in \Gamma \end{align*} assuming the induction hypothesis has already been proved for $B$ and $C$ at every prime theory. First suppose $B \to C \in \Gamma$. To prove $\Gamma \Vdash B \to C$, we must check the Kripke forcing clause for implication. Thus let $\Delta \in W$ be a prime theory such that $\Gamma \leq \Delta$, meaning $\Gamma \subset \Delta$, and assume $\Delta \Vdash B$. Since $\Gamma \subset \Delta$ and $B \to C \in \Gamma$, we have $B \to C \in \Delta$. The induction hypothesis for $B$ at the node $\Delta$ converts the semantic assumption $\Delta \Vdash B$ into the syntactic membership statement $B \in \Delta$. Now $\Delta$ is deductively closed, and intuitionistic propositional calculus derives $C$ from $B \to C$ and $B$ by modus ponens. Therefore $C \in \Delta$. Applying the induction hypothesis for $C$ at $\Delta$, we obtain $\Delta \Vdash C$. Since this was shown for every stronger node $\Delta \geq \Gamma$, the forcing clause gives $\Gamma \Vdash B \to C$. For the converse, suppose $\Gamma \Vdash B \to C$ but $B \to C \notin \Gamma$. Because $\Gamma$ is deductively closed, non-membership means non-derivability from $\Gamma$: \begin{align*} \Gamma \nvdash B \to C. \end{align*} The deduction theorem for intuitionistic propositional calculus says that $\Gamma \cup \{B\} \vdash C$ holds exactly when $\Gamma \vdash B \to C$ holds. Therefore \begin{align*} \Gamma \cup \{B\} \nvdash C. \end{align*} This is the syntactic gap we need to turn into a semantic counterexample. Apply the prime extension lemma to the set $\Sigma := \Gamma \cup \{B\}$ and the formula $D := C$. It gives a prime theory $\Delta \in W$ such that $\Gamma \cup \{B\} \subset \Delta$ and $C \notin \Delta$. The inclusion $\Gamma \subset \Delta$ says exactly that $\Delta$ is a stronger node than $\Gamma$ in the canonical order. Since $B \in \Delta$, the induction hypothesis gives $\Delta \Vdash B$. Since $C \notin \Delta$, the induction hypothesis gives $\Delta \nVdash C$. But this is incompatible with $\Gamma \Vdash B \to C$, because the forcing clause for implication requires every stronger node that forces $B$ also to force $C$. Thus the assumption $B \to C \notin \Gamma$ is impossible, and we conclude $B \to C \in \Gamma$. [/guided] This completes the structural induction and proves the truth lemma for every formula $B$ and every canonical node $\Gamma \in W$. [/step] [step:Use a prime theory omitting the non-derivable formula] Assume $\nvdash A$. Apply the prime extension claim with $\Sigma := \varnothing$ and $D := A$. Since $\varnothing \nvdash A$, there exists a prime intuitionistic theory $\Gamma \in W$ such that $A \notin \Gamma$. By the truth lemma applied to the formula $A$ at the node $\Gamma$, we have \begin{align*} \Gamma \Vdash A \iff A \in \Gamma. \end{align*} Since $A \notin \Gamma$, it follows that $\Gamma \nVdash A$. The canonical structure $(W,\leq,V)$ is a Kripke model, so $A$ is not forced at every node of every Kripke model. [/step] [step:Conclude completeness by contraposition] We have proved the contrapositive: if $\nvdash_{\mathrm{IPC}} A$, then there exists a Kripke model and a node of that model at which $A$ is not forced. Therefore, if $A$ is forced at every node of every Kripke model for intuitionistic propositional logic, then $\vdash_{\mathrm{IPC}} A$. This is the Kripke completeness theorem for intuitionistic propositional logic. [/step]