Proving $\lnot((A\Rightarrow B)\Rightarrow\lnot(B\Rightarrow C))\Rightarrow(A\Rightarrow C)$

Question

I want to find a proof for $\lnot \left( \left( A\Rightarrow B\right) \Rightarrow \lnot \left( B\Rightarrow C\right) \right) \Rightarrow \left( A\Rightarrow C\right)$ with these four axioms:

(A1) $A\Rightarrow \left( B\Rightarrow A\right) $

(A2) $\left( A\Rightarrow \left( B\Rightarrow C\right) \right) \Rightarrow \left( \left( A\Rightarrow B\right) \Rightarrow \left( A\Rightarrow C\right) \right) $

(A3) $(\lnot B\Rightarrow \lnot A)\Rightarrow \left( A\Rightarrow B\right) $

(MP) $\frac{A,A\Rightarrow B}{B}$.

This axioms make a Hilbert system so for rule of inference we have: {A,A→B}⊢B

or MP (Modus Ponens).

Thanks.

Answer 1

If you’re going to prove this using only the axioms and no Deduction Theorem, then you’ll first need to prove

~~A<—>A,

which will allow you to prove that

~(A—>~B)—>A and

~(A—>~B)—>B.

You’ll also need to prove

(B—>C)—>((A—>B)—>(A—>C)), which yields

(A—>B)—>((B—>C)—>(A—>C)).