Is a derivation a proof?

Question

Is there a difference between "derivation" and "proof"? I imagine a derivation is a type of proof but that proofs are perhaps more general. Although then again, I suppose every proof should be derivable from some axioms, so perhaps there is no difference?

Answer 1

See for example :

• Richard Kaye, The Mathematics of Logic : A guide to completeness theorems and their applications (2007), page 24-25 :

Formal systems are kinds of mathematical games with strings of symbols and precise rules. They mimic the idea of a ‘proof’.

Definition 3.1 Let [$\Sigma$ a set of strings and $\tau$ a string]. We write $\Sigma \vdash \tau$ to mean that it is possible to write down $\tau$ in a finite number of steps that follow the rules of the game for $\Sigma$.

If $\Sigma \vdash \tau$ then there is a list of strings that can be written down in the game, each of which is written down according to one of the [...] rules, the last one in the list being $\tau$. Sometimes this list of strings is called a formal proof or formal derivation of $\tau$ from strings in $\Sigma$ following the rules given.

Thus $\Sigma \vdash \tau$ can be expressed as saying ‘there is a formal proof of $\tau$ from strings in $\Sigma$’.

---

In other books, you can find "deduction" used with the same meaning; see :

• Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 111 :

DEFINITION. A deduction of $\varphi$ from $\Gamma$ is a finite sequence $\langle α_0,\ldots,α_n \rangle$ of formulas such that $α_n$ is $\varphi$ and for each $k ≤ n$, either

(a) $α_k$ is in $\Gamma \cup \Lambda$ [where $\Lambda$ is the set of logical axioms], or

(b) $α_k$ is obtained by modus ponens [the rule of inference of the calculus, or proof system] from two earlier formulas in the sequence; that is, for some $i,j < k$, $α_j$ is $α_i \to α_k$.

If such a deduction exists, we say that $\varphi$ is deducible from $\Gamma$, or that $\varphi$ is a theorem of $\Gamma$, and we write $\Gamma \vdash \varphi$.

---

In conclusion, a derivation is a "formalized" proof, i.e. it is the "formal counterpart" of a mathematical proof according to the language and rules of a formal system.