View source for Deduction theorem

<!--
d0305901.png
$#A+1 = 49 n = 0
$#C+1 = 49 : ~/encyclopedia/old_files/data/D030/D.0300590 Deduction theorem
Automatically converted into TeX, above some diagnostics.
Please remove this comment and the {{TEX|auto}} line below,
if TeX found to be correct.
-->

{{TEX|auto}}
{{TEX|done}}

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|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|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====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  S.C. Kleene,   "Introduction to metamathematics" , North-Holland  (1951)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  H.B. Curry,   "Foundations of mathematical logic" , McGraw-Hill  (1963)</TD></TR></table>

====Comments====

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  A. Grzegorczyk,   "An outline of mathematical logic" , Reidel  (1974)</TD></TR></table>