# $\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}$
Title $\mathcal{NJ}p$ mathcalNJp 2013-03-22 13:05:17 2013-03-22 13:05:17 Henry (455) Henry (455) 7 Henry (455) Definition msc 03F03 NJp