# Trouble proving the deduction theorem

I wish to show that in a Hilbert-style propositional logic system, 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$$

Where we have axiom schemas such as $\vdash A \to (B \to A)$ as well as $\vdash (A \to (B \to C)) \to ((A \to B) \to(A \to C))$ and the modus ponens rule of inference $A, A \to B \vdash B$.

To my understanding this deduction theorem is saying "If we have proven $B$ from the set of assumptions $\Delta \cup \{A\}$, then we have also proven $A \to B$ from the set of assumptions $\Delta$."

Let's say we have an $n$-line proof of $\Delta \cup \{A\} \vdash B$. For integer $k$ where $1 \leq k \leq n$, we have lines $\varphi_1, \varphi_2, ..., \varphi_n$ where $\varphi_n = B$.

Every single $\varphi_k$ in this proof is either:

1. An instance of an axiom schema (i.e. an axiom), or a theorem, i.e. a wff built from axioms.
2. An assumption from $\Delta$.
3. A wff proven via modus ponens from two earlier lines, i.e. $\varphi_i, \varphi_j \vdash \varphi_k$ where $\varphi_j = \varphi_i \to \varphi_k$ and $i,j < k$.

Let's focus on case $1$ first and say that we have some $\varphi_k = B \to (A \to B)$. And since we are given that we have a proof of $B$, then by modus ponens we also have $B, B \to (A \to B) \vdash (A \to B)$, so we have also proven $A \to B$.

First question: Have I been speaking correctly / accurately so far?

Second question: Does this mean we have shown $\Delta \vdash A \to B$ or have we only shown that $\Delta \cup \{A\} \vdash A \to B$? I don't quite understand how we "eliminate" the $A$ bit on the left side.

• The deduction theorem actually says that if there is a derivation of $B$ from $\Delta,A$ then there is a different derivation of $A \to B$ from $\Delta$. The new derivation is constructed by following the proof of the deduction theorem, but it is not at all the same as the original derivation. – Carl Mummert Sep 26 '18 at 1:01

You are right to suspect that your described method does not work to prove the Deduction Theorem: if you simply extend the existing deduction of $$B$$ from $$\Delta \cup \{ A \}$$ by adding $$B \rightarrow (A \rightarrow B)$$ (from axiom 1) and then getting $$A \rightarrow B$$ through Modus Ponens, then all you have ended up showing is that there is a deduction of $$\Delta \cup \{ A\} \vdash A \rightarrow B$$, because the original set of premises is still $$\Delta \cup \{ A \}$$. And you can't just throw out the $$A$$, since in the extended derivation, you still need to get to $$B$$ by itself, which may well depend on $$A$$.

So ... you need to do something else to show $$\Delta \vdash A \rightarrow B$$

Here is what you need to do. Transform the deduction of $$\Delta \cup \{A \} \vdash B$$ into a deduction of $$\Delta \vdash A \rightarrow B$$ by showing how you can get a deduction $$\Delta \vdash A \rightarrow \varphi_i$$ for $$\varphi_i$$ of the original deduction. And that you can show by strong induction, where you have to consider that every $$\varphi_i$$ comes about as one of the three cases: as an element of $$\Delta$$, an instance of some axiom, or by the use of Modus Ponens.

Here is a simple example:

If we take that $$\Delta = \{ A \rightarrow B \}$$, then we know that $$\Delta \cup \{ A \} \vdash B$$, i.e. that $$\{ A \rightarrow B, A \} \vdash B$$. Indeed, here is a derivation for that:

$$\begin{array}{ccc} 1 & A \rightarrow B & Given\\ 2 & A & Given\\ 3 & B & \text{Modus Ponens } 2,3 \end{array}$$

OK, so now we want to convert this to a derivation of $$\Delta \vdash A \rightarrow B$$, i.e. of $$\{ A \rightarrow B \} \vdash A \rightarrow B$$

Now, there is of course a very simple derivation for $$\{ A \rightarrow B \} \vdash A \rightarrow B$$, but what I want to show below is that we can systematically convert the earlier derivation of $$\{ A \rightarrow B, A \} \vdash B$$ into a new derivation of $$\{ A \rightarrow B \} \vdash A \rightarrow B$$

Again, the basic idea is that, since we are 'pulling out' $$A$$ from the set of assumptions, in the new derivation we want to get a statement of the form $$A \rightarrow \varphi_i$$ for every line $$\varphi_i$$ from the original derivation. Think of this as 'conditionalizing' every statement with the condition $$A$$. So, the basic scheme for the derivation will look like:

$$\begin{array}{ccc} ..\\ k & A \rightarrow (A \rightarrow B) & ??\\ ..\\ l & A \rightarrow A & ??\\ ..\\ m & A \rightarrow B & ?? \end{array}$$

Now, notice that the last line is $$A \rightarrow B$$, which is exactly what we are trying to get, so that's already good. But of course, we have yet to figure out how to actually get there. In fact, let's first enter the givens, which are all the same givens as in the original derivation, excvept for $$A$$, since that's the one we're 'pulling out':

$$\begin{array}{ccc} 1 & A \rightarrow B & Given\\ ..\\ k & A \rightarrow (A \rightarrow B) & ??\\ ..\\ l & A \rightarrow A & ??\\ ..\\ m & A \rightarrow B & ?? \end{array}$$

OK, now, note that we put down line $$k$$ exactly because we had line $$1$$ as a given in the original derivation. That is, for tevery $$\varphi_i \in \Delta$$, we put down, and are trying to get to, $$A \rightarrow \varphi_i$$ .. how can we do that? Easy: just exploit axiom $$1$$:

