# 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)$.

1. 1.

for $\land$, there are three rules, one introduction rule $\land\!I$, and two elimination rules $\land\!E_{L}$ and $\land\!E_{R}$:

 {{{\hbox{\vbox{ \moveright 11.249828pt\vbox{\halign{\cr}A&\quad\quad B}}\nointerlineskip% \kern 2.0pt\moveright 0.0pt\vbox{\hrule width 22.499657pt height 1px}% \nointerlineskip\kern 2.0pt\moveright 0.0pt\hbox{A\land B}}\kern-29.999542pt% \kern 5.0pt\raise 6.499931pt\hbox{(\land\!I)}\kern 0.0pt}\hskip 56.905512pt% \hbox{\vbox{ \moveright 3.749943pt\vbox{\halign{\cr}A\land B}}\nointerlineskip\kern 2.0pt% \moveright 0.0pt\vbox{\hrule width 7.499886pt height 1px}\nointerlineskip\kern 2% .0pt\moveright 0.0pt\hbox{A}}\kern-14.999771pt\kern 5.0pt\raise 7.039923pt% \hbox{(\land\!E_{L})}\kern 0.0pt}\hskip 56.905512pt\hbox{\vbox{ \moveright 3.749943pt\vbox{\halign{\cr}A\land B}}\nointerlineskip\kern 2.0pt% \moveright 0.0pt\vbox{\hrule width 7.499886pt height 1px}\nointerlineskip\kern 2% .0pt\moveright 0.0pt\hbox{B}}\kern-14.999771pt\kern 5.0pt\raise 7.039923pt% \hbox{(\land\!E_{R})}\kern 0.0pt}
2. 2.

