Just to say: I'd also be really interested to hear if people who think they should be able to prove the deduction theorem from these premises can't. I'm suspicious that they can, but I'd like to know either way!
I'm struggling to see how to derive the deduction theorem from some particular axioms. Basically I've got:
(1) A -> (B -> A)
(2) A -> (B -> C) ->((A -> B) -> (A -> C))
(3) (~A -> ~B) -> (B -> A)
(4) (x)A -> A(t) where t is free for x.
Rules of inference are:
(2*) From A -> B, infer A -> (x)B so long as x does not occur free in A or any premise.
Supposing we are proving the theorem for A, at the inductive step I get stuck showing that if C is derived from D by means of (2*) and we have A -> D, then we have A ->C.
Any help would be really great.
Suppose that the derivation with an assumption A ends with the application of (2*); say, we infer B -> (x)C from B -> C. By IH, there exists a derivation of A -> (B -> C). Now, it is equivalent to A /\ B -> C, i.e., ~(A -> ~B) -> C. In more detail, the formulas
(A -> (B -> C)) -> (~(A -> ~B) -> C) (*)
(~(A -> ~B) -> C) -> (A -> (B -> C)) (**)
are derivable in propositional logic. Therefore, from (A -> (B -> C)) and (*) we can derive ~(A -> ~B) -> C by MP. Since (2*) was applied legally in the old derivation, x does not occur freely in A or B, so we can get ~(A -> ~B) -> (x)C. From here and (**), A -> (B -> (x)C) is obtained by MP.
Of course, (*) and (**) have to be derived first. For example, completeness theorem for propositional logic can be proved before considering predicate logic.
This method may not be optimal because one has to use the axiom (3) to derive (*) and (**), whereas, say, in Natural Deduction, the analog of (3) is not necessary.
Do you have a proof of this fact from a textbook or a lecture? If you don't understand a particular step, we can discuss it.
Too bad it's not the system exactly as the one in the original post except (2*) is replaced by axiom schema (5): B -> (x)B, where x does not occur free in B.
Then you'd be done just by proving the four cases you've already proven: (1) the conclusion is an axiom, (2) the conclusion is a premise, (3) the conclusion is of the form P -> P, (4) the conclusion follows by modus ponens.