Natural Deduction — Introduction and Elimination Rules

Actually building a proof system

Basic (1st–2nd year university)

Goal of this page

Understand the introduction and elimination rules given to each connective, and be able to read and write proof trees that involve discharging assumptions. Learn that this is precisely the propositional layer of a proof-checking kernel.

1. The idea of natural deduction

In the Introduction we met the idea of inference rules. Natural deduction is a proof system that organizes those inference rules systematically, connective by connective. The key is to give each connective a pair of rules:

  • Introduction rule: the rule that creates the connective
  • Elimination rule: the rule that uses the connective

It simply turns into rules the natural reasoning a mathematician does every day: "$A$ and $B$ hold, so $A$ and $B$ (together)," and "$A$ and $B$ together, so $A$ holds." It was organized by Gentzen and Prawitz.

2. Rules for each connective

First, how to read a rule

Every rule below is written with a horizontal line. Above the line are the premises (what is already established); below it is the conclusion (what newly follows).

$$\dfrac{\text{premise}_1 \quad \text{premise}_2 \quad \cdots}{\text{conclusion}}$$

That is, read it as "if everything above the line holds, then the bottom holds."

The $(\land\text{I})$ etc. on the right is the rule's name, read in two parts. The leading symbol ($\land$, $\lor$, $\to$, …) indicates "which connective the rule is about," and the following I means introduction (the rule that creates that connective), E means elimination (the rule that uses it). So $(\land\text{I})$ reads "the introduction rule for $\land$" = the rule that creates the conjunction $A \land B$.

The $\land$ in the name being the same symbol as the connective $\land$ in the conclusion is no coincidence: it shows "this is the rule about that $\land$." By the same logic, the rule that creates $\lor$ is $(\lor\text{I})$ and the one that creates $\to$ is $(\to\text{I})$, so the introduction/elimination names line up per connective.

Conjunction $\land$ (and)

Introduction $\land$I: if $A$ and $B$ hold separately, then together $A \land B$ ($A$ and $B$) holds.
Elimination $\land$E: if $A \land B$ holds, you can extract just $A$, or just $B$, from it.

$$\dfrac{A \quad B}{A \land B}\ (\land\text{I}) \qquad \dfrac{A \land B}{A}\ (\land\text{E}) \qquad \dfrac{A \land B}{B}\ (\land\text{E})$$

Read the left as "from the $A$ and $B$ above, the $A\land B$ below," and the right two as "from the $A\land B$ above, the $A$ (or $B$) below."

Implication $\to$ (if … then)

Start with the easier elimination $\to$E (modus ponens): if $A \to B$ ($A$ implies $B$) and $A$ both hold, then $B$ holds.

$$\dfrac{A \to B \quad A}{B}\ (\to\text{E})$$

Introduction $\to$I is the most characteristic rule of natural deduction: to assert $A \to B$ ("$A$ implies $B$"), first assume $A$ is true. This "tentatively placed $A$" is written in brackets as $[A]$. Under that assumption, derive for several steps (the vertical dots $\vdots$ denote "the intermediate derivation") and reach $B$; then you may conclude $A \to B$. At the same time, the placed assumption $[A]$ has served its purpose and is withdrawn (this is called discharge; treated in detail in §3 below).

$$\dfrac{\begin{matrix}[A] \\[2pt] \vdots \\[2pt] B\end{matrix}}{A \to B}\ (\to\text{I})$$

The vertical stack reads top to bottom as "assume $A$ → … intermediate derivation … → $B$ obtained," and below the line we conclude "therefore $A \to B$." It is exactly the everyday argument "if $A$ were the case, then $B$ follows; hence $A$ implies $B$."

Disjunction $\lor$ (or)

Introduction $\lor$I: if $A$ holds, then "$A$ or $B$" ($A \lor B$) of course holds (likewise from $B$ to $A \lor B$).

$$\dfrac{A}{A \lor B}\ (\lor\text{I}) \qquad \dfrac{B}{A \lor B}\ (\lor\text{I})$$

Elimination $\lor$E (case analysis): if $A \lor B$ holds and both "if $A$ then $C$" and "if $B$ then $C$" can be shown, then whichever of $A$, $B$ is actually true, the conclusion is $C$. This is exactly the familiar mathematical case analysis.

Example: if "$n$ is even or odd" holds, and both "if even then $n(n+1)$ is even" and "if odd then $n(n+1)$ is even" can be shown, then either way we conclude "$n(n+1)$ is even."

