You are here
Homenatural deduction for propositional logic
Primary tabs
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 $\perp$ for falsity, and two logical connectives $\land$ and $\to$. The other connectives are defined as follows:

$\neg A:=A\to\perp$,

$A\lor B:=\neg(\neg A\land\neg B)$,

$A\leftrightarrow B:=(A\to B)\land(B\to A)$.
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 $\perp$, there are two rules, one introduction $\perp\!I$ (ex falso quodlibet), and one RAA (reductio ad absurdum):
$\infer[(\perp\!I)]{A}{\perp}\infer[(RAA)]{A}{\infer*{\perp}{[\neg A]}}$
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 $\neg A$, and then reach a contradiction ($\perp$), and hence we conclude with $A$. Of course, $\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. 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))$

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

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

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

$A\leftrightarrow\neg\neg A$
For example, $\vdash\neg(A\land\neg A)$ as \prooftree \AxiomC$[A\land\neg A]_{1}$ \RightLabel$(\land\!E_{L})$ \UnaryInfC$A$ \AxiomC$[A\land\neg A]_{1}$ \RightLabel$(\land\!E_{R})$ \UnaryInfC$\neg A$ \RightLabel$(\to\!E)$ \BinaryInfC$\perp$ \RightLabel$(\to\!I)_{1}$ \UnaryInfC$(A\land\neg A)\to\perp$ is a derivation of $(A\land\neg A)\to\perp$, which is $\neg(A\land\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,\neg A\vdash\perp$,
2. if $\Sigma\cup\{A\}\vdash\perp$, then $\Sigma\vdash\neg A$,
3. $A\vdash A\lor B$ and $B\vdash A\lor B$,
4. if $\Sigma\cup\{A\}\vdash C$ and $\Sigma\cup\{B\}\vdash C$, then $\Sigma\cup\{A\lor B\}\vdash C$.
Remark. If $\neg$ and $\lor$ were introduced as primitive logical symbols instead of them as being “defined”, then we need to have inference rules for $\neg$ and $\lor$ as well:
1. for $\neg$, there are two rules, one introduction $\neg I$ and one elimination $\neg E$:
$\infer[(\neg I)]{\neg A}{\infer*{\perp}{[A]}}\infer[(\neg E)]{\perp}{A&\quad% \neg A}$ 2. 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]}}$
Note that the inference rules correspond to the metatheorems above: rule $\neg E$ corresponds to metatheorem 1, $\neg I$ corresponds to 2, $\lor\!I_{L}$ and $\lor\!I_{R}$ correspond to 3, and $\lor\!E$ to 4. The resulting system is deductively equivalent to original NK system.
Mathematics Subject Classification
03F03 no label found03B05 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