prove using the Hilbert System

{not q} ⊢ (p→q)→(not p)

This means that I can assume (not q) and must prove (p→q)→(not p)

the only things I have available to me are these axioms
A1 (A - (B-A))
A2 ((A - (B-C)) - ((A-B)-(A-C)))
A3 (((~A) - (~B)) - (B-A))

and modus ponens which states if we have A-B and A we can infer B

Question

prove using the Hilbert System

{not q} ⊢ (p→q)→(not p)

This means that I can assume (not q) and must prove (p→q)→(not p)

the only things I have available to me are these axioms
A1 (A -> (B->A)) 
A2 ((A -> (B->C)) -> ((A->B)->(A->C))) 
A3 (((~A) -> (~B)) -> (B->A))

and modus ponens which states if we have A->B and A we can infer B

zugzwang · Answer

~q
Show that
(p→q)→~p ???

anonymous · Answer

yeah, but I need to use the axioms of the hilbert system to show it

zugzwang · Answer

Can you 
suppose
p→q
and then derive ~p
?

anonymous · Answer

I don't think I can assume (p->q). At least as far as my understanding of the hilbert system goes

anonymous · Answer

I think the only thing I can work with are the axioms and (~q)