Introduction and elimination are balanced. For instance, building $A \land B$ by $\land$I and immediately extracting $A$ by $\land$E is a detour; you could have just used $A$ from the start. The operation that removes this "build then immediately use" waste is reduction, and it corresponds to computation (λ-calculus).

3. Discharging assumptions and proof trees

Implication introduction $\to$I is the most characteristic operation of natural deduction. To show $A \to B$, first place $A$ as an assumption and derive $B$ under it. Once derived, enclose the assumption $A$ in brackets $[A]$ to discharge (close) it, and conclude $A \to B$. A discharged $A$ is no longer an open assumption.

At this point, assumptions are given a number ($[A]^1$ = "assumption $A$, number 1"). The discharging rule writes that number alongside the rule name as $(\to\text{I}, 1)$. This makes it unambiguous "which assumption this $\to$I closed." The superscript $1$ of $[A]^1$ and the $1$ of $(\to\text{I}, 1)$ are labels pointing to the same assumption (not different numbers). It is a device to avoid confusion when there are several assumptions.

This number is a formal annotation, information required by $\to$I (which assumption was discharged), not a free comment. Conversely, rules that do not discharge assumptions — $(\to\text{E})$, $(\land\text{I})$, $(\land\text{E})$, $(\lor\text{I})$ — are complete with just the rule name, with no number after it.

Deriving A→C from A→B and B→C [A]¹ A→B (→E) B B→C (→E) C (→I, 1) A→C
Figure 1: A hypothetical-syllogism proof tree. Premises placed side by side above a line (e.g., $[A]$ and $A\to B$) mean "both are used," not a comma or $\land$. The assumption $A$, tagged 1, is used, and finally discharged by $\to$I to conclude $A \to C$ (after discharge, $A$ does not remain as an open assumption).
Read Figure 1's proof tree as text
  1. Apply $\to$-elimination ($\to$E) to the assumption $[A]^1$ and the premise $A \to B$ to obtain $B$.
  2. Apply $\to$-elimination ($\to$E) to that $B$ and the premise $B \to C$ to obtain $C$.
  3. Apply $\to$-introduction ($\to$I, 1), which discharges the assumption $[A]^1$, to conclude $A \to C$.

This operation of placing an assumption and finally closing it coincides exactly, under the Curry–Howard correspondence, with the operation of building a function (lambda abstraction). Assuming $A$, building $B$, and concluding $A \to B$ is the same as defining a function that takes an argument of type $A$ and returns a value of type $B$.

4. The propositional layer of a proof-checking kernel

Natural deduction is not just a paper tool. The propositional layer of proof assistants and proof-checking kernels is precisely an implementation of these introduction and elimination rules. Each rule's correct application is decided just by matching "do the premises have the right shape?", so it can be checked mechanically (What a Proof Is).

Adding the introduction and elimination rules for the quantifiers $\forall, \exists$ to the connectives gives natural deduction for predicate logic. The guarantee that these rules "permit only correct inference" is the next chapter's soundness.

Summary

Key points

  • Natural deduction: give each connective a pair of an introduction rule (create) and an elimination rule (use)
  • Introduction and elimination are balanced; the operation removing "build then immediately use" waste is reduction
  • Discharging an assumption: assume $A$, derive $B$, close it with $\to$I to get $A \to B$
  • Discharge corresponds to lambda abstraction (building a function) (Curry–Howard)
  • Natural deduction is the propositional layer of a proof-checking kernel

Frequently asked questions

What is natural deduction?

A proof system that gives each connective a pair of rules: an introduction rule (which creates the connective) and an elimination rule (which uses it). Organized by Gentzen and Prawitz, it lets you build proofs close to a mathematician's natural reasoning. A proof is a proof tree built by stacking rule applications.

How do introduction and elimination rules differ?

An introduction rule produces a connective in the conclusion (from $A$ and $B$, infer $A \land B$); an elimination rule uses a connective as a premise (from $A \land B$, infer $A$). For each connective the two are balanced: building something and immediately using it returns to the start (it can be simplified).

What does discharging an assumption mean?

When introducing $A \to B$, you assume $A$, derive $B$, and then close (discharge) the assumption $A$. Once discharged, $A$ is no longer open, and $A \to B$ holds without it. This corresponds to introducing an assumption in a proof assistant and finally closing it with a lambda abstraction.