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