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?
 A: 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:


*

*$B$ is an axiom. Then we can show $\Gamma\vdash A\to B$ as in the text

*$B\in \Gamma$. Again, see text

*$B=A$. Again, see text

*$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.
