Natural Deduction

Overview

Natural deduction is a proof system typically used alongside classical truth-functional propositional and predicate logic. It is meant to mimic the patterns of reasoning that one might "naturally" make when forming arguments in plain English.

Natural deduction is interesting in that it has no axioms.

Inference Rules

Scoped to propositional logic, there are 10 inference rules corresponding to an "introduction" and "elimination" of each propositional logic operator.

Negation

For propositions $E_{1}$ and $E_{2}$ ,

\neg - I : \begin{matrix} from E_{1} infer E_{2} \land \neg E_{2} \\ \neg E_{1} \end{matrix}

and

\neg - E : \begin{matrix} from \neg E_{1} infer E_{2} \land \neg E_{2} \\ E_{1} \end{matrix}

Conjunction

For propositions $E_{1}, \dots, E_{n}$ ,

\land - I : \begin{matrix} E_{1}, \dots, E_{n} \\ E_{1} \land \dots \land E_{n} \end{matrix}

and

\land - E : \begin{matrix} E_{1} \land \dots \land E_{n} \\ E_{i} \end{matrix}

Disjunction

For propositions $E_{1}, \dots, E_{n}$ ,

\lor - I : \begin{matrix} E_{i} \\ E_{1} \lor \dots \lor E_{n} \end{matrix}

and

\lor - E : \begin{matrix} E_{1} \lor \dots \lor E_{n}, E_{1} \Rightarrow E, \dots, E_{n} \Rightarrow E \\ E \end{matrix}

Implication

For propositions $E_{1}, \dots, E_{n}$ ,

\Rightarrow - I : \begin{matrix} from E_{1}, \dots, E_{n} infer E \\ (E_{1} \land \dots \land E_{n}) \Rightarrow E \end{matrix}

and

\Rightarrow - E : \begin{matrix} E_{1} \Rightarrow E_{2}, E_{1} \\ E_{2} \end{matrix}

Biconditional

For propositions $E_{1}$ and $E_{2}$ ,

\Leftrightarrow - I : \begin{matrix} E_{1} \Rightarrow E_{2}, E_{2} \Rightarrow E_{1} \\ E_{1} \Leftrightarrow E_{2} \end{matrix}

and

\Leftrightarrow - E : \begin{matrix} E_{1} \Leftrightarrow E_{2} \\ E_{1} \Rightarrow E_{2}, E_{2} \Rightarrow E_{1} \end{matrix}