natural deduction for propositional logic
The natural deduction system for classical propositional logic^{} described here is based on the language^{} that consists of a set of propositional variables, a symbol $\u27c2$ for falsity, and two logical connectives $\wedge $ and $\to $. The other connectives are defined as follows:

•
$\mathrm{\neg}A:=A\to \u27c2$,

•
$A\vee B:=\mathrm{\neg}(\mathrm{\neg}A\wedge \mathrm{\neg}B)$,

•
$A\leftrightarrow B:=(A\to B)\wedge (B\to A)$.
In this system, there are no axioms, only rules of inference^{}.

1.
for $\wedge $, there are three rules, one introduction rule $\wedge I$, and two elimination rules $\wedge {E}_{L}$ and $\wedge {E}_{R}$:
$$\text{A \hspace{1em} \u2062 \hspace{1em} B \u2227 A B}(\wedge I)\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{0.5em}\u2006}\text{\u2227 A B A}(\wedge {E}_{L})\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{0.5em}\u2006}\text{\u2227 A B B}(\wedge {E}_{R})$$ 
2.
for $\to $, there are two rules, one introduction $\to I$ and one elimination $\to E$ (modus ponens^{}):
$$\text{[ A ] .... B \u2192 A B}(\to I)\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{0.5em}\u2006}\text{A \hspace{1em} \u2192 \u2062 \hspace{1em} A B B}(\to E)$$ 
3.
for $\u27c2$, there are two rules, one introduction $\u27c2I$ (ex falso quodlibet), and one RAA (reductio ad absurdum^{}):
$$\text{\u27c2 A}(\u27c2I)\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{0.5em}\u2006}\text{[ \u2062 \xac A ] .... \u27c2 A}(RAA)$$
Remark. In the rules $\to I$ and RAA, 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 RAA, to prove $A$, we start by assuming $\mathrm{\neg}A$, and then reach a contradiction^{} ($\u27c2$), and hence we conclude with $A$. Of course, $\mathrm{\neg}A$ is no longer needed at this point.
Classical propositional logic as defined by the natural deduction system above is termed NK. Derivations and theorems^{} for NK are defined in the usual manner like all natural deduction systems, which can be found here (http://planetmath.org/DeductionsFromNaturalDeduction). Some of the theorems of NK are listed below:

•
$A\to (B\to A)$

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

•
$(\mathrm{\neg}A\to \mathrm{\neg}B)\to (B\to A)$

•
$A\wedge B\to B\wedge A$

•
$\mathrm{\neg}(A\wedge \mathrm{\neg}A)$

•
$A\leftrightarrow \mathrm{\neg}\mathrm{\neg}A$
For example, $\u22a2\mathrm{\neg}(A\wedge \mathrm{\neg}A)$ as
${[A\wedge \mathrm{\neg}A]}_{1}$ $\left(\wedge {E}_{L}\right)$ $A$ ${[A\wedge \mathrm{\neg}A]}_{1}$ $\left(\wedge {E}_{R}\right)$ $\mathrm{\neg}A$ $\left(\to E\right)$ $\u27c2$ ${(\to I)}_{1}$ $(A\wedge \mathrm{\neg}A)\to \u27c2$
is a derivation of $(A\wedge \mathrm{\neg}A)\to \u27c2$, which is $\mathrm{\neg}(A\wedge \mathrm{\neg}A)$, where all of the assumptions have been discharged. The subscript indicates that the discharging of the assumptions at the top correspond to the application of the inference rule $\to I$ at the bottom.
Note also that the first three theorems are the axiom schemas^{} for the Łukasiewicz’s axiom system for propositional logic, and it is easy to see that NK and the axiom system are in fact deductively equivalent: the theorems in both systems are precisely the same. In addition^{} to the theorems above, we also have the following metatheorems:

1.
$A,\mathrm{\neg}A\u22a2\u27c2$,

2.
if $\mathrm{\Sigma}\cup \{A\}\u22a2\u27c2$, then $\mathrm{\Sigma}\u22a2\mathrm{\neg}A$,

3.
$A\u22a2A\vee B$ and $B\u22a2A\vee B$,

4.
if $\mathrm{\Sigma}\cup \{A\}\u22a2C$ and $\mathrm{\Sigma}\cup \{B\}\u22a2C$, then $\mathrm{\Sigma}\cup \{A\vee B\}\u22a2C$.
Remark. If $\mathrm{\neg}$ and $\vee $ were introduced as primitive logical symbols instead of them as being “defined”, then we need to have inference rules for $\mathrm{\neg}$ and $\vee $ as well:

1.
for $\mathrm{\neg}$, there are two rules, one introduction $\mathrm{\neg}I$ and one elimination $\mathrm{\neg}E$:
$$\text{[ A ] .... \u27c2 \u2062 \xac A}(\mathrm{\neg}I)\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{0.5em}\u2006}\text{A \hspace{1em} \u2062 \hspace{1em} \xac A \u27c2}(\mathrm{\neg}E)$$ 
2.
for $\vee $, there are three rules, two introduction rules $\vee {I}_{E}$, $\vee {I}_{L}$, and one elimination rule $\vee E$:
$$\text{A \u2228 A B}(\vee {I}_{L})\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{0.5em}\u2006}\text{B \u2228 A B}(\vee {I}_{R})\mathit{\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{0.5em}\u2006}\text{\u2228 A B \hspace{1em} \u2062 \hspace{1em} [ A ] . . . . C \hspace{1em} [ B ] . . . . C C}(\vee E)$$
Note that the inference rules correspond to the metatheorems above: rule $\mathrm{\neg}E$ corresponds to metatheorem 1, $\mathrm{\neg}I$ corresponds to 2, $\vee {I}_{L}$ and $\vee {I}_{R}$ correspond to 3, and $\vee E$ to 4. The resulting system is deductively equivalent to original NK system.
Title  natural deduction for propositional logic 

Canonical name  NaturalDeductionForPropositionalLogic 
Date of creation  20130322 19:31:59 
Last modified on  20130322 19:31:59 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  25 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03F03 
Classification  msc 03B05 
Synonym  natural deduction for classical propositional logic 
Defines  NK 