Implicational fragment of intuitionistic propositional logic ($\mathrm{IPC}(\to )$)

The implicational fragment of intuitionistic propositional logic contains formulas built from atoms using only logical implication, with only implication introduction, implication elimination, and assumptions as proof rules.

The canonical worlds are deductively closed implicational theories ordered by inclusion. A world forces an atom exactly when the atom belongs to that theory. The truth lemma says that a world forces an implicational formula exactly when the formula belongs to the theory.

For implicational formulas $\Gamma$ and $\phi$,The reverse implication follows from the canonical Kripke model for implicational intuitionistic logic and its truth lemma.

If $\Gamma$ and $\phi$ are implicational and $\Gamma {⊢}_{\mathrm{IPC}}\phi$, then $\Gamma {⊢}_{\mathrm{IPC}(\to )}\phi$. Soundness for Kripke semantics followed by Kripke completeness of implicational intuitionistic logic proves the claim.