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

{{{\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 $\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}

4.

for $\perp$ , there is one rule, an introduction rule $\perp\!I$ (ex falso quodlibet):

$\perp$ $A$ $(\perp\!I)$

In short, intuitionistic propositional logic is classical propositional logic without the rule RAA (reductio ad absurdum). Furthermore, $\neg$ is a defined one-place 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 (http://planetmath.org/DeductionsFromNaturalDeduction). 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

$[A]_{2}$ $[\neg A]_{1}$ $(\to\!E)$ $\perp$ $(\to\!I)_{1}$ $\neg A\to\perp$ $(\to\!I)_{2}$ $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

$[A]_{1}$ A→¬¬A $(\to\!E)$ $\neg\neg A$ $[\neg\neg\neg A]_{2}$ $(\to\!E)$ $\perp$ $(\to\!I)_{1}$ $\neg A$ $(\to\!I)_{2}$ $\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$ :

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

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

Title	natural deduction for intuitionistic propositional logic
Canonical name	NaturalDeductionForIntuitionisticPropositionalLogic
Date of creation	2013-03-22 19:32:11
Last modified on	2013-03-22 19:32:11
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	25
Author	CWoo (3771)
Entry type	Definition
Classification	msc 03B20
Classification	msc 03F03
Classification	msc 03F55
Related topic	DisjunctionProperty