Namespaces
Variants
Actions

Difference between revisions of "Deducible rule"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
(TeX)
Line 1: Line 1:
A meta-mathematical theorem (cf. [[Meta-theorem|Meta-theorem]]) from which it is allowed by the use of a finite number of derivations (cf. [[Derivation, logical|Derivation, logical]]) from hypotheses <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030580/d0305801.png" /> (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030580/d0305802.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030580/d0305803.png" />) to show that a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030580/d0305804.png" /> is derivable from the hypotheses <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030580/d0305805.png" />; the derivations <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030580/d0305806.png" /> are called auxiliary derivations of the deducible rule, while the conclusion <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030580/d0305807.png" /> is called the resulting derivation. A deducible rule is a special case of a [[Sound rule|sound rule]]. The most important examples of deducible rules are the [[Deduction theorem|deduction theorem]], the rule of [[Reductio ad absurdum|reductio ad absurdum]], and other rules governing the introduction and elimination of logical symbols, such as the rules for the introduction of the disjunction: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030580/d0305808.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030580/d0305809.png" /> (for these deducible rules the number of auxiliary derivations is zero), and of elimination of disjunction: from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030580/d03058010.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030580/d03058011.png" /> follows that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030580/d03058012.png" />. In a number of cases, deducible rules have the following structure: A calculus is extended and strengthened, and the deducibility in the new calculus implies certain consequences regarding the deducibility in the basic calculus. Such deducible rules arise, in particular, in the elimination of descriptive definitions (definitions modelling the extensions of concepts and notations in constructing a mathematical theory). The available apparatus of deducible rules serves to bring the conversion methods with formal conclusions much nearer to specific mathematical reasoning.
+
{{TEX|done}}
 +
A meta-mathematical theorem (cf. [[Meta-theorem|Meta-theorem]]) from which it is allowed by the use of a finite number of derivations (cf. [[Derivation, logical|Derivation, logical]]) from hypotheses $\Gamma_i\vdash\Delta_i$ ($1\leq i\leq n$, $n\geq0$) to show that a formula $\Delta$ is derivable from the hypotheses $\Gamma$; the derivations $\Gamma_i\vdash\Delta_i$ are called auxiliary derivations of the deducible rule, while the conclusion $\Gamma\vdash\Delta$ is called the resulting derivation. A deducible rule is a special case of a [[Sound rule|sound rule]]. The most important examples of deducible rules are the [[Deduction theorem|deduction theorem]], the rule of [[Reductio ad absurdum|reductio ad absurdum]], and other rules governing the introduction and elimination of logical symbols, such as the rules for the introduction of the disjunction: $A\vdash A\lor B$ and $B\vdash A\lor B$ (for these deducible rules the number of auxiliary derivations is zero), and of elimination of disjunction: from $\Gamma,A\vdash C$ and $\Gamma,B\vdash C$ follows that $\Gamma,A\lor B\vdash C$. In a number of cases, deducible rules have the following structure: A calculus is extended and strengthened, and the deducibility in the new calculus implies certain consequences regarding the deducibility in the basic calculus. Such deducible rules arise, in particular, in the elimination of descriptive definitions (definitions modelling the extensions of concepts and notations in constructing a mathematical theory). The available apparatus of deducible rules serves to bring the conversion methods with formal conclusions much nearer to specific mathematical reasoning.
  
  

Revision as of 15:17, 9 April 2014

A meta-mathematical theorem (cf. Meta-theorem) from which it is allowed by the use of a finite number of derivations (cf. Derivation, logical) from hypotheses $\Gamma_i\vdash\Delta_i$ ($1\leq i\leq n$, $n\geq0$) to show that a formula $\Delta$ is derivable from the hypotheses $\Gamma$; the derivations $\Gamma_i\vdash\Delta_i$ are called auxiliary derivations of the deducible rule, while the conclusion $\Gamma\vdash\Delta$ is called the resulting derivation. A deducible rule is a special case of a sound rule. The most important examples of deducible rules are the deduction theorem, the rule of reductio ad absurdum, and other rules governing the introduction and elimination of logical symbols, such as the rules for the introduction of the disjunction: $A\vdash A\lor B$ and $B\vdash A\lor B$ (for these deducible rules the number of auxiliary derivations is zero), and of elimination of disjunction: from $\Gamma,A\vdash C$ and $\Gamma,B\vdash C$ follows that $\Gamma,A\lor B\vdash C$. In a number of cases, deducible rules have the following structure: A calculus is extended and strengthened, and the deducibility in the new calculus implies certain consequences regarding the deducibility in the basic calculus. Such deducible rules arise, in particular, in the elimination of descriptive definitions (definitions modelling the extensions of concepts and notations in constructing a mathematical theory). The available apparatus of deducible rules serves to bring the conversion methods with formal conclusions much nearer to specific mathematical reasoning.


Comments

Such rules are also called derived rules, cf. Derived rule; Derivable rule.

How to Cite This Entry:
Deducible rule. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Deducible_rule&oldid=17186
This article was adapted from an original article by S.Yu. Maslov (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article