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)

References

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