Deduction theorem
A general term for a number of theorems which allow one to establish that the implication can be proved if it is possible to deduce logically formula
from formula
. In the simplest case of classical, intuitionistic, etc., propositional calculus, a deduction theorem states the following: If
(
is deducible from the assumptions
), then
![]() | (*) |
( may be empty). In the presence of quantifiers an analogous statement is false:
![]() |
but not
![]() |
One of the formulations of a deduction theorem for traditional (classical, intuitionistic, etc.) predicate calculus is: If , then
![]() |
where is the result of prefixing
quantifiers (cf. Quantifier) over all the free variables of the formula
. In particular, if
is a closed formula, a deduction theorem assumes the form (*). This formulation of a deduction theorem makes it possible to reduce proof search in axiomatic theories to proof search in predicate calculus: Formula
is deducible from axioms
if and only if the formula
![]() |
is deducible in predicate calculus.
A deduction theorem is formulated in a similar manner for logics with operations "resembling" quantifiers. Thus, a deduction theorem has the following form for the modal logics S4 and S5 (cf. Modal logic):
![]() |
More precise formulations of deduction theorems are obtained if one introduces -quantifiers not over all the free variables, but only over those bounded by quantifiers in the course of the deduction. One says that a variable
is varied for a formula
in a given deduction if
is free in
and if the deduction under consideration involves an application of the rule of
-introduction into the conclusion of an implication (or the
-introduction into a premise), in which the quantifier over
is introduced, and the premise of the application depends on
in the proof under consideration. A deduction theorem for traditional predicate calculus may now be rendered more precise as follows:
![]() |
where is the complete list of variables varied for
in the deduction under consideration. In particular, if no free variable in
is varied, a deduction theorem assumes the form (*). In formulating the appropriate refinements of a deduction theorem for modal logics it should be borne in mind that the variation takes place in the rules for the introduction of
into the conclusion of the implication and
into the premise.
In establishing a deduction theorem for the calculus of relevant implication (i.e. for systems adapted to the interpretation of as "B is deducible with essential use of assumption A" ) one has the alternative of modifying the concept of the deduction itself or else of assuming that the variation takes place in any use of a "secondary" assumption; for instance, on passing from the pair
,
to
, formula
is varied, since it does not form part of the second member of the pair.
If, in a given deduction, is not varied, a deduction theorem assumes the form (*), and if
is varied it takes the following form:
![]() |
where is a "true" constant (or the conjunction of the formulas
for all propositional variables
in
,
,
).
References
[1] | S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951) |
[2] | H.B. Curry, "Foundations of mathematical logic" , McGraw-Hill (1963) |
Comments
References
[a1] | A. Grzegorczyk, "An outline of mathematical logic" , Reidel (1974) |
Deduction theorem. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Deduction_theorem&oldid=46599