$\\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

$\\mathcal{NJ}p$