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.
![\begin{displaymath}\begin{array}{cc} \frac{\begin{array}{c}\Gamma\Rightarrow\alp... ...amma,\Sigma,\Pi]\Rightarrow\phi\end{array}}(\vee E) \end{array}\end{displaymath}](http://images.planetmath.org:8080/cache/objects/3504/l2h/img4.png "\begin{displaymath}\begin{array}{cc} \frac{\begin{array}{c}\Gamma\Rightarrow\alp... ...amma,\Sigma,\Pi]\Rightarrow\phi\end{array}}(\vee E) \end{array}\end{displaymath}")
![\begin{displaymath}\begin{array}{cc} \frac{\begin{array}{c}\Gamma,\alpha\Rightar... ...,\Sigma]\Rightarrow\beta\end{array}}(\rightarrow E) \end{array}\end{displaymath}](http://images.planetmath.org:8080/cache/objects/3504/l2h/img7.png "\begin{displaymath}\begin{array}{cc} \frac{\begin{array}{c}\Gamma,\alpha\Rightar... ...,\Sigma]\Rightarrow\beta\end{array}}(\rightarrow E) \end{array}\end{displaymath}")
where 
is atomic