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}$ :

{{{\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.

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.

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,

“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 (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.

$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$ :

{{{{\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.

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
Canonical name	NaturalDeductionForPropositionalLogic
Date of creation	2013-03-22 19:31:59
Last modified on	2013-03-22 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