Version without JavaScript, read-only: workshops, quizzes and running code are not available here. Full version · Catalogue · Sign in

Lecture notes · chapter 6

Natural deduction

Proving a formula through a sequence of small steps, each justified by a rule, the way one reasons by hand, and why these proofs tell the truth.

Proving rather than computing

So far, to know whether $\Sigma \vDash A$, we compute: truth tables, search for a countermodel, resolution. These methods give an answer, but they do not look like reasoning. Natural deduction (Gentzen, 1934) writes proofs: sequences of elementary steps, each justified by a rule, which look like what one would write in a mathematics exam.

We write $\Sigma \vdash A$, read “$A$ is provable from $\Sigma$”, if there is a proof of $A$ that uses only the hypotheses of $\Sigma$.

Two symbols, two notions:

  • $\Sigma \vDash A$ is about truth: every model of $\Sigma$ is a model of $A$;
  • $\Sigma \vdash A$ is about proof: we can write a proof.

The theorem at the end of the chapter says that they coincide.

The rules

Each connective has two kinds of rules: an introduction rule ($i$), which says how to prove a formula whose main connective it is, and an elimination rule ($e$), which says how to use such a formula. Above the line, what must have been established; below it, what we derive from it.

Conjunction

$$\frac{A \qquad B}{A \land B}\;(\land_i) \qquad\qquad \frac{A \land B}{A}\;(\land_{e1}) \qquad \frac{A \land B}{B}\;(\land_{e2})$$

Implication

$$\frac{\begin{matrix}[A] \\ \vdots \\ B\end{matrix}}{A \to B}\;(\to_i) \qquad\qquad \frac{A \to B \qquad A}{B}\;(\to_e)$$

To prove $A \to B$, we assume $A$, and prove $B$ under this assumption. Once $A \to B$ is obtained, the assumption $A$ is discharged: it can no longer be used. This is exactly “suppose $A$; …; hence $B$; thus $A \to B$”. The elimination is modus ponens.

Disjunction

$$\frac{A}{A \lor B}\;(\lor_{i1}) \qquad \frac{B}{A \lor B}\;(\lor_{i2}) \qquad\qquad \frac{A \lor B \qquad \begin{matrix}[A] \\ \vdots \\ C\end{matrix} \qquad \begin{matrix}[B] \\ \vdots \\ C\end{matrix}}{C}\;(\lor_e)$$

The elimination is reasoning by cases: if $A$ or $B$, and $C$ follows from each of the two cases, then $C$.

Negation and absurdity

We treat $\lnot A$ as “$A$ leads to a contradiction”, written $\bot$.

$$\frac{\begin{matrix}[A] \\ \vdots \\ \bot\end{matrix}}{\lnot A}\;(\lnot_i) \qquad \frac{A \qquad \lnot A}{\bot}\;(\lnot_e) \qquad \frac{\bot}{A}\;(\bot_e) \qquad \frac{\begin{matrix}[\lnot A] \\ \vdots \\ \bot\end{matrix}}{A}\;(\text{RAA})$$

$(\bot_e)$ says that from a contradiction, anything follows. $(\text{RAA})$ is proof by contradiction (reductio ad absurdum): to prove $A$, assume $\lnot A$ and reach a contradiction. It is what makes the logic classical; without it, $p \lor \lnot p$ cannot be proved.

The equivalence $A \leftrightarrow B$ is an abbreviation of $(A \to B) \land (B \to A)$.

Writing a proof

We write the proof as a numbered list, Fitch-style. A temporary assumption opens a box, marked by a vertical bar; the rule that discharges it closes the box. A line can be used only as long as we have not left its box. Inside a box, we may copy a line from an outer box that is still open: this is reiteration.

Proof and truth

Theorem. For every set of formulas $\Sigma$ and every formula $A$:

  • soundness: if $\Sigma \vdash A$, then $\Sigma \vDash A$;
  • completeness: if $\Sigma \vDash A$, then $\Sigma \vdash A$.

Soundness is proved rule by rule: each one, applied to formulas true in an interpretation, produces a formula true in that interpretation (taking discharged assumptions into account). For instance, for $(\to_e)$: if $A \to B$ and $A$ are true in $v$, then so is $B$. Completeness is harder, and admitted.

Consequence: to show that a formula is not provable, a countermodel is enough. We will never prove $p \to q$ without hypotheses, since $p = 1, q = 0$ makes it false.