A **deduction** from a set is a sequence of well-formed formulas with each element being justified as a tautology or the result of a rule of inference. A deduction from the empty set is a proof.

## Formal definitionEdit

Let be a formal system and let be it's underlying formal language and let

Then a deduction of from is a sequence of well-formed formulas such that one of the following holds for :

- is justified by a rule of inference of .

A deduction of from is a proof if and only if .