$\mathcal{NJ}p$

$\mathcal{NJ}p$ is a natural deduction proof system for intuitionistic 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}(\bot_{i}),\quad\text{ % where }\alpha\text{ is atomic}

𝒩⁢𝒥⁢p