# What is the utility, exactly, of the Deduction Theorem?

The Deduction Theorem states that for a set of assumptions $\Delta$ and two wffs $A$ and $B$, we have the metalogical relationship:

$$\Delta \cup \{A\} \vdash B \implies \Delta \vdash A \to B$$

In other words if we can prove $B$ from some set of assumptions (conjoined with $A$), then it's the same as proving $A \to B$ from our assumptions.

My question here is not asking for a proof: I'm asking what it's allowing us to do. I'm not even fully sure I understand what this is saying or how its making our lives any easier.

From my uninitiated perspective it would seem that the advantage is letting us treat the logical connective $\to$ as a way to represent a proof from $A$ to $B$ within our logic system rather than mucking about in the metalogical realm, but I feel like I'm looking at it wrong / interpreting this result incorrectly.

What is the deduction theorem telling us? How does it make things more "natural"? What is it doing?

• In the line below the displayed equation the phrase (intersected with $A$) should read in conjunction with $A$). $\Delta \cup \{ A \}$ means you are adding something to $\Delta$. – Jay Sep 19 '18 at 22:40
• It's useful when proving all sorts of things. It's usually a small intermediate step when trying to prove certain things; but it is also used in the proof of the soundness theorem. – Squirtle Sep 19 '18 at 22:40
• you just need to go and practice writing proofs using this system without using any additional theorems like this one. Only axioms and MP. You will quickly see that you might want to use some shortcuts like this theorem. – famesyasd Sep 19 '18 at 23:35
• After doing enough proofs in the Hilbert system you might want to take a look at another systems to see if they are any more comfortable than this one. – famesyasd Sep 19 '18 at 23:41

The theorem says that to prove an implication it is enough to assume the hypothesis and proceed to prove the conclusion. Proofs of that kind tend to be more natural than proofs that conclude the implication directly.

Just as in regular mathematical practice: many theorems have the form "Assuming $A$, then we have $B$", and we usually prove them by assuming $A$ and using it along the way to conclude $B$. And we feel we are done, even though the task was not to prove $B$, but instead "$A$ implies $B$".

So the theorem is saying that the rules of propositional calculus "capture" a common way of reasoning in practice. The more of such rules we manage to establish the easier it becomes to use the calculus to prove statements. The first few formal proofs always feel strange, perhaps even artificial. These results, such as the deduction theorem, aim at turning this rigid, "artificial" proof system into a natural and useful tool.

There is another key reason why the theorem is useful, now in the context of propositional logic itself, namely, it is a basic tool that helps us prove the completeness theorem. We establish other metatheorems along the way (such as: We can argue by contradiction), and all combined help us in making feasible the task of showing that the proof system is complete: We define a notion of truth for propositional formulas (via truth tables), and completeness says that the proof system is enough to deduce all true implications. This is a very useful first step in more elaborate contexts where we may want to mechanize proofs in more complicated logics.

• Wonderful answer, +1! – Taroccoesbrocco Sep 19 '18 at 22:47
• @user525966 As an example, Lemma 1.11(d) in Mendelson's logic text is proven with the assistance of the deduction theorem. An earlier StackExchange question asked for assistance in proving this result without the deduction theorem; the answers given there should be enlightening in understanding the difference. – Ian Sep 19 '18 at 23:09
• @user525966 Yes, that's what it means. And the deduction theorem says precisely that given a proof for $\{A\} \vdash B$ ("Assume $A$; by the end we conclude $B$"), there exists also a proof for $\vdash A \rightarrow B$ ("Assume nothing; by the end we conclude $A \rightarrow B$"). – Ian Sep 20 '18 at 0:21
• No. Without the deduction theorem, you are left with the task of proving $A\to B$. That is what you want. The fact that $A\vdash B$ does not mean a priori that you indeed have proved $A\to B$. Again: Most mathematical theorems in practice are statements of the form $A\to B$. That is what you want to prove. The deduction theorem gives you a way to conclude that, from the sort of move that is standard in mathematics. Perhaps the confusion is that it may seem that the content of the result is that if $\vdash A\to B$ then $\{A\}\vdash B$. But this is trivial. The deduction theorem is the converse. – Andrés E. Caicedo Sep 20 '18 at 0:55
• I'm sorry, but it seems to me you are not listening to the answers. Again, in mathematics you prove theorems. You cannot prove assumptions. In proofs, all steps are axioms or theorems. No step is an assumption. Without the deduction theorem you cannot prove "If $X$ is a closed and bounded set of reals, then $X$ is compact" by saying "Assume $X$ is a closed and bounded set of reals" and going from there, because "$X$ is a closed and bounded set of reals" is not itself a theorem. – Andrés E. Caicedo Sep 20 '18 at 1:19