2
$\begingroup$

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?

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

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.

$\endgroup$

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).

Would you like to answer one of these unanswered questions instead?

Not the answer you're looking for? Browse other questions tagged or ask your own question.