help with some Hilbert style proofs in a propositional logic axiom system. I'm very new to classical propositional logic, and my lecturer is using a system with the following axioms:
A1. X→(Y→X)
A2. (X→(Y→Z))→((X→Y)→(X→Z))
A3. (¬Y→¬X)→(X→Y)
Use uniform substitution and Modes Ponens (MP) as rule of inference. Deduction Theorem also allowed.
I'd like to deduce the following:
(a) X, Y ⊢ ¬(X→(¬Y)) (conjunction, but expressed in terms of NOT and IMPLIES)
(b) X→((X→Y)→Y)
(c) (X→Y)→(((¬Y)→X)→Y)
(d) (((¬Y)→X)→Y)→(X→Y)
Remark: The last two are to show that the axiom (A3) can be replaced with a different axiom:
B3. (¬Y→¬X)→(((¬Y)→X)→Y).
Solution: Bram28 proves (b) and (c) below. I demonstrate (a) and (d).
(d) is alright; first, I claim that X, ((¬Y→X)→Y) ⊢ Y.
Axiom (A1) gives ⊢X→(¬Y→X) so that ((¬Y→X)→Y)⊢X→Y by Hypothetical Syllogism (HS), which Bram28 shows to be valid.
Now that we have ((¬Y→X)→Y)⊢X→Y just apply the deduction theorem to get what we want: ⊢((¬Y→X)→Y)→(X→Y).
(a) is slightly trickier.
Axiom (A1) gives ⊢ Y→(X→Y) so that X, Y ⊢ (X→Y).
Next, by part (b), we have as a theorem that ⊢X→((X→¬Y)→¬Y).
Therefore X, Y ⊢(X→¬Y)→¬Y.
But ⊢(¬¬(X→¬Y))→(X→¬Y) by DN Elim, which Bram28 shows to be valid.
By HS, X, Y ⊢(¬¬(X→¬Y))→¬Y.
By Axiom (A3) and MP, X, Y ⊢(Y→¬(X→¬Y)).
Also, rather trivially X, Y ⊢Y.
Finally by MP we conclude X, Y ⊢¬(X→¬Y) as required.
 A: Just as an example of how to use the Deduction Theorem, let me do b)
First, let's show that $X, X \rightarrow Y \vdash Y$:


*

*$X$ Premise

*$X \rightarrow Y$ Premise

*$Y$ MP 1,2
OK, so we have $X, X \rightarrow Y \vdash Y$
By the Deduction Theorem, we thus have $X \vdash (X \rightarrow Y) \rightarrow Y$
And applying the Deduction Thorem on that, we get $\vdash X \rightarrow ((X \rightarrow Y) \rightarrow Y)$
Now, the others aren't quite so easy, but here are some useful derivations thay may help:
Let's prove: $\phi \to \psi, \psi \to \chi, \phi \vdash \chi$:


*

*$\phi \to \psi$ Premise

*$\psi \to \chi$ Premise

*$\phi$ Premise

*$\psi$ MP 1,3

*$\chi$ MP 2,4
By the Deduction Theorem, this gives us Hypothetical Syllogism (HS): $\phi \to \psi, \psi \to \chi \vdash \phi \to \chi$
Now let's prove the general principle that $\neg \phi \vdash (\phi \to \psi)$:


*

*$\neg \phi$ Premise

*$\neg \phi \to (\neg \psi \to \neg \phi)$ Axiom1

*$\neg \psi \to \neg \phi$  MP 1,2

*$(\neg \psi \to \neg \phi) \to (\phi \to \psi)$ Axiom3

*$\phi \to \psi$ MP 3,4
With the Deduction Theorem, this means $\vdash \neg \phi \to (\phi \to \psi)$ (Duns Scotus Law)
Let's use Duns Scotus to show that $\neg \phi \to \phi \vdash \phi$


*

*$\neg \phi \to \phi$ Premise

*$\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))$ (Duns Scotus Law)

*$(\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))) \to ((\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi)))$  Axiom2

*$(\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi))$  MP 2,3

*$\neg \phi \to \neg (\neg \phi \to \phi)$ MP 1,4

*$(\neg \phi \to \neg (\neg \phi \to \phi)) \to ((\neg \phi \to \phi) \to \phi)$ Axiom3

*$(\neg \phi \to \phi) \to \phi$  MP 5,6

*$\phi$ MP 1,7
By the Deduction Theorem, this means $\vdash (\neg \phi \to \phi) \to \phi$ (Law of Clavius)
Using Duns Scotus and the Law of Clavius, we can now show that $ \neg \neg \phi \vdash \phi$:


*

*$\neg \neg \phi$ Premise

*$\neg \neg \phi \to (\neg \phi \to \phi)$ Duns Scotus

*$\neg \phi \to \phi$ MP 1,2

*$(\neg \phi \to \phi) \to \phi$ Law of Clavius

*$\phi$ MP 3,4
By the Deduction Theorem, this also means that $\vdash \neg \neg \phi \to \phi$ (DN Elim)
Now we can prove $\vdash \phi \to \neg \neg \phi$ (DN Intro) as well:


*

*$\neg \neg \neg \phi \to \neg \phi$ (DN Elim)

*$(\neg \neg \neg \phi \to \neg \phi) \to (\phi \to \neg \neg \phi)$ Axiom 3

*$\phi \to \neg \neg \phi$ MP 1,2
Now we can derive Modus Tollens: $\phi \to \psi, \neg \psi \vdash \neg \phi$:


*

*$\phi \to \psi$ Premise

*$\neg \psi$ Premise

*$\neg \neg \phi \to \phi$ DN Elim

*$\neg \neg \phi \to \psi$ HS 1,3

*$\psi \to \neg \neg \psi$ DN Intro

*$\neg \neg \phi \to \neg \neg \psi$ HS 4,5

*$(\neg \neg \phi \to \neg \neg \psi) \to (\neg \psi \to \neg \phi)$ Axiom3

*$\neg \psi \to \neg \phi$ MP 6,7

*$\neg \phi$ MP 2,8
By the Deduction Theorem this gives us $\phi \to \psi \vdash \neg \psi \to \neg \phi$ (Contraposition) 
And if we apply the Deduction Theorem on Contradiction, we get $\vdash (\phi \to \psi) \to (\neg \psi \to \neg \phi)$.
Finally, we can prove $\phi \to \psi, \neg \phi \to \psi \vdash \psi$:


*

*$\phi \to \psi$ Premise

*$\neg \phi \to \psi$ Premise

*$\neg \psi \to \neg \phi$ Contraposition 1

*$\neg \psi \to \psi$ HS 2,3

*$(\neg \psi \to \psi) \to \psi$ Law of Clavius

*$\psi$ MP 4,5
Now we can apply the Deduction Theorem twice, and get:
$\vdash (\phi \to \psi) \to ((\neg \phi \to \psi) \to \psi)$
