Namespaces
Variants
Actions

Difference between revisions of "Derivation rule"

From Encyclopedia of Mathematics
Jump to: navigation, search
m (link removed)
(Category:Logic and foundations)
 
(One intermediate revision by the same user not shown)
Line 1: Line 1:
 
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.
 
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d0312301.png" /> not containing the letter <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d0312302.png" /> and a natural number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d0312303.png" /> have been selected, a derivation rule with <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d0312305.png" />-premises is defined as some [[Algorithm|algorithm]] <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d0312306.png" /> over the alphabet <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d0312307.png" />. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d0312308.png" /> is applicable to the word <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d0312309.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d03123010.png" /> are words over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d03123011.png" />, while the symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d03123012.png" /> serves as the comma, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d03123013.png" /> are regarded as the premises, while <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d03123014.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d03123015.png" /> is deducible from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d031/d031230/d03123016.png" /> by one application of the rule.
+
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.
  
  
Line 10: Line 10:
 
====References====
 
====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>
 
<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]]

Latest revision as of 19:19, 17 October 2014

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) (a given derivation rule is often meaningful only in the context of a specific calculus). For calculi with semantics (in particular, in most logico-mathematical calculi, cf. 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. In most calculi being studied, a derivation rule has only a finite number of premises (the most important exception is the 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 $\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). 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

[a1] A. Grzegorczyk, "An outline of mathematical logic" , Reidel (1974)
[a2] J.B. Rosser, "Logic for mathematicians" , McGraw-Hill (1953)
How to Cite This Entry:
Derivation rule. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Derivation_rule&oldid=29779
This article was adapted from an original article by S.Yu. Maslov (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article