Deduction theorem
Encyclopedia
In mathematical logic
, the deduction theorem is a metatheorem
of first-order logic
. It is a formalization of the common proof technique in which an implication A → B is proved by assuming A and then proving B from this assumption. The deduction theorem explains why proofs of conditional sentences in mathematics are logically correct. Though it has seemed "obvious" to mathematicians literally for centuries that proving B from A conjoined with a set of theorems is sufficient to proving the implication A → B based on those theorems alone, it was left to Herbrand and Tarski to show (independently) this was logically correct in the general case—another instance, perhaps, of modern logic "cleaning up" mathematical practice.
The deduction theorem states that if a formula B is deducible from a set of assumptions
, where A is a closed formula, then the implication A → B is deducible from 
In symbols, 
implies
. In the special case where 
is the empty set
, the deduction theorem shows that
implies 
The deduction theorem holds for all first-order theories with the usual deductive systems for first-order logic. However, there are first-order systems in which new inference rules are added for which the deduction theorem fails.
The deduction rule is an important property of Hilbert-style systems because the use of this metatheorem leads to much shorter proofs than would be possible without it. Although the deduction theorem could be taken as primitive rule of inference in such systems, this approach is not generally followed; instead, the deduction theorem is obtained as an admissible rule
using the other logical axioms and modus ponens
. In other formal proof systems, the deduction theorem is sometimes taken as a primitive rule of inference
. For example, in natural deduction
, the deduction theorem is recast as an introduction rule for "→".
"Prove" axiom 2:
Using axiom 1 to show ((P→(Q→P))→R)→R:
1. Hypothesis is a step where one adds an additional premise to those already available. So, if your previous step S was deduced as:
then one adds another premise H and gets:
This is symbolized by moving from the n-th level of indentation to the n+1-th level and saying
2. Reiteration is a step where one re-uses a previous step. In practice, this is only necessary when one wants to take a hypothesis which is not the most recent hypothesis and use it as the final step before a deduction step.
3. Deduction is a step where one removes the most recent hypothesis (still available) and prefixes it to the previous step. This is shown by unindenting one level as follows:
These axiom schemas are chosen to enable one to derive the deduction theorem from them easily. So it might seem that we are begging the question. However, they can be justified by checking that they are tautologies
using truth tables and that modus ponens preserves truth.
From these axiom schemas one can quickly deduce the theorem schema P→P (reflexivity of implication) which is used below:
Suppose that we have that Γ and H prove C, and we wish to show that Γ proves H→C. For each step S in the deduction which is a premise in Γ (a reiteration step) or an axiom, we can apply modus ponens to the axiom 1, S→(H→S), to get H→S. If the step is H itself (a hypothesis step), we apply the theorem schema to get H→H. If the step is the result of applying modus ponens to A and A→S, we first make sure that these have been converted to H→A and H→(A→S) and then we take the axiom 2, (H→(A→S))→((H→A)→(H→S)), and apply modus ponens to get (H→A)→(H→S) and then again to get H→S. At the end of the proof we will have H→C as required, except that now it only depends on Γ, not on H. So the deduction step will disappear, consolidated into the previous step which was the conclusion derived from H.
To minimize the complexity of the resulting proof, some preprocessing should be done before the conversion. Any steps (other than the conclusion) which do not actually depend on H should be moved up before the hypothesis step and unindented one level. And any other unnecessary steps (which are not used to get the conclusion or can be bypassed), such as reiterations which are not the conclusion, should be eliminated.
During the conversion, it may be useful to put all the applications of modus ponens to axiom 1 at the beginning of the deduction (right after the H→H step).
When converting a modus ponens, if A is outside the scope of H, then it will be necessary to apply axiom 1, A→(H→A), and modus ponens to get H→A. Similarly, if A→S is outside the scope of H, apply axiom 1, (A→S)→(H→(A→S)), and modus ponens to get H→(A→S). It should not be necessary to do both of these, unless the modus ponens step is the conclusion, because if both are outside the scope, then the modus ponens should have been moved up before H and thus be outside the scope also.
Under the Curry–Howard correspondence, the above conversion process for the deduction meta-theorem is analogous to the conversion process from lambda calculus
terms to terms of combinatory logic
, where axiom 1 corresponds to the K combinator, and axiom 2 corresponds to the S combinator. Note that the I combinator corresponds to the theorem schema P→P.
in the following form:
Here, the symbol ├ means "is a syntactical consequence of." We indicate below how the proof of this deduction theorem differs from that of the deduction theorem in propositional calculus.
In the most common versions of the notion of formal proof, there are, in addition to the axiom schemes
of propositional calculus (or the understanding that all tautologies of propositional calculus are to
be taken as axiom schemes in their own right), quantifier axioms, and in addition to modus ponens
, one additional rule of inference
, known as the rule of generalization
: "From K, infer ∀vK."
In order to convert a proof of G from T∪{F} to one of F→G from T, one deals
with steps of the proof of G which are axioms or result from application of modus ponens in the
same way as for proofs in propositional logic. Steps which result from application of the rule of
generalization are dealt with via the following quantifier axiom (valid whenever the variable
v is not free in formula H):
Since in our case F is assumed to be closed, we can take H to be F. This axiom allows
one to deduce F→∀vK from F→K, which is just what is needed whenever
the rule of generalization is applied to some K in the proof of G.
First, we write a proof using a natural-deduction like method:
Second, we convert the inner deduction to an axiomatic proof:
Third, we convert the outer deduction to an axiomatic proof:
These three steps can be stated succinctly using the Curry–Howard correspondence:
. However, the following "two-way deduction theorem" does hold in one form of paraconsistent logic:
that requires the contrapositive inference to hold in addition to the requirement of the classical deduction theorem.
which is the elimination rule for implication.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, the deduction theorem is a metatheorem
Metatheorem
In logic, a metatheorem is a statement about a formal system proven in a metalanguage. Unlike theorems proved within a given formal system, a metatheorem is proved within a metatheory, and may reference concepts that are present in the metatheory but not the object theory.- Discussion :A formal...
of first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
. It is a formalization of the common proof technique in which an implication A → B is proved by assuming A and then proving B from this assumption. The deduction theorem explains why proofs of conditional sentences in mathematics are logically correct. Though it has seemed "obvious" to mathematicians literally for centuries that proving B from A conjoined with a set of theorems is sufficient to proving the implication A → B based on those theorems alone, it was left to Herbrand and Tarski to show (independently) this was logically correct in the general case—another instance, perhaps, of modern logic "cleaning up" mathematical practice.
The deduction theorem states that if a formula B is deducible from a set of assumptions
, where A is a closed formula, then the implication A → B is deducible from In symbols, implies
. In the special case where is the empty setEmpty set
In mathematics, and more specifically set theory, the empty set is the unique set having no elements; its size or cardinality is zero. Some axiomatic set theories assure that the empty set exists by including an axiom of empty set; in other theories, its existence can be deduced...
, the deduction theorem shows that
implies The deduction theorem holds for all first-order theories with the usual deductive systems for first-order logic. However, there are first-order systems in which new inference rules are added for which the deduction theorem fails.
The deduction rule is an important property of Hilbert-style systems because the use of this metatheorem leads to much shorter proofs than would be possible without it. Although the deduction theorem could be taken as primitive rule of inference in such systems, this approach is not generally followed; instead, the deduction theorem is obtained as an admissible rule
Admissible rule
In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense,...
using the other logical axioms and modus ponens
Modus ponens
In classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
. In other formal proof systems, the deduction theorem is sometimes taken as a primitive rule of inference
Rule of inference
In logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion...
. For example, in natural deduction
Natural deduction
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...
, the deduction theorem is recast as an introduction rule for "→".
Examples of deduction
"Prove" axiom 1:-
- P 1. hypothesis
- Q 2. hypothesis
- P 3. reiteration of 1
- Q→P 4. deduction from 2 to 3
- P 1. hypothesis
- P→(Q→P) 5. deduction from 1 to 4 QED
"Prove" axiom 2:
-
- P→(Q→R) 1. hypothesis
- P→Q 2. hypothesis
- P 3. hypothesis
- Q 4. modus ponens 3,2
- Q→R 5. modus ponens 3,1
- R 6. modus ponens 4,5
- P→R 7. deduction from 3 to 6
- P→Q 2. hypothesis
- (P→Q)→(P→R) 8. deduction from 2 to 7
- P→(Q→R) 1. hypothesis
- (P→(Q→R))→((P→Q)→(P→R)) 9. deduction from 1 to 8 QED
Using axiom 1 to show ((P→(Q→P))→R)→R:
-
- (P→(Q→P))→R 1. hypothesis
- P→(Q→P) 2. axiom 1
- R 3. modus ponens 2,1
- ((P→(Q→P))→R)→R 4. deduction from 1 to 3 QED
Virtual rules of inference
From the examples, you can see that we have added three virtual (or extra and temporary) rules of inference to our normal axiomatic logic. These are "hypothesis", "reiteration", and "deduction". The normal rules of inference (i.e. "modus ponens" and the various axioms) remain available.1. Hypothesis is a step where one adds an additional premise to those already available. So, if your previous step S was deduced as:
then one adds another premise H and gets:
This is symbolized by moving from the n-th level of indentation to the n+1-th level and saying
-
-
-
-
- S previous step
- H hypothesis
- S previous step
-
-
-
2. Reiteration is a step where one re-uses a previous step. In practice, this is only necessary when one wants to take a hypothesis which is not the most recent hypothesis and use it as the final step before a deduction step.
3. Deduction is a step where one removes the most recent hypothesis (still available) and prefixes it to the previous step. This is shown by unindenting one level as follows:
-
-
-
-
-
- H hypothesis
- ......... (other steps)
- C (conclusion drawn from H)
- H→C deduction
-
-
-
-
Conversion from proof using the deduction meta-theorem to axiomatic proof
In axiomatic versions of propositional logic, one usually has among the axiom schemas (where P, Q, and R are replaced by any propositions):- Axiom 1 is: P→(Q→P)
- Axiom 2 is: (P→(Q→R))→((P→Q)→(P→R))
- Modus ponens is: from P and P→Q infer Q
These axiom schemas are chosen to enable one to derive the deduction theorem from them easily. So it might seem that we are begging the question. However, they can be justified by checking that they are tautologies
Tautology (logic)
In logic, a tautology is a formula which is true in every possible interpretation. Philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921; it had been used earlier to refer to rhetorical tautologies, and continues to be used in that alternate sense...
using truth tables and that modus ponens preserves truth.
From these axiom schemas one can quickly deduce the theorem schema P→P (reflexivity of implication) which is used below:
- (P→((Q→P)→P))→((P→(Q→P))→(P→P)) from axiom schema 2 with P, (Q→P), P
- P→((Q→P)→P) from axiom schema 1 with P, (Q→P)
- (P→(Q→P))→(P→P) from modus ponens applied to step 2 and step 1
- P→(Q→P) from axiom schema 1 with P, Q
- P→P from modus ponens applied to step 4 and step 3
Suppose that we have that Γ and H prove C, and we wish to show that Γ proves H→C. For each step S in the deduction which is a premise in Γ (a reiteration step) or an axiom, we can apply modus ponens to the axiom 1, S→(H→S), to get H→S. If the step is H itself (a hypothesis step), we apply the theorem schema to get H→H. If the step is the result of applying modus ponens to A and A→S, we first make sure that these have been converted to H→A and H→(A→S) and then we take the axiom 2, (H→(A→S))→((H→A)→(H→S)), and apply modus ponens to get (H→A)→(H→S) and then again to get H→S. At the end of the proof we will have H→C as required, except that now it only depends on Γ, not on H. So the deduction step will disappear, consolidated into the previous step which was the conclusion derived from H.
To minimize the complexity of the resulting proof, some preprocessing should be done before the conversion. Any steps (other than the conclusion) which do not actually depend on H should be moved up before the hypothesis step and unindented one level. And any other unnecessary steps (which are not used to get the conclusion or can be bypassed), such as reiterations which are not the conclusion, should be eliminated.
During the conversion, it may be useful to put all the applications of modus ponens to axiom 1 at the beginning of the deduction (right after the H→H step).
When converting a modus ponens, if A is outside the scope of H, then it will be necessary to apply axiom 1, A→(H→A), and modus ponens to get H→A. Similarly, if A→S is outside the scope of H, apply axiom 1, (A→S)→(H→(A→S)), and modus ponens to get H→(A→S). It should not be necessary to do both of these, unless the modus ponens step is the conclusion, because if both are outside the scope, then the modus ponens should have been moved up before H and thus be outside the scope also.
Under the Curry–Howard correspondence, the above conversion process for the deduction meta-theorem is analogous to the conversion process from lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
terms to terms of combinatory logic
Combinatory logic
Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming...
, where axiom 1 corresponds to the K combinator, and axiom 2 corresponds to the S combinator. Note that the I combinator corresponds to the theorem schema P→P.
The deduction theorem in predicate logic
The deduction theorem is also valid in first-order logicFirst-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
in the following form:
- If T is a theoryTheory (mathematical logic)In mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...
and F, G are formulas with F closedSentence (mathematical logic)In mathematical logic, a sentence of a predicate logic is a boolean-valued well formed formula with no free variables. A sentence can be viewed as expressing a proposition, something that may be true or false...
, and T∪{F}├G, then T├F→G.
Here, the symbol ├ means "is a syntactical consequence of." We indicate below how the proof of this deduction theorem differs from that of the deduction theorem in propositional calculus.
In the most common versions of the notion of formal proof, there are, in addition to the axiom schemes
of propositional calculus (or the understanding that all tautologies of propositional calculus are to
be taken as axiom schemes in their own right), quantifier axioms, and in addition to modus ponens
Modus ponens
In classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
, one additional rule of inference
Rule of inference
In logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion...
, known as the rule of generalization
Generalization (logic)
In mathematical logic, generalization is an inference rule of predicate calculus. It states that if \vdash P has been derived, then \vdash \forall x \, P can be derived....
: "From K, infer ∀vK."
In order to convert a proof of G from T∪{F} to one of F→G from T, one deals
with steps of the proof of G which are axioms or result from application of modus ponens in the
same way as for proofs in propositional logic. Steps which result from application of the rule of
generalization are dealt with via the following quantifier axiom (valid whenever the variable
v is not free in formula H):
- (H→K)→(H→∀vK).
Since in our case F is assumed to be closed, we can take H to be F. This axiom allows
one to deduce F→∀vK from F→K, which is just what is needed whenever
the rule of generalization is applied to some K in the proof of G.
Example of conversion
To illustrate how one can convert a natural deduction to the axiomatic form of proof, we apply it to the tautology Q→((Q→R)→R). In practice, it is usually enough to know that we could do this. We normally use the natural-deductive form in place of the much longer axiomatic proof.First, we write a proof using a natural-deduction like method:
-
- Q 1. hypothesis
- Q→R 2. hypothesis
- R 3. modus ponens 1,2
- (Q→R)→R 4. deduction from 2 to 3
- Q 1. hypothesis
- Q→((Q→R)→R) 5. deduction from 1 to 4 QED
Second, we convert the inner deduction to an axiomatic proof:
- (Q→R)→(Q→R) 1. theorem schema (A→A)
- ((Q→R)→(Q→R))→(((Q→R)→Q)→((Q→R)→R)) 2. axiom 2
- ((Q→R)→Q)→((Q→R)→R) 3. modus ponens 1,2
- Q→((Q→R)→Q) 4. axiom 1
- Q 5. hypothesis
- (Q→R)→Q 6. modus ponens 5,4
- (Q→R)→R 7. modus ponens 6,3
- Q→((Q→R)→R) 8. deduction from 5 to 7 QED
Third, we convert the outer deduction to an axiomatic proof:
- (Q→R)→(Q→R) 1. theorem schema (A→A)
- ((Q→R)→(Q→R))→(((Q→R)→Q)→((Q→R)→R)) 2. axiom 2
- ((Q→R)→Q)→((Q→R)→R) 3. modus ponens 1,2
- Q→((Q→R)→Q) 4. axiom 1
- [((Q→R)→Q)→((Q→R)→R)]→[Q→(((Q→R)→Q)→((Q→R)→R))] 5. axiom 1
- Q→(((Q→R)→Q)→((Q→R)→R)) 6. modus ponens 3,5
- [Q→(((Q→R)→Q)→((Q→R)→R))]→([Q→((Q→R)→Q)]→[Q→((Q→R)→R))]) 7. axiom 2
- [Q→((Q→R)→Q)]→[Q→((Q→R)→R))] 8. modus ponens 6,7
- Q→((Q→R)→R)) 9. modus ponens 4,8 QED
These three steps can be stated succinctly using the Curry–Howard correspondence:
- first, in lambda calculus, the function f = λa. λb. b a has type q → (q → r) → r
- second, by lambda elimination on b, f = λa. s i (k a)
- third, by lambda elimination on a, f = s (k (s i)) k
Paraconsistent deduction theorem
In general, the classical deduction theorem doesn't hold in paraconsistent logicParaconsistent logic
A paraconsistent logic is a logical system that attempts to deal with contradictions in a discriminating way. Alternatively, paraconsistent logic is the subfield of logic that is concerned with studying and developing paraconsistent systems of logic.Inconsistency-tolerant logics have been...
. However, the following "two-way deduction theorem" does hold in one form of paraconsistent logic:
-
if and only if (
and 
)
that requires the contrapositive inference to hold in addition to the requirement of the classical deduction theorem.
The resolution theorem
The resolution theorem is the converse of the deduction theorem. It follows immediately from modus ponensModus ponens
In classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
which is the elimination rule for implication.
External links
- Introduction to Mathematical Logic by Vilnis Detlovs and Karlis Podnieks Podnieks is a comprehensive tutorial. See Section 1.5.