View source for Derived rule

''of a derivation in a given calculus''

A [[Derivation rule|derivation rule]] whose conclusion is derivable from its premises in the calculus under consideration. For example, in [[Propositional calculus|propositional calculus]] the derivation rule

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031300/d0313001.png" /></td> </tr></table>

is a derived rule, since in this calculus there is derivability from the premises:

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031300/d0313002.png" /></td> </tr></table>

Every derived rule is a [[Sound rule|sound rule]], but not every sound rule is a derived rule. For example, the [[Substitution rule|substitution rule]] in propositional calculus is a sound but not a derived rule.

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  S.C. Kleene,   "Introduction to metamathematics" , North-Holland  (1951)</TD></TR></table>