Proof of the deduction theorem explanation

I'm reading through this proof of the deduction theorem, and there are a few things I don't understand.

The basic idea is to show that if $\Gamma\cup \{A\}\vdash B$, then we have a proof of $B$ with $n$ lines. We let $B_1,...,B_n=B$ denote the formulas appearing in each line of the proof of $B$ and we prove by induction that $\Gamma\vdash (A\implies B_i)$ for all $1\le i\le n$, in particular, we'll have proved that $\Gamma\vdash (A\implies B)$.

I get the proof of the base case, but I got lost in the inductive step, it looks the author uses some kind of 'double-induction', could someone explain what happens from the beginning of the inductive step and forwards? Is this proof really rigorous?

1 Answer

The formulation might be a bit misleading. The author does not perform the induction on a specific proof of a specific statement $B$, but rather the $n$ case is that all proofs of length $n$ of arbitrary stateent (not only of $B$) allow us to apply the deduction theorem. With a different view on induction, we can combine the base case and inductive step (as you may have noticed that there was a bit of repeating going on):

Let $S$ be the set of formulas $B$ with the property $\Gamma\cup\{A\}\vdash B$. Then for each $B\in S$ there exists at least one proof of $\Gamma\cup\{A\}\vdash B$. Given $B\in S$, let $f(B)$ be the minimal length (in lines) such a proof can have. Let $S'$ be the set of formulas $B$ for which $\Gamma\vdash A\to B$.

Assume $S\setminus S'$ is not empty and let $B\in S\setminus S'$ be such that $f(B)$ is minimal. Pick a proof of $\Gamma\cup\{A\}\vdash B$ of length $n:=f(B)$. Then one of four cases are possible:

1. $B$ is an axiom. Then we can show $\Gamma\vdash A\to B$ as in the text
2. $B\in \Gamma$. Again, see text
3. $B=A$. Again, see text
4. $B$ is obtained by modus ponens from two earlier lines of the form $C\to B$ and $C$ in our proof. The very fact that these lines occur before the last line of a proof of lengh $n$ tells us that $\Gamma\cup C$ and $\Gamma\cup C\to B$ require less than $n$ lines of proof. Therefore $f(C)<n$, $f(C\to B)<n$ (and in fact $C,C\to B\in S$ in the first place) and thus by minimality of $n$ we have $C\in S'$, $C\to B\in S'$. Thus we can write down a proof of $\Gamma \vdash A\to C$, followed by a proof of $\Gamma \vdash A\to(C\to B)$, and then append three more steps 8as in the text) to arrive at $C\vdash A\to B$.

As we found $B\in S'$ in each of the four possible cases, the assumption that $S\setminus S'$ is not empty must be wrong.