# Is a derivation a proof?

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?

• In my experience, "derivation" is a special kind of proof, of an equation or similarly succinct statement. – vadim123 Mar 9 '15 at 4:25
• To me, derivation might be a synonym for en.wikipedia.org/wiki/Constructive_proof – parsiad Mar 9 '15 at 4:27
• A good answer would require you to specify exactly what you mean by "proof" and "derivation." – Daniel W. Farlow Mar 9 '15 at 4:29

See for example :

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 :

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.

## protected by Community♦Mar 10 '17 at 8:32

Thank you for your interest in this question. Because it has attracted low-quality or spam answers that had to be removed, posting an answer now requires 10 reputation on this site (the association bonus does not count).