Implicational fragment of intuitionistic propositional logic

ID: implicational-fragment-of-intuitionistic-propositional-logic

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.

New to topics? Read the docs here!