Namespaces
Variants
Actions

Deducible rule

From Encyclopedia of Mathematics
Jump to: navigation, search

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://www.encyclopediaofmath.org/index.php?title=Deducible_rule&oldid=33739
This article was adapted from an original article by S.Yu. Maslov (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article