Proof of deduction theorem without induction

Question

Can we prove deduction theorem without using inductive argument.

Using MP and following axiom schema:

1) A⇒(B⇒ A)

2) [A⇒(B⇒C)]⇒[(A⇒B)⇒(A⇒C)]

Answer 1

The deduction theorem takes the form "For any proof of type ...., there exists a proof of type ---". It is a general theorem, in other words, about proofs. In standard jargon, it is a meta-theorem about the propositional calculus, not a theorem inside the propositional calculus.

You obviously can't prove such a meta-level generalisation inside the Hilbert-style logical system, just using MP and instances of the given schemata, for those will only deliver more theorems inside the propositional calculus (which aren't generalisations about proofs!).

To prove the deduction theorem, you need to stand outside the propositional calculus and hit it with some appropriate mathematical tools to prove a general result about the propositional calculus. What more appropriate than an argument by induction on the length of proofs?