$\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$
Canonical name	mathcalNJp
Date of creation	2013-03-22 13:05:17
Last modified on	2013-03-22 13:05:17
Owner	Henry (455)
Last modified by	Henry (455)
Numerical id	7
Author	Henry (455)
Entry type	Definition
Classification	msc 03F03
Synonym	NJp

𝒩𝒥p<math id="m1" class="ltx_Math" alttext="\mathcal{NJ}p" display="inline"><mrow><mi class="ltx_font_mathcaligraphic">𝒩</mi><mo>⁢</mo><mi class="ltx_font_mathcaligraphic">𝒥</mi><mo>⁢</mo><mi>p</mi></mrow></math>

$\mathcal{NJ}p$