Logical formula deducing

Question

I'm trying to find a way how to deduce a certain formula in Logical System which has only $(\lnot, \to )$ - negation and implication functions and these axioms:

Ax1: $X\to (Y\to X)$

Ax2: $((X\to Y)\to (\lnot Y\to\lnot X))$

Ax3: $(X\to (Y\to Z))\to((X\to Y)\to (X\to Z))$

and there is a rule - Modus Ponens of course

Formula: $((\lnot k\to k)\to k)\to (\lnot (k\to k)\to \lnot k)$

I was trying to start with axiom 2 since it's very similar to desired formula ($X=k, Y=(k\to k)$) but no success.

Do you know how to do that?

Answer 1

Here is a derivation:

1. $(k\to (k\to k)) \to (\neg(k\to k) \to \neg k)$

   by Ax.2, with $X = k, Y = (k\to k)$.

2. $k\to(k\to k)$

   by Ax.1, with $X=k, Y=k$.

3. $(\neg(k\to k) \to \neg k)$

   by 1. and 2. via MP.

4. $(\neg(k\to k) \to \neg k) \to [((\neg k\to k)\to k) \to (\neg(k\to k) \to \neg k)]$

   Ax.1 with $X = (\neg(k\to k) \to \neg k) =$ 3., $Y = ((\neg k\to k)\to k)$.

5. $((\neg k\to k)\to k) \to (\neg(k\to k) \to \neg k)$

   by 3. and 4. via MP.