$\mathcal{NJ}p$ is a natural deduction proof system for intuisitionistic propositional logic. Its only axiom is $\alpha\Rightarrow\alpha$ for any atomic $\alpha$ Its rules are:

$$\begin{array}{cc} \frac{\begin{array}{c}\Gamma\Rightarrow\alpha\end{array}}{ \begin{array}{cc} \Gamma\Rightarrow\alpha\vee\beta& \Gamma\Rightarrow\beta\vee\alpha \end{array}{cc}}(\vee I) & \frac{\begin{array}{ccc} \Gamma\Rightarrow\alpha& \Sigma,\alpha^0\Rightarrow\phi& \Pi,\beta^0\Rightarrow\phi \end{array}} {\begin{array}{c}[\Gamma,\Sigma,\Pi]\Rightarrow\phi\end{array}}(\vee E) \end{array}$$

The syntax $\alpha^0$ indicates that the rule also holds if that formula is omitted.

$$\begin{array}{cc} \frac{\begin{array}{cc} \Gamma\Rightarrow\alpha& \Sigma\Rightarrow\beta \end{array}}{\begin{array}{c} [\Gamma,\Sigma]\Rightarrow\alpha\wedge\beta\end{array}}(\wedge I) & \frac{\begin{array}{c}\Gamma\Rightarrow\alpha\wedge\beta\end{array}} {\begin{array}{cc} \Gamma\Rightarrow\alpha& \Gamma\Rightarrow\beta \end{array}}(\wedge E) \end{array}$$

$$\begin{array}{cc} \frac{\begin{array}{c}\Gamma,\alpha\Rightarrow\beta\end{array}}{ \begin{array}{c}\Gamma\Rightarrow\alpha\rightarrow\beta\end{array}}(\rightarrow I) & \frac{\begin{array}{cc} \Gamma\Rightarrow\alpha\rightarrow\beta& \Sigma\Rightarrow\alpha \end{array}} {\begin{array}{c}[\Gamma,\Sigma]\Rightarrow\beta\end{array}}(\rightarrow E) \end{array}$$

$$\frac{\Gamma\Rightarrow\bot}{\Gamma\Rightarrow\alpha}\text{ where }\alpha\text{ is atomic}(\bot_i)$$