$$\begin{array}{ccc} 1 & A \rightarrow B & Given\\ 2 & (A \rightarrow B) \rightarrow (A \rightarrow (A \rightarrow B)) & \text{ Axiom } 1\\ 3 & A \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 1,2 \\ ..\\ l & A \rightarrow A & ??\\ ..\\ m & A \rightarrow B & ?? \end{array}$$

Now, the $$A \rightarrow A$$ is because the $$A$$ was in the original set of givens as well, but since in the new derivation we no longer have $$A$$ as a given, we need to derive $$A \rightarrow A$$ in a different way. But, as you found, such a derivation can always be done:

$$\begin{array}{ccc} 1 & A \rightarrow B & Given\\ 2 & (A \rightarrow B) \rightarrow (A \rightarrow (A \rightarrow B)) & \text{ Axiom } 1\\ 3 & A \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 1,2 \\ 4 & (A \rightarrow ((A \rightarrow A) \rightarrow A) \rightarrow ((A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)) & \text{ Axiom } 2\\ 5 & A \rightarrow ((A \rightarrow A) \rightarrow A) & \text{ Axiom } 1\\ 6 & (A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A) & \text{ Modus Ponens } 4,5 \\ 7 & A \rightarrow (A \rightarrow A) & \text{ Axiom } 1\\ 8 & A \rightarrow A & \text{ Modus Ponens } 6,7 \\ ..\\ m & A \rightarrow B & ?? \end{array}$$

OK, almost done. Now we need to show how line $$m$$ can be derived from the original lines $$k$$ and $$l$$, i.e. lines $$3$$ and $$8$$. Well, for this you use axiom 2. That is, since in the original derivation we went from $$A \rightarrow B$$ and $$A$$ to $$B$$ via Modus Ponens, in the new derivation we need to do this using the conditionalized statements, i.e. we need to go from $$A \rightarrow (A \rightarrow B)$$ and $$A \rightarrow A$$ to $$A \rightarrow B$$. How do we do this? Well, this is exactly what Axiom 2 is for: Axiom 2 always looks a ittle weird if you first see it, but Axiom 2 is actually the embodiment of this kind of 'conditionalized Modus Ponens'. Here is how it goes:

$$\begin{array}{ccc} 1 & A \rightarrow B & Given\\ 2 & (A \rightarrow B) \rightarrow (A \rightarrow (A \rightarrow B)) & \text{ Axiom } 1\\ 3 & A \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 1,2 \\ 4 & (A \rightarrow ((A \rightarrow A) \rightarrow A) \rightarrow ((A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)) & \text{ Axiom } 2\\ 5 & A \rightarrow ((A \rightarrow A) \rightarrow A) & \text{ Axiom } 1\\ 6 & (A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A) & \text{ Modus Ponens } 4,5 \\ 7 & A \rightarrow (A \rightarrow A) & \text{ Axiom } 1\\ 8 & A \rightarrow A & \text{ Modus Ponens } 6,7 \\ 9 & (A \rightarrow (A \rightarrow B))\rightarrow ((A \rightarrow A) \rightarrow (A \rightarrow B)) & \text{ Axiom } 2\\ 10 & (A \rightarrow A) \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 3,9 \\ 11 & A \rightarrow B & \text{ Modus Ponens } 8,10 \end{array}$$

.... and we're done!

OK, so this was just a simple example, but I think you can see how this general technique always works: Your goal is to conditionalize all statements from the original derivation with the '$$A$$' that you pull out, and you derive those as follows:

Derive $$A \rightarrow A$$ for that $$A$$.

Derive $$A \rightarrow \varphi_i$$ for every $$\varphi_i \in \Delta$$ using the $$\varphi_i$$ you still have as a given in the new derivation, and using axiom 1.

Derive any $$A \rightarrow \varphi_k$$ where in the original derivation $$\varphi_k$$ was derived using Modus Ponens from earlier $$\varphi_i$$ and $$\varphi_j = \varphi_i \rightarrow \varphi_k$$ from the conditionalized $$A \rightarrow \varphi_i$$ and $$A \rightarrow \varphi_j = A \rightarrow (\varphi_i \rightarrow \varphi_k)$$ using axiom 2

• But in the lines of a proof, it's possible none of them are $A$, and it's possible no assumptions from $\Delta$ are used correct? – user525966 Sep 19 '18 at 13:39
• @user525966 That's correct ... but of course you cannot assume that. So, if you do have a line $A$ in the original proof, you'll want to make sure you get to a line $A \rightarrow A$ in the transformed proof. But you know how to derive $A \rightarrow A$ from those two axioms, right? – Bram28 Sep 19 '18 at 20:10
• proofwiki.org/wiki/Law_of_Identity/Formulation_2/Proof_3 but it's a bit long. However I am still a little unclear or what all of this "looks like". We have some collection of assumptions "off to the side" but then we have our main "proof" which is composed of lines, and these lines are either axioms, theorems, items found in our assumption pool, or new syntactic results from modus ponens, right? And $A$ is just some arbitrary assumption we toss alongside near our assumption pool and may or may not ever be included in the proof lines. – user525966 Sep 19 '18 at 20:16
• @user525966 I added an example conversion to my post – Bram28 Sep 23 '18 at 0:03
• A minor question but in your final proof, line $10$, I think it's modus ponens $3, 9$, and then for line $11$, modus ponens $8, 10$? – user525966 Sep 25 '18 at 13:03