\documentclass[12pt]{article}
\usepackage{amsmath,amsfonts,amssymb,amsthm}

\usepackage{multicol}

\setlength{\oddsidemargin}{-0.25in}
\setlength{\evensidemargin}{-0.25in}
\setlength{\topmargin}{-0.5in}
\setlength{\headheight}{0.0in}
\setlength{\headsep}{0.0in}
\setlength{\topskip}{0.0in}
\setlength{\textheight}{9.85in}
\setlength{\textwidth}{7in}

\begin{document}

\newcommand{\LEMMA}{\vspace{0.05in} \noindent \fbox{\large\sc Lemma:}  }
\newcommand{\COR}{\vspace{0.05in} \noindent \fbox{\large\sc Corollary:}  }
\newcommand{\DEF}{\vspace{0.05in} \noindent \fbox{\large\sc Definition:}  }
\newcommand{\THM}{\vspace{0.05in} \noindent \fbox{\large\sc Theorem:}  }
\newcommand{\EX}{\vspace{0.05in} \noindent \fbox{\large\sc Example:}  }
\newcommand{\bproof}{\vspace{0.1in} \noindent {\bf Proof:} }
\newcommand{\eproof}{$\blacksquare$ \vspace{0.05in}}

\newcommand{\force}{{$\mbox{\,\!}$}}

\pagestyle{empty}

\begin{center}
\Large \sc The Deduction Theorem
\end{center}

\vspace{-0.1in}

\THM Let $\mathcal{H}$ be a set of propositions (hypotheses). If $A$ and $B$ are propositions, then\\ \force \hfill $\mathcal{H} \vdash_L A \to B$ if and only if $\mathcal{H},A \vdash_L B$. In particular, $A \vdash_L B$, if and only if $\vdash_L A \to B$.
 
% \vspace{0.15in}
 
\bproof
One direction of this result is easy. Suppose that $B_1,\dots,B_n$ is a proof of $\mathcal{H} \vdash_L A \to B$ where $B_n=A \to B$. Then the $B$'s are still valid steps if we have the hypotheses $\mathcal{H}$ plus $A$. So we have that $B_1,\dots,B_n=A \to B,B_{n+1}=A,B_{n+2}=B$ is a proof of $\mathcal{H},A \vdash_L B$ where the last two steps are justified because $A$ is a hypothesis and $B$ is the result of applying Modus Ponens to the previous two steps.
 
Now for the more difficult direction. Suppose $B_1,\dots,B_n$ (where $B_n=B$) is a proof of $\mathcal{H},A \vdash_L B$. Also, we assume that \underline{\it this} proof does not use any lemmas (calling on a lemma is merely an abbreviation, so this proof is completely unabbreviated). The proof below provides an algorithm for translating proofs relying on the deduction theorem to (longer) proofs avoiding the use of this theorem. First, we define three procedures:

\vspace{-0.05in}

