= Solution
Soundness follows by induction on derivations: assumptions are forced by hypothesis, implication introduction uses the definition of <Kripke forcing relation>, and implication elimination uses it at the current world.
For completeness, form the <canonical Kripke model for implicational intuitionistic logic>. Its worlds are <deductively closed set of formulae>[deductively closed] implicational theories $\Delta$ extending $\operatorname{Cn}(\Gamma)$, ordered by inclusion, and
$$
\Delta\Vdash p\quad\Longleftrightarrow\quad p\in\Delta
$$
for each atom $p$. We prove the truth lemma
$$
\Delta\Vdash\alpha\quad\Longleftrightarrow\quad\alpha\in\Delta
$$
by induction on implicational formulas. The atomic case is the definition. For $\alpha\to\beta$, membership implies forcing by closure under implication elimination. Conversely, if $\alpha\to\beta\notin\Delta$, the implication-introduction rule shows that $\operatorname{Cn}(\Delta\cup\{\alpha\})$ does not contain $\beta$; this extension forces $\alpha$ but not $\beta$, so $\Delta$ does not force $\alpha\to\beta$.
If $\Gamma\nvdash_{\mathrm{IPC}(\to)}\varphi$, the root $\operatorname{Cn}(\Gamma)$ of this canonical model forces every member of $\Gamma$ but does not force $\varphi$. Together with soundness, this proves <Kripke completeness of implicational intuitionistic logic>.
Finally suppose the implicational formulas $\Gamma$ and $\varphi$ satisfy $\Gamma\vdash_{\mathrm{IPC}}\varphi$. The <soundness theorem for propositional logic> for intuitionistic Kripke semantics gives $\Gamma\models_{\mathrm{Kripke}}\varphi$, and the completeness just proved gives $\Gamma\vdash_{\mathrm{IPC}(\to)}\varphi$. This is the <conservativity of intuitionistic propositional logic over its implicational fragment>.
Back to article page
