Namespaces
Variants
Actions

Difference between revisions of "Deduction theorem"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
 
Line 1: Line 1:
A general term for a number of theorems which allow one to establish that the implication <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d0305901.png" /> can be proved if it is possible to deduce logically formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d0305902.png" /> from formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d0305903.png" />. In the simplest case of classical, intuitionistic, etc., propositional calculus, a deduction theorem states the following: If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d0305904.png" /> (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d0305905.png" /> is deducible from the assumptions <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d0305906.png" />), then
+
<!--
 +
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.
 +
-->
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d0305907.png" /></td> <td valign="top" style="width:5%;text-align:right;">(*)</td></tr></table>
+
{{TEX|auto}}
 +
{{TEX|done}}
  
(<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d0305908.png" /> may be empty). In the presence of quantifiers an analogous statement is false:
+
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
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d0305909.png" /></td> </tr></table>
+
$$ \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
 
but not
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059010.png" /></td> </tr></table>
+
$$
 +
\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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059011.png" />, then
+
One of the formulations of a deduction theorem for traditional (classical, intuitionistic, etc.) predicate calculus is: If $  \Gamma , A \vdash B $,
 +
then
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059012.png" /></td> </tr></table>
+
$$
 +
\Gamma  \vdash  ( \forall A \supset B ) ,
 +
$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059013.png" /> is the result of prefixing <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059014.png" /> quantifiers (cf. [[Quantifier|Quantifier]]) over all the free variables of the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059015.png" />. In particular, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059016.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059017.png" /> is deducible from axioms <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059018.png" /> if and only if the formula
+
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
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059019.png" /></td> </tr></table>
+
$$
 +
\forall A _ {1}  \supset  ( \forall A _ {2}  \supset \dots \supset  ( \forall A _ {n}  \supset
 +
B ) \dots )
 +
$$
  
 
is deducible in predicate calculus.
 
is deducible in predicate calculus.
Line 23: Line 60:
 
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]]):
 
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]]):
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059020.png" /></td> </tr></table>
+
$$
 +
\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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059021.png" />-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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059022.png" /> is varied for a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059023.png" /> in a given deduction if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059024.png" /> is free in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059025.png" /> and if the deduction under consideration involves an application of the rule of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059026.png" />-introduction into the conclusion of an implication (or the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059027.png" />-introduction into a premise), in which the quantifier over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059028.png" /> is introduced, and the premise of the application depends on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059029.png" /> in the proof under consideration. A deduction theorem for traditional predicate calculus may now be rendered more precise as follows:
+
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:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059030.png" /></td> </tr></table>
+
$$
 +
\textrm{ If }  \Gamma , A  \vdash  B,\  \textrm{ then } \
 +
\Gamma  \vdash  ( \forall y _ {1} \dots y _ {n} A  \supset  B ) ,
 +
$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059031.png" /> is the complete list of variables varied for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059032.png" /> in the deduction under consideration. In particular, if no free variable in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059033.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059034.png" /> into the conclusion of the implication and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059035.png" /> into the premise.
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059036.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059037.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059038.png" /> to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059039.png" />, formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059040.png" /> is varied, since it does not form part of the second member of the pair.
+
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, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059041.png" /> is not varied, a deduction theorem assumes the form (*), and if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059042.png" /> is varied it takes the following form:
+
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:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059043.png" /></td> </tr></table>
+
$$
 +
\textrm{ If }  A, \Gamma  \vdash  B,\  \textrm{ then } \
 +
\Gamma  \vdash  (( A \& t )  \supset  B ) ,
 +
$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059044.png" /> is a  "true"  constant (or the conjunction of the formulas <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059045.png" /> for all propositional variables <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059046.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059047.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059048.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/d/d030/d030590/d03059049.png" />).
+
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====
 
====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>
 
<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====
 
====Comments====
 
  
 
====References====
 
====References====
 
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  A. Grzegorczyk,  "An outline of mathematical logic" , Reidel  (1974)</TD></TR></table>
 
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  A. Grzegorczyk,  "An outline of mathematical logic" , Reidel  (1974)</TD></TR></table>

Latest revision as of 17:32, 5 June 2020


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)

Comments

References

[a1] A. Grzegorczyk, "An outline of mathematical logic" , Reidel (1974)
How to Cite This Entry:
Deduction theorem. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Deduction_theorem&oldid=17084
This article was adapted from an original article by G.E. Mints (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article