Deduction theorem

A general term for a number of theorems which allow one to establish that the implication $ A \supset B $ can be proved if it is possible to deduce logically formula $ B $ from formula $ A $. In the simplest case of classical, intuitionistic, etc., propositional calculus, a deduction theorem states the following: If $ \Gamma , A \vdash B $( $ B $ is deducible from the assumptions $ \Gamma , A $), then

$$ \tag{* } \Gamma \vdash ( A \supset B ) $$

( $ \Gamma $ may be empty). In the presence of quantifiers an analogous statement is false:

$$ A ( x) \vdash \forall x A ( x) , $$

but not

$$ \vdash A ( x) \supset \forall x A ( x) . $$

One of the formulations of a deduction theorem for traditional (classical, intuitionistic, etc.) predicate calculus is: If $ \Gamma , A \vdash B $, then

$$ \Gamma \vdash ( \forall A \supset B ) , $$

where $ \forall A $ is the result of prefixing $ \forall $ quantifiers (cf. Quantifier) over all the free variables of the formula $ A $. In particular, if $ A $ 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 $ B $ is deducible from axioms $ A _ {1} \dots A _ {n} $ if and only if the formula

$$ \forall A _ {1} \supset ( \forall A _ {2} \supset \dots \supset ( \forall A _ {n} \supset B ) \dots ) $$

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):

$$ \textrm{ If } \Gamma , A \vdash B,\ \textrm{ then } \ \Gamma \vdash ( \square A \supset B ) . $$

More precise formulations of deduction theorems are obtained if one introduces $ \forall $- 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 $ y $ is varied for a formula $ A $ in a given deduction if $ y $ is free in $ A $ and if the deduction under consideration involves an application of the rule of $ \forall $- introduction into the conclusion of an implication (or the $ \exists $- introduction into a premise), in which the quantifier over $ y $ is introduced, and the premise of the application depends on $ A $ in the proof under consideration. A deduction theorem for traditional predicate calculus may now be rendered more precise as follows:

$$ \textrm{ If } \Gamma , A \vdash B,\ \textrm{ then } \ \Gamma \vdash ( \forall y _ {1} \dots y _ {n} A \supset B ) , $$

where $ y _ {1} \dots y _ {n} $ is the complete list of variables varied for $ A $ in the deduction under consideration. In particular, if no free variable in $ A $ 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 $ \square $ into the conclusion of the implication and $ \dia $ into the premise.

In establishing a deduction theorem for the calculus of relevant implication (i.e. for systems adapted to the interpretation of $ A \supset B $ 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 $ A , \Gamma \vdash C $, $ \Gamma \vdash D $ to $ A , \Gamma \vdash ( C \& D) $, formula $ A $ is varied, since it does not form part of the second member of the pair.

If, in a given deduction, $ A $ is not varied, a deduction theorem assumes the form (*), and if $ A $ is varied it takes the following form:

$$ \textrm{ If } A, \Gamma \vdash B,\ \textrm{ then } \ \Gamma \vdash (( A \& t ) \supset B ) , $$

where $ t $ is a "true" constant (or the conjunction of the formulas $ ( p \supset p) $ for all propositional variables $ p $ in $ A $, $ \Gamma $, $ B $).

References

[1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[2]	H.B. Curry, "Foundations of mathematical logic" , McGraw-Hill (1963)

References

[a1]	A. Grzegorczyk, "An outline of mathematical logic" , Reidel (1974)