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