Can someone please explain Deduction theorem in Logic. I am using the textbook "Mathematical Logic" for Tourlakis.
I can't understand it at all.
$\endgroup$ 13 Answers
$\begingroup$The statement is the reverse of modus ponens so to speak: If it is possible to deduce $B$ under the assumption that $A$ holds, then it is possible to deduce the single formula $A\to B$. But in contrast to modus ponens this is not an immediate rule of inference by itself, even though its result seems so obvious.
$\endgroup$ $\begingroup$You can see Stephen Cole Kleene, Mathematical Logic (1967).
It is not very "user friendly": other textbooks are better for beginning with mathematical logic, but it adopt a presentation of the proof system that is interesting.
Limit ourselfs for simplicity to propositional calculus (Chapter I, page 3-on): the book states an Hilbert-style proof system, based on a list of axioms [page 15]: from 1a to 10b, and a single rule of inference, the only primitive one : modus ponens [page 34].
Then he proves a set of "derived rules" [Theorem 13, page 44] that are the analogue of introduction and elimination rules of Natural Deduction.
Typically, we have a couple of rules (one for introduction and one for elimination) for every connective.
The couple of rules for $\rightarrow$ are :
$A,A \rightarrow B \vdash B \quad $ --- called $\rightarrow$-elimination; it is simply modus ponens
if $\Gamma , A \vdash B$, then $\Gamma \vdash A \rightarrow B \quad $ --- called $\rightarrow$-introduction; it is the Deduction Theorem [see Kleene, page 39].
The "derived rules" are proved via meta-theorems, i.e. we use an argument in the meta-theory showing that we can add them without causing troubles.
The proof of the Deduction Theorem amount to displaying a method that, whenever we are given a deduction of $B$ from the assumption $A$ and the set of assumptions $\Gamma$, we can "build" a new deduction of $A \rightarrow B$ from the set of assumptions $\Gamma$.
If we refer to George Tourlakis, Mathematical Logic (2008), we have a different set of axioms and two primitive rules of inference : Leibniz and Equanimity.
This is a different proof systems, but the general "mechanism" is the same : you can introduce derived rules, like Transitivity [page 47] and Equanimity + Leibniz Merged [page 57].
But the overall result is the same : we want that all different proof systems (Equational, Natural Deduction, Hilbert-style) are sound and complete, i.e. we want that each of them can prove all and only the tautologies.
Also in Tourlakis you have the Deduction Theorem : see page 81-on; can be useful to re-read at page 45 the Remark 1.4.10 (Theorem vs. Metatheorem).
$\endgroup$ 3 $\begingroup$By way of example, suppose we want to establish that $(a \to (b \to c)) \to (b \to (a \to c))$ is provable, i.e. that
$$\vdash (a \to (b \to c)) \to (b \to (a \to c))$$
The deduction theorem states that this holds if the following holds:
$$(a \to (b \to c)) \vdash (b \to (a \to c))$$
That is, there is a proof of the original theorem if we can prove $(b \to (a \to c))$ using $(a \to (b \to c))$ as an assumption. Applying the theorem again, the above holds if
$$(a \to (b \to c)),\ b \vdash (a \to c)$$
Which in turn holds if
$$(a \to (b \to c)),\ b,\ a \vdash c$$
That is, the original theorem is provable (with no assumptions) if $c$ is provable with $a$, $b$ and $a \to (b \to c)$ as assumptions. This is easy to prove:
- $(a \to (b \to c)),\ b,\ a \vdash a$ by assumption
- $(a \to (b \to c)),\ b,\ a \vdash a \to (b \to c)$ by assumption
- $(a \to (b \to c)),\ b,\ a \vdash b \to c$ by modus ponens on 1 and 2
- $(a \to (b \to c)),\ b,\ a \vdash b$ by assumption
- $(a \to (b \to c)),\ b,\ a \vdash c$ by modus ponens on 3 and 4.
To appreciate the usefulness of the deduction theorem, try to prove $(a \to (b \to c)) \to (b \to (a \to c))$ without using it.
So far, I have only shown (assuming that the deduction theorem is true) that $$(a \to (b \to c)) \to (b \to (a \to c))$$ is provable, but I haven't constructed such a proof.
The Wikipedia article has an algorithm for going from $\Gamma, H \vdash C$ to $\Gamma \vdash H \to C$, that is, for turning an assumption into a condition. Instead of proving $C$ given $H$, you can prove "if $H$ then $C$".
To construct a proof of $(a \to (b \to c)) \to (b \to (a \to c))$, use the proof of $c$ with assumptions to construct a proof of $a \to c$ with fewer assumptions, then a proof of $b \to (a \to c)$ with even fewer assumptions, and then a proof of $(a \to (b \to c)) \to (b \to (a \to c))$ with no assumptions.
$\endgroup$ 1
