2
$\begingroup$

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$
1
  • $\begingroup$ When I was struggling with Enderton's 'A Mathematical Introduction to Logic', I found Mordechai Ben-Ari's 'Mathematical Logic for Computer Science' extremely useful for self-learning. $\endgroup$
    – KGhatak
    Jun 21, 2020 at 18:40

3 Answers 3

5
$\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$
3
$\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$ So how could i use the deduction theorem ? And What kind of questions can i get on the deduction theorem? Also i would be thankful if you explained 3.1 and 3.2 in Tourlakis. The material is very hard to understand. It would be good if you gave a summary of these two sections and how could i use them ? $\endgroup$ Feb 21, 2014 at 16:24
  • $\begingroup$ @Tennisman -you can read this post and you can appreciate how much easier is to prove some results with the DT than without it ... $\endgroup$ Feb 22, 2014 at 8:27
  • $\begingroup$ @Trismegistos - Thanks ! $\endgroup$ Feb 24, 2014 at 10:22
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:

  1. $(a \to (b \to c)),\ b,\ a \vdash a$ by assumption
  2. $(a \to (b \to c)),\ b,\ a \vdash a \to (b \to c)$ by assumption
  3. $(a \to (b \to c)),\ b,\ a \vdash b \to c$ by modus ponens on 1 and 2
  4. $(a \to (b \to c)),\ b,\ a \vdash b$ by assumption
  5. $(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
  • $\begingroup$ Bonus point for mentioning the conversion algorithm on Wikipedia! I've been looking for that for a day now, but didn't know how to search for it and finally found it now thanks to you! $\endgroup$
    – Isti115
    Apr 29, 2020 at 21:39

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .