is a natural deduction proof system for intuisitionistic propositional logic. Its only axiom is for any atomic . Its rules are:
The syntax indicates that the rule also holds if that formula is omitted.