PlanetMath (more info)
 Math for the people, by the people. Sponsor PlanetMath
Encyclopedia | Requests | Forums | Docs | Wiki | Random | RSS  
Login
create new user
name:
pass:
forget your password?
Main Menu
Owner confidence rating: Medium Entry average rating: No information on entry rating
$\mathcal{NJ}p$ (Definition)

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




"$\mathcal{NJ}p$" is owned by Henry.
(view preamble | get metadata)

View style:

Other names:  NJp
Log in to rate this entry.
(view current ratings)

Cross-references: formula, syntax, axiom, propositional logic, proof, natural deduction
There is 1 reference to this entry.

This is version 3 of $\mathcal{NJ}p$, born on 2002-10-03, modified 2002-10-03.
Object id is 3504, canonical name is MathcalNJp.
Accessed 3198 times total.

Classification:
AMS MSC03F03 (Mathematical logic and foundations :: Proof theory and constructive mathematics :: Proof theory, general)

Pending Errata and Addenda
None.
[ View all 1 ]
Discussion
Style: Expand: Order:
forum policy

No messages.

Interact
post | correct | update request | add derivation | add example | add (any)