for $\to$, there are two rules, one introduction $\to\!I$ and one elimination $\to\!E$ (modus ponens  ):

 {{{{\hbox{\vbox{ \moveright 14.999771pt\vbox{\halign{\cr}\vbox{ \moveright 7.499886pt\vbox{\halign{\cr}\vbox{ \moveright 14.999771pt\vbox{\halign{\cr}[A]}}\nointerlineskip\kern 2.0pt% \moveright 0.0pt\hbox{\hbox{\vtop{\vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}}% }}}\nointerlineskip\kern 2.0pt\moveright 0.0pt\hbox{\hbox{B}}}}}% \nointerlineskip\kern 2.0pt\moveright 0.0pt\vbox{\hrule width 22.499657pt heig% ht 1px}\nointerlineskip\kern 2.0pt\moveright 0.0pt\hbox{A\to B}}\kern-29.999% 542pt\kern 5.0pt\raise 6.499931pt\hbox{(\to\!I)}\kern 0.0pt}\hskip 56.905512% pt\hbox{\vbox{ \moveright 3.749943pt\vbox{\halign{\cr}A&\quad\quad A\rightarrow B}}% \nointerlineskip\kern 2.0pt\moveright 0.0pt\vbox{\hrule width 7.499886pt heigh% t 1px}\nointerlineskip\kern 2.0pt\moveright 0.0pt\hbox{B}}\kern-14.999771pt% \kern 5.0pt\raise 6.499931pt\hbox{(\to\!E)}\kern 0.0pt}
3. 3.

for $\perp$, there are two rules, one introduction $\perp\!I$ (ex falso quodlibet), and one RAA (reductio ad absurdum   ):

 {{{{\hbox{\vbox{ \moveright 3.749943pt\vbox{\halign{\cr}\perp}}\nointerlineskip\kern 2.0pt% \moveright 0.0pt\vbox{\hrule width 7.499886pt height 1px}\nointerlineskip\kern 2% .0pt\moveright 0.0pt\hbox{A}}\kern-14.999771pt\kern 5.0pt\raise 6.499931pt% \hbox{(\perp\!I)}\kern 0.0pt}\hskip 56.905512pt\hbox{\vbox{ \moveright 7.499886pt\vbox{\halign{\cr}\vbox{ \moveright 7.499886pt\vbox{\halign{\cr}\vbox{ \moveright 14.999771pt\vbox{\halign{\cr}[\neg A]}}\nointerlineskip\kern 2.0% pt\moveright 0.0pt\hbox{\hbox{\vtop{\vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}% }}}}}\nointerlineskip\kern 2.0pt\moveright 0.0pt\hbox{\hbox{\perp}}}}}% \nointerlineskip\kern 2.0pt\moveright 0.0pt\vbox{\hrule width 7.499886pt heigh% t 1px}\nointerlineskip\kern 2.0pt\moveright 0.0pt\hbox{A}}\kern-14.999771pt% \kern 5.0pt\raise 6.499931pt\hbox{(RAA)}\kern 0.0pt}

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,

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

• $(\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

$[A\land\neg A]_{1}$   $(\land\!E_{L})$          $A$         $[A\land\neg A]_{1}$   $(\land\!E_{R})$         $\neg A$          $(\to\!E)$                                                          $\perp$                                                  $(\to\!I)_{1}$                                                  $(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 meta-theorems:

1. 1.

$A,\neg A\vdash\perp$,

2. 2.

if $\Sigma\cup\{A\}\vdash\perp$, then $\Sigma\vdash\neg A$,

3. 3.

$A\vdash A\lor B$ and $B\vdash A\lor B$,

4. 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. 1.

for $\neg$, there are two rules, one introduction $\neg I$ and one elimination $\neg E$:

 {{{{\hbox{\vbox{ \moveright 11.249828pt\vbox{\halign{\cr}\vbox{ \moveright 7.499886pt\vbox{\halign{\cr}\vbox{ \moveright 14.999771pt\vbox{\halign{\cr}[A]}}\nointerlineskip\kern 2.0pt% \moveright 0.0pt\hbox{\hbox{\vtop{\vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}}% }}}\nointerlineskip\kern 2.0pt\moveright 0.0pt\hbox{\hbox{\perp}}}}}% \nointerlineskip\kern 2.0pt\moveright 0.0pt\vbox{\hrule width 14.999771pt heig% ht 1px}\nointerlineskip\kern 2.0pt\moveright 0.0pt\hbox{\neg A}}\kern-22.499% 657pt\kern 5.0pt\raise 6.499931pt\hbox{(\neg I)}\kern 0.0pt}\hskip 56.905512% pt\hbox{\vbox{ \moveright 3.749943pt\vbox{\halign{\cr}A&\quad\quad\neg A}}% \nointerlineskip\kern 2.0pt\moveright 0.0pt\vbox{\hrule width 7.499886pt heigh% t 1px}\nointerlineskip\kern 2.0pt\moveright 0.0pt\hbox{\perp}}\kern-14.99977% 1pt\kern 5.0pt\raise 6.499931pt\hbox{(\neg E)}\kern 0.0pt}
2. 2.

for $\lor$, there are three rules, two introduction rules $\lor\!I_{E}$, $\lor\!I_{L}$, and one elimination rule $\lor\!E$:

 {{{{{{{\hbox{\vbox{ \moveright 11.249828pt\vbox{\halign{\cr}A}}\nointerlineskip\kern 2.0pt% \moveright 0.0pt\vbox{\hrule width 22.499657pt height 1px}\nointerlineskip% \kern 2.0pt\moveright 0.0pt\hbox{A\lor B}}\kern-29.999542pt\kern 5.0pt\raise 7% .039923pt\hbox{(\lor\!I_{L})}\kern 0.0pt}\hskip 56.905512pt\hbox{\vbox{ \moveright 11.249828pt\vbox{\halign{\cr}B}}\nointerlineskip\kern 2.0pt% \moveright 0.0pt\vbox{\hrule width 22.499657pt height 1px}\nointerlineskip% \kern 2.0pt\moveright 0.0pt\hbox{A\lor B}}\kern-29.999542pt\kern 5.0pt\raise 7% .039923pt\hbox{(\lor\!I_{R})}\kern 0.0pt}\hskip 56.905512pt\hbox{\vbox{ \moveright 7.499886pt\vbox{\halign{\cr}A\lor B&\quad\quad\vbox{ \moveright 7.499886pt\vbox{\halign{\cr}\vbox{ \moveright 14.999771pt\vbox{\halign{\cr}[A]}}\nointerlineskip\kern 2.0pt% \moveright 0.0pt\hbox{\hbox{\vtop{\vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}}% }}}\nointerlineskip\kern 2.0pt\moveright 0.0pt\hbox{\hbox{C}}}\quad\vbox{ \moveright 7.499886pt\vbox{\halign{\cr}\vbox{ \moveright 14.999771pt\vbox{\halign{\cr}[B]}}\nointerlineskip\kern 2.0pt% \moveright 0.0pt\hbox{\hbox{\vtop{\vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}}% }}}\nointerlineskip\kern 2.0pt\moveright 0.0pt\hbox{\hbox{C}}}}}% \nointerlineskip\kern 2.0pt\moveright 0.0pt\vbox{\hrule width 7.499886pt heigh% t 1px}\nointerlineskip\kern 2.0pt\moveright 0.0pt\hbox{C}}\kern-14.999771pt% \kern 5.0pt\raise 6.499931pt\hbox{(\lor\!E)}\kern 0.0pt}

Note that the inference rules correspond to the meta-theorems above: rule $\neg E$ corresponds to meta-theorem 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.

Title natural deduction for propositional logic NaturalDeductionForPropositionalLogic 2013-03-22 19:31:59 2013-03-22 19:31:59 CWoo (3771) CWoo (3771) 25 CWoo (3771) Definition msc 03F03 msc 03B05 natural deduction for classical propositional logic NK