View source for Derivation rule

A method for generating objects, called conclusions of the derivation rule, from a set of objects called the premises of the rule; the formulation of a derivation rule plays a determining role in describing calculi (cf. [[Calculus|Calculus]]) (a given derivation rule is often meaningful only in the context of a specific calculus). For calculi with [[Semantics|semantics]] (in particular, in most logico-mathematical calculi, cf. [[Logico-mathematical calculus|Logico-mathematical calculus]]) a derivation rule preserves truth, i.e. true premises permit true conclusions only; the most prominent example of such a derivation rule is the rule of [[Modus ponens|modus ponens]]. In most calculi being studied, a derivation rule has only a finite number of premises (the most important exception is the [[Carnap rule|Carnap rule]]). As a rule, the number of premises of a given derivation rule remains unchanged in all its applications. The number of possible applications of a given rule, however, is in principle unlimited.

The methods of formulation of a derivation rule are extremely varied; they depend on the language of the calculus and may include variables of different types. The great majority of derivation rules may be generated according to the following general scheme: After an alphabet $A$ not containing the letter $\bullet$ and a natural number $l$ have been selected, a derivation rule with $l$-premises is defined as some [[Algorithm|algorithm]] $\mathfrak{A}$ over the alphabet $A \cup \{\bullet\}$. If $\mathfrak{A}$ is applicable to the word $P_0 \bullet \cdots \bullet P_l$, where $P_0,\ldots,P_l$ are words over $A$, while the symbol $\bullet$ serves as the comma, then $P_1,\ldots,P_l$ are regarded as the premises, while $P_0$ is regarded as the conclusion of some specific application of the derivation rule. A special case of such derivation rules are derivation rules without premises (or axiom schemes, cf. [[Axiom scheme|Axiom scheme]]). In any calculus containing only such rules, the set of deducible words is countable. A derivation rule often satisfies a more rigorous requirement as well: It is possible to tell, with the aid of algorithms, whether $P_0$ is deducible from $P_1,\ldots,P_l$ by one application of the rule.



====Comments====
Often, instead of  "derivation rule"  one simply uses the word  "rule" . Modus ponens, e.g., is sometimes referred to as the rule of detachment.

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  A. Grzegorczyk,   "An outline of mathematical logic" , Reidel  (1974)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  J.B. Rosser,   "Logic for mathematicians" , McGraw-Hill  (1953)</TD></TR></table>

{{TEX|done}}

[[Category:Logic and foundations]]