Inconsistency of propositional calculus given $(\neg A \to B) \to (A \to \neg B)$

Question

Consider the classical propositional calculus system (Hilbert system) with three axiom shemes: (1) $A \to (B \to A)$, (2) $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$, (3) $(\neg A \to \neg B) \to (B \to A)$. And you can use modus ponens.

Now we add a new axiom scheme: $(\neg A \to B) \to (A \to \neg B)$.

Sure this is not always true. But how to (formally, in the sense of propositional calculus) prove adding this results an inconsistent system? I.e., you can deduce $A$ and $\neg A$ for some wf.

---

For simplicity, you can use the deduction theorem and the hypothetical syllogism. I need a formal proof obeying the rules of the propositional calculus.

Answer 1

I’m not familiar with Hilbert systems, so apologies for imprecisions.

Suppose we know something:

$A$

Then under your axiom scheme (1) we can legitimately derive:

$\neg A \to A$

Now we apply your new naughty axiom scheme to deduce:

$A \to \neg A$

And since we already know $A$, we can apply modus ponens to this, inferring:

$\neg A$

which is inconsistent with $A$.

Answer 2

Axiom scheme 1 with $\lnot B$ replacing $B:$ $$ A \to (\lnot B \to A). $$ New axiom scheme with letters $A,B$ interchanged: $$(\lnot B \to A) \to (B \to \lnot A).$$ Modus ponens on last two lines: $$A \to (B \to \lnot A).$$ Axiom scheme 3 with $C=\lnot A$ and modus ponens applied to this: $$ (A \to B) \to (A \to \lnot A).$$ In this replace $B$ by $A$: $$(A \to A) \to (A \to \lnot A)$$ At this point I need to invoke $A \to A.$ [I did not get that from Hilbert's axioms, but surely it must follow from them] If I can do that, next apply modus ponens and get to: $$A \to \lnot A.$$ This is a contradiction, since it implies every proposition is false, for example we could replace $A$ here by the entire axiom scheme 1, call that $U,$ then modus ponens, and arrive at a proof that $U$ and $\lnot U$ both hold.