Proving the Deduction Theorem In propositional logic, how do we prove metalogical concepts like the Deduction Theorem, which says
$$\Delta, A \vdash B \implies \Delta \vdash A \to B$$
Hopefully I am using the symbols correctly. I'm not sure if these have more formal representations (I am uncomfortable using $\implies$ since its meaning isn't standardized).
Anyhow since we are operating outside of logic does this mean our proof of this theorem must resort to informal reasoning in some regard? How do we proof this result when $\to$ is just an arbitrary connective? Are we introducing an interpretation first?
 A: Here is the standard proof of the deduction theorem that I know. For each statement $C$ that occurs in the proof $P_1$ of $B$ from $\Delta\cup\{A\}$, the statement $A\to C$ is proved in the proof $P_2$ of $A\to B$ from $\Delta$.
For example, in the Hilbert system, if $C$ is a statement that occurs in $P_1$ then $C$ is an axiom or $C\in\Delta$ or $C=A$ or $C$ follows from modus ponens. If $C$ is an axiom or if $C\in\Delta$ then we may derive $A\to C$ in $P_2$ from the axiom $C\to(A\to C)$ and modus ponens. If $C=A$ then we prove $A\to A$ in $P_2$ (which is either an axiom or an easy consequence of the axioms). If $C$ follows from modus ponens then $C=Y$ where both $X$ and $X\to Y$ have been proven in $P_1$. Inductively, we have that $A\to X$ and $A\to(X\to Y)$ have been proven in $P_2$. Then we may derive $A\to C$ in $P_2$ from the axiom $(A\to(X\to Y))\to((A\to X)\to(A\to Y))$ and two applications of modus ponens.
A: To answer the last paragraph first, there is no presumption of an interpretation here. To say whether or not $\to$ could be any arbitrary connective in this case, it depends on what you mean. If the question is whether, from the same axioms and rules of inference, you could derive the same thing for $\vee$ or $\wedge$, the answer is no; the proof rules treat the connectives differently. If the question is whether you can derive it regardless of what kind of changes you made to the semantics, the answer is yes; changing the semantics may break things like soundness or completeness, but it won't change the notion of proof.
And since this theorem is stated outside of the logic in question, it means the proof lives in some kind of metalanguage, but the metalanguage may be another formal language (like ZFC or something). In practice, the proofs you read will usually be presented informally, as a sketch of how you could potentially implement it in some more formal language, but lots of these theorems have been proved in a completely formal way with software like Coq.
As for how to prove it, I steal this approach for a Hilbert system from Bell & Machover's A Course in Mathematical Logic. First, we need to understand what a deduction is for a Hilbert-style proof system. Given a set of formulas $\Phi$, a deduction of $\alpha$ from $\Phi$ is a sequence of formulas $\varphi_1,\ldots,\varphi_n$ such that (A) $\varphi_n=\alpha$, and (B) for each $k$ with $1\leq k\leq n$, $\varphi_k$ is either an axiom, a member of $\Phi$, or there are $i,j\lt k$ with $\varphi_j=\varphi_i\to\varphi_k$ (i.e. $\varphi_k$ can be obtained by modus ponens from previous formulas in the proof). If there exists a sequence like this, we say $\Phi\vdash \alpha$.
So let's single out a particular member of $\Phi$ and call it $\beta$, and assume we have any particular deduction $D=[\varphi_1,\ldots,\varphi_n=\alpha]$.  There are basically two cases.
Case 1: $\varphi_k$ is an axiom, or in $\Phi$, we have already that $\varphi_k\to (\beta\to\varphi_k)$ is an axiom, then we can add to our deduction $D$ the three additional steps 


*

*$\varphi_k$

*$\varphi_k\to(\beta\to\varphi_k)$

*$\beta\to\varphi_k$


The new deduction is now a deduction $\Phi\vdash\beta\to\alpha$. 
Case 2: If there are $i,j\lt k$ with $\varphi_j=\varphi_i\to\varphi_k$, then we can add to $D$ the new lines $$[\varphi_i\to(\beta\to\varphi_i),\:\beta\to\varphi_i,\:(\varphi_i\to\varphi_k)\to(\beta\to(\varphi_i\to\varphi_k),\:\beta\to(\varphi_i\to\varphi_k)].$$ Another axiom of most Hilbert systems is $$(\beta\to(\varphi_i\to\varphi_k))\to((\beta\to\varphi_i)\to(\beta\to\varphi_k)).$$ If in addition to the four steps we just added we also add this axiom and the obvious ones that follow from applying modus ponens, then the new deduction is again one that $\Phi\vdash\beta\to\varphi_k$. In particular, we obtain $\beta\to\alpha$ since $\alpha=\varphi_n$.