\begin{description}
\item[Translation Procedure \#1:] For some step $B_m$, suppose that $B_m$ is a member of $\mathcal{H}$ or an axiom. After removing the hypothesis $A$, we still have all of the hypotheses in $\mathcal{H}$. So whether $B_m$ belongs to $\mathcal{H}$ or it is an axiom, $B_m$ is still allowed as a step in our (new) proof. So we replace $B_m$ in the old proof with $C_1=B_m$, $C_2 = (B_m \to (A \to B_m))$, $C_3=(A \to B_m)$ (briefly justified by Hypothesis/Axiom, Axiom \#1, Modus Ponens).  

\item[Translation Procedure \#2:] Suppose $B_m=A$. Then $A \to B_m$ is the same as $A \to A$ (i.e., Lemma \#1). Thus we replace $B_m$ by pasting in a proof of Lemma 1: $C_1 = A \to ((A \to A) \to A), C_2 = (A \to ((A \to A) \to A)) \to ((A \to (A \to A)) \to (A \to A)), C_3 = (A \to (A \to A)) \to (A \to A), C_4 = A \to (A \to A), C_5 = A \to A$ (briefly justified by Axiom \#1, Axiom \#2, Modus Ponens, Axiom \#1, Modus Ponens). 

\item[Translation Procedure \#3:] Suppose $B_m$ is the result of applying Modus Ponens to previous steps, say $B_k$ and $B_\ell$ (where $k,\ell <m$) and $B_\ell$ is an implication of the form $B_k \to B_m$ (so Modus Ponens can conclude $B_m$). Also, assume that we have previously proven $A \to B_k$ and $A \to B_\ell = A \to (B_k \to B_m)$. Then $B_m$ in our old proof is replaced by $C_1 = (A \to (B_k \to B_m)) \to ((A \to B_k) \to (A \to B_m))$ (this is Axiom \#2), $C_2=(A \to B_k) \to (A \to B_m)$ (this comes from Modus Ponens applied to $C_1$ and $A \to (B_k \to B_m)= A \to B_\ell$ (which was previously proven), $C_3=A \to B_m$ (again Modus Ponens is applied to $C_2$ and the previously proven $A \to B_k$).
\end{description}

\vspace{-0.05in}

We now proceed to translate our old proof of $\mathcal{H},A \vdash_L B$ to a proof of $\mathcal{H} \vdash_L A \to B$. The first step $B_1$ (of our old proof) must be either a hypothesis or an axiom. So $B_1$ is either something from $\mathcal{H}$, $A$ itself, or an axiom. Thus we apply either translation procedure \#1 or \#2 and now have a proof of $A \to B_1$ using only hypotheses in $\mathcal{H}$ (i.e., $\mathcal{H} \vdash_L A \to B_1$).

Next, assume we have translated/expanded steps $B_1,B_2,\dots,B_{m-1}$. So we have proof(s) of $\mathcal{H} \vdash_L A \to B_k$ for $k=1,2,\dots, m-1$. Consider $B_m$. Either $B_m$ is a hypothesis, axiom, or the result of an application of Modus Ponens (we have unabbreviated all lemmas, so this kind of step doesn't show up). If $B_m$ is a hypothesis (i.e., either a member of $\mathcal{H}$ or $A$) or an axiom, we can apply either translation procedure \#1 or \#2. Alternatively, if $B_m$ is the result of Modus Ponens, we are in the context of translation procedure \#3 (we've previously proven $A \to B_k$ and $A \to B_\ell = A \to (B_k \to B_m)$, so we apply this translation procedure and by tacking these steps onto
the end of our proofs of $\mathcal{H} \vdash_L A \to B_k$ for $k=1,2,\dots, m-1$, we get a proof of $\mathcal{H} \vdash_L A \to B_m$.  

Once we have applied this procedure going from $B_1$ to $B_n$, our final conclusion is $A \to B_n = A \to B$. Thus we get a proof of $\mathcal{H} \vdash_L A \to B$. 
\eproof

\newpage

Let's prove Lemma 6 using the deduction theorem and then apply our translation procedures to remove the use of the theorem.

\vspace{0.15in}

\noindent \fbox{\large\sc Lemma 6:} $A \to (B \to C), B \vdash_L A \to C$

\bproof
First, we prove $A \to (B \to C), B, A \vdash_L C$.

\vspace{0.05in}

% Increase tablular row spacing (so proof isn't so squished).
\renewcommand{\arraystretch}{1.2}

\noindent
\begin{tabular}{rlcl}
1. &  $A \to (B \to C)$ & \qquad & Hypothesis\\
2. & $B$  & & Hypothesis \\
3. & $A$  & & Hypothesis \\
4. & $B \to C$  & & M.P. \#1 and \#3 \\
5. & $C$  & & M.P. \#4 and \#2
\end{tabular}

\vspace{0.05in}

Therefore, since we have proven $A \to (B \to C), B, A \vdash_L C$, by the deduction theorem we also have $A \to (B \to C), B \vdash_L A \to C$
\eproof

\vspace{0.05in}

Now let's use our translation procedures to get (a much longer) proof of Lemma 6 without calling on the deduction theorem.

%\vspace{0.05in}
\bproof

\vspace{0.05in}

\noindent
\force \hspace{-0.1in}
\begin{tabular}{rlcl}
$1_1$. &  $A \to (B \to C)$ & \quad & Hypothesis\\ \vspace{0.05in}
$1_2$. &  $(A \to (B \to C)) \to (A \to (A \to (B \to C)))$ & \qquad & Axiom \#1 with $A:=A \to (B \to C)$ and $B:=A$\\
$1_3$. &  $A \to (A \to (B \to C))$ & \qquad & M.P. \#$1_2$ and \#$1_1$\\
$2_1$. & $B$  & & Hypothesis \\
$2_2$. &  $B \to (A \to B)$ & \qquad & Axiom \#1 with $A:=B$ and $B:=A$\\
$2_3$. &  $A \to B$ & \qquad & Modus Ponens \#$2_2$ and \#$2_1$\\
$3_1$. & $A \to ((A \to A) \to A)$  & &  Axiom \#1 with $A:=A$ and $B:=A$\\
$3_2$. & \parbox[t][][t]{3in}{$A \to ((A \to A) \to A)$\\ \force \hfill $\to ((A \to (A \to A)) \to (A \to A))$}  & &  \parbox[t][][t]{3.45in}{Axiom \#2 with $A:=A$ and $B:=A \to A$\\ \force \hfill and $C:=A$}\\
$3_3$. & $(A \to (A \to A)) \to (A \to A)$  & &  M.P. \#$3_2$ and \#$3_1$\\
$3_4$. &  $A \to (A \to A)$ & \qquad & Axiom \#1 with $A:=A$ and $B:=A$\\
$3_5$. & $A \to A$  & &  M.P. \#$3_3$ and \#$3_4$\\
$4_1$. & \parbox[t][][t]{3in}{$A \to (A \to (B \to C))$\\ \force \hfill $\to ((A \to A) \to (A \to (B \to C))$}  & &  \parbox[t][][t]{3.45in}{Axiom \#2 with $A:=A$ and $B:=A$\\ \force \hfill and $C:=B \to C$}\\
$4_2$. & $(A \to A) \to (A \to (B \to C))$  & &  M.P. \#$4_1$ and \#$1_3$\\
$4_3$. & $A \to (B \to C)$  & &  M.P. \#$4_2$ and \#$3_5$\\
$5_1$. & $A \to (B \to C) \to ((A \to B) \to (A \to C))$  & &  Axiom \#2 with $A:=A$ and $B:=B$ and $C:=C$\\
$5_2$. & $(A \to B) \to (A \to C)$  & & M.P. \#$5_1$ and \#$4_3$\\
$5_3$. & $A \to C$  & & M.P. \#$5_2$ and \#$2_3$\\
\end{tabular}

\vspace{0.05in}

\noindent \eproof

%\vspace{0.1in}

Summing up, we can always translate proofs using the deduction theorem to proofs that avoid its usage. This is still true if we use several instances of the deduction theorem to turn nested implications into multiple hypotheses. But each usage of the deduction theorem would require a new run through our translation theorem. Notice that the translation procedure increases the proof's length by a factor of 3 (plus 2 more lines if lemma \#1's proof is pasted in since it's $5=3+2$ lines long). Thus if we called on the deduction theorem twice and our resulting proof was 4 lines long, the proof only calling on it once would likely be $4 \times 3 + 2 = 14$ lines long and then the proof not calling it at all would likely be $14 \times 3 + 2 = 44$ lines long! Yikes!!




\end{document}
