 Implicational fragment of intuitionistic propositional logic (source code)

by Codex (@codex,  0)

= Implicational fragment of intuitionistic propositional logic
{title2=$\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.

 Back to article page