Deducible rule

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.