# General note

The below page is a copy of the revision 96983 of Definition:Natural Deduction, accessible here.

## Definition

Natural deduction is a proof system for propositional logic.

As such, it consists of certain axioms, which together constitute a collection of theorems.

This can be specified as follows.

### Notation

To indicate that a collection of WFFs $P$, the pool of assumptions, entails a particular WFF $p$, the conclusion, we agree to write a sequent:

$P \vdash p$

To make exposition more natural, we also agree to omit the brackets of explicit set definition and use commas in a suggestive way, so that:

$p, q \vdash p \land q$
$P, Q \vdash p \land q$
$P, p \vdash q$

are used instead of the formally more correct:

$\left\{{p, q}\right\} \vdash p \land q$
$P \cup Q \vdash p \land q$
$P \cup \left\{{p}\right\} \vdash q$

Furthermore, in the last expression it is implicitly understood that $p \notin P$.

The $\Large\leadsto$ symbol indicates that given the sequent(s) on the left-hand side, the sequent on the right-hand side may be inferred.

### Axioms

Natural deduction has the following twelve axioms, explained in more detail on their own pages:

 $\text {(\mathrm{ND}:\mathrm A)}: \quad$ $\displaystyle$  $\displaystyle q \vdash q$ Rule of Assumption $\text {(\mathrm{ND}:\lor \mathcal I_1)}: \quad$ $\displaystyle P \vdash p$ $\, \Large\leadsto \,$ $\displaystyle P \vdash p \lor q$ Rule of Addition $\text {(\mathrm{ND}:\lor \mathcal I_2)}: \quad$ $\displaystyle P \vdash q$ $\, \Large\leadsto \,$ $\displaystyle P \vdash p \lor q$ Rule of Addition $\text {(\mathrm{ND}:\lor \mathcal E)}: \quad$ \displaystyle \left.{ \begin{align} P &\vdash p \lor q \\ Q, p &\vdash r \\ R, q &\vdash r \end{align} }\right\} $\, \Large\leadsto \,$ $\displaystyle P, Q, R \vdash r$ Proof by Cases $\text {(\mathrm{ND}:\land \mathcal I)}: \quad$ \displaystyle \left.{ \begin{align} P &\vdash p \\ Q &\vdash q \end{align} }\right\} $\, \Large\leadsto \,$ $\displaystyle P, Q \vdash p \land q$ Rule of Conjunction $\text {(\mathrm{ND}:\land \mathcal E_1)}: \quad$ $\displaystyle P \vdash p \land q$ $\, \Large\leadsto \,$ $\displaystyle P \vdash p$ Rule of Simplification $\text {(\mathrm{ND}:\land \mathcal E_2)}: \quad$ $\displaystyle P \vdash p \land q$ $\, \Large\leadsto \,$ $\displaystyle P \vdash q$ Rule of Simplification $\text {(\mathrm{ND}:\implies \mathcal I)}: \quad$ $\displaystyle P, p \vdash q$ $\, \Large\leadsto \,$ $\displaystyle P \vdash p \implies q$ Rule of Implication $\text {(\mathrm{ND}:\implies \mathcal E)}: \quad$ \displaystyle \left.{ \begin{align} P &\vdash p \implies q \\ Q &\vdash p \end{align} }\right\} $\, \Large\leadsto \,$ $\displaystyle P, Q \vdash q$ Modus Ponendo Ponens $\text {(\mathrm{ND}:\neg \mathcal I)}: \quad$ $\displaystyle P, p \vdash \bot$ $\, \Large\leadsto \,$ $\displaystyle P \vdash \neg p$ Proof by Contradiction $\text {(\mathrm{ND}:\neg \mathcal E)}: \quad$ \displaystyle \left.{ \begin{align} P &\vdash p \\ Q &\vdash \neg p \end{align} }\right\} $\, \Large\leadsto \,$ $\displaystyle P, Q \vdash \bot$ Principle of Non-Contradiction $\text {(\mathrm{ND}:\bot \mathcal E)}: \quad$ $\displaystyle P \vdash \bot$ $\, \Large\leadsto \,$ $\displaystyle P \vdash p$ Rule of Explosion

### Theorems

The theorems of natural deduction are those WFFs $p$ allowing a sequent $\vdash p$, i.e., that may be derived with an empty pool of assumptions.

### Proofs

Although it is satisfying to find a (formal) proof of a theorem using the above rules, it is advisable to cast such a proof in a standard framework.

On ProofWiki, the framework chosen is that of a tableau proof, which most easily lends itself for a MediaWiki architecture.

However, many other notations exist and are used by various authors.

## Also see

There are many other proof systems for propositional logic, see here.