You are here
Homenatural deduction for intuitionistic propositional logic
Primary tabs
natural deduction for intuitionistic propositional logic
The natural deduction system for intuitionistic propositional logic described here is based on the language that consists of a set of propositional variables, a symbol $\perp$ for falsity, and logical connectives $\land$, $\lor$, $\to$. In this system, there are no axioms, only rules of inference.
1. for $\land$, there are three rules, one introduction rule $\land\!I$, and two elimination rules $\land\!E_{L}$ and $\land\!E_{R}$:
$\infer[(\land\!I)]{A\land B}{A&\quad B}\infer[(\land\!E_{L})]{A}{A\land B}% \infer[(\land\!E_{R})]{B}{A\land B}$ 2. for $\to$, there are two rules, one introduction $\to\!I$ and one elimination $\to\!E$ (modus ponens):
$\infer[(\to\!I)]{A\to B}{\infer*{B}{[A]}}\infer[(\to\!E)]{B}{A&\quad A% \rightarrow B}$ 3. for $\lor$, there are three rules, two introduction rules $\lor\!I_{E}$, $\lor\!I_{L}$, and one elimination rule $\lor\!E$:
$\infer[(\lor\!I_{L})]{A\lor B}{A}\infer[(\lor\!I_{R})]{A\lor B}{B}\infer[(\lor% \!E)]{C}{A\lor B&\quad\infer*{C}{[A]}\quad\infer*{C}{[B]}}$ 4. for $\perp$, there is one rule, an introduction rule $\perp\!I$ (ex falso quodlibet):
$\infer[(\perp\!I)]{A}{\perp}$
In short, intuitionistic propositional logic is classical propositional logic without the rule RAA (reductio ad absurdum). Furthermore, $\neg$ is a defined oneplace logical symbol: $\neg A:=A\to\perp$.
Remark. In the rules $\to\!I$ and $\lor\!E$, the square brackets around the top formula denote that the formula is removed, or discharged. In other words,
“once the conclusion is reached, the assumption can be dropped.”
In $\to\!I$, when the formula $B$ is deduced from the assumption or hypothesis $A$, we conclude with the formula $A\to B$. Once this conclusion is reached, $A$ is superfluous and therefore removed, as it is embodied in the formula $A\to B$. This is often encountered in mathematical proofs: if we want to prove $A\to B$, we first assume $A$, then we proceed with the proof and reach $B$, and therefore $A\to B$. Simiarly, in $\lor\!E$, if $C$ can be concluded from $A$ and from $B$ individually, then $C$ can be concluded from anyone of them, or $A\lor B$, without the assumptions $A$ and $B$ individually.
Intuitionistic propositional logic as defined by the natural deduction system above is termed NJ. Derivations and theorems for NJ are defined in the usual manner like all natural deduction systems, which can be found here. Some of the theorems of NJ are listed below:

$A\to(B\to A)$

$(A\to(B\to C))\to((A\to B)\to(A\to C))$

$(A\to B)\to(\neg B\to\neg A)$

$A\land B\to B\land A$

$\neg(A\land\neg A)$

$A\to\neg\neg A$

$\neg\neg\neg A\to\neg A$
For example, $\vdash A\to\neg\neg A$ as \prooftree \AxiomC$[A]_{2}$ \AxiomC$[\neg A]_{1}$ \RightLabel$(\to\!E)$ \BinaryInfC$\perp$ \RightLabel$(\to\!I)_{1}$ \UnaryInfC$\neg A\to\perp$ \RightLabel$(\to\!I)_{2}$ \UnaryInfC$A\to(\neg A\to\perp)$ and $A\to(\neg A\to\perp)$ is just $A\to\neg\neg A$. Also, $\vdash\neg\neg\neg A\to\neg A$, as \prooftree \AxiomC$[A]_{1}$ \AxiomC
A→¬¬A
\RightLabel$(\to\!E)$ \BinaryInfC$\neg\neg A$ \AxiomC$[\neg\neg\neg A]_{2}$ \RightLabel$(\to\!E)$ \BinaryInfC$\perp$ \RightLabel$(\to\!I)_{1}$ \UnaryInfC$\neg A$ \RightLabel$(\to\!I)_{2}$ \UnaryInfC$\neg\neg\neg A\to\neg A$ The subscripts indicate that the discharging of the assumptions at the top correspond to the applications of the inference rules $\to\!I$ at the bottom. The box around $A\to\neg\neg A$ indicates that the derivation of $A\to\neg\neg A$ has been embedded (as a subtree) into the derivation of $\neg\neg\neg A\to\neg A$.
Remark. If $\neg$ were introduced as a primitive logical symbol instead of it being as “defined”, then we need to have inference rules for $\neg$ as well, one of which is introduction $\neg I$, and the other elimination $\neg E$:
$\infer[(\neg I)]{\neg A}{\infer*{\perp}{[A]}}\infer[(\neg E)]{\perp}{A&\quad% \neg A}$ 
Note that in the original NJ system, $\neg I$ is just an instance of $\to\!I$, and $\neg E$ is just an instance of $\to\!E$.
Mathematics Subject Classification
03B20 no label found03F03 no label found03F55 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections