Hi all,

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:

(1*) MP

(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.

Regards

Sam