Propositional calculus axiom the other way around

Question

I have the following axioms of propositional calculus (as well as modus ponens and the deduction theorem if needed):

$$(a \to (b \to a)) \tag1$$ $$ (((a \to (b \to c)) \to ((a \to b) \to (a \to c))) \tag2 $$ $$ ((\neg b \to \neg a) \to (a \to b)) \tag3$$

I'm trying to deduce the last one the other way around (i.e. $((b \to a) \to (\neg a \to \neg b))$) but never manage to get a point... This isn't something I have to do but I feel as though it could be very convenient in my further proofs.

Any help would be greatly appreciated! Thank you!

Answer 1

We need to assume $\neg a$ is an abbreviation for $a \to \bot$; otherwise, there is no way to introduce negations without having an assumption with a negation in it.

First note that $b \to a, a \to \bot, b \vdash \bot$ by two applications of modus ponens. Then we do three applications of the deduction theorem: first we obtain $b \to a, a \to \bot \vdash \neg b$, then $b \to a \vdash \neg a \to \neg b$, and then finally $\vdash (b\to a) \to (\neg a \to \neg b)$.

Answer 2

Undoubtedly, a shorter proof exists, but here's a Prover9 proof:

% -------- Comments from original proof --------

% Proof 1 at 12.05 (+ 0.88) seconds.

% Length of proof is 40.

% Level of proof is 14.

% Maximum clause weight is 24.

% Given clauses 1744.

1 P((x -> y) -> (-y -> -x)) # label(non_clause) # label(goal). [goal].

2 -P(x -> y) | -P(x) | P(y). [assumption].

3 P(x -> (y -> x)). [assumption].

4 P((x -> (y -> z)) -> ((x -> y) -> (x -> z))). [assumption].

5 P((-x -> -y) -> (y -> x)). [assumption].

6 -P((c1 -> c2) -> (-c2 -> -c1)). [deny(1)].

7 P(x -> (y -> (z -> y))). [hyper(2,a,3,a,b,3,a)].

8 P(((x -> (y -> z)) -> (x -> y)) -> ((x -> (y -> z)) -> (x -> z))). [hyper(2,a,4,a,b,4,a)].

9 P(x -> ((y -> (z -> u)) -> ((y -> z) -> (y -> u)))). [hyper(2,a,3,a,b,4,a)].

10 P((x -> y) -> (x -> x)). [hyper(2,a,4,a,b,3,a)].

11 P(((-x -> -y) -> y) -> ((-x -> -y) -> x)). [hyper(2,a,4,a,b,5,a)].

12 P(x -> ((-y -> -z) -> (z -> y))). [hyper(2,a,3,a,b,5,a)].

14 P(x -> (y -> (z -> (u -> z)))). [hyper(2,a,3,a,b,7,a)].

17 P(x -> x). [hyper(2,a,10,a,b,7,a)].

18 P(((x -> y) -> x) -> ((x -> y) -> y)). [hyper(2,a,4,a,b,17,a)].

26 P((x -> ((y -> x) -> z)) -> (x -> z)). [hyper(2,a,8,a,b,7,a)].

44 P((x -> ((y -> (z -> y)) -> u)) -> (x -> u)). [hyper(2,a,8,a,b,14,a)].

48 P(((x -> (y -> z)) -> (((x -> y) -> (x -> z)) -> u)) -> ((x -> (y -> z)) -> u)). [hyper(2,a,8,a,b,9,a)].

71 P((x -> (-y -> -z)) -> (x -> (z -> y))). [hyper(2,a,4,a,b,12,a)].

159 P(-x -> (x -> y)). [hyper(2,a,26,a,b,12,a)].

160 P((x -> y) -> ((z -> x) -> (z -> y))). [hyper(2,a,26,a,b,9,a)].

166 P(x -> (-y -> (y -> z))). [hyper(2,a,3,a,b,159,a)].

197 P(((-x -> (x -> y)) -> z) -> z). [hyper(2,a,18,a,b,166,a)].

815 P(((x -> y) -> z) -> (y -> z)). [hyper(2,a,44,a,b,160,a)].

835 P(x -> (((y -> z) -> u) -> (z -> u))). [hyper(2,a,3,a,b,815,a)].

841 P(x -> ((x -> y) -> y)). [hyper(2,a,815,a,b,18,a)].

842 P(x -> ((-y -> -x) -> y)). [hyper(2,a,815,a,b,11,a)].

918 P((x -> y) -> (x -> ((y -> z) -> z))). [hyper(2,a,160,a,b,841,a)].

1299 P((x -> (-y -> -x)) -> (x -> y)). [hyper(2,a,4,a,b,842,a)].

3180 P((x -> (y -> z)) -> (y -> (x -> z))). [hyper(2,a,48,a,b,835,a)].

4594 P(--x -> x). [hyper(2,a,197,a,b,1299,a)].

4644 P(--x -> ((x -> y) -> y)). [hyper(2,a,918,a,b,4594,a)].

4672 P(x -> --x). [hyper(2,a,5,a,b,4594,a)].

4728 P((x -> y) -> (x -> --y)). [hyper(2,a,160,a,b,4672,a)].

19603 P(x -> ((x -> y) -> --y)). [hyper(2,a,3180,a,b,4728,a)].

19609 P((x -> y) -> (--x -> y)). [hyper(2,a,3180,a,b,4644,a)].

20528 P(--x -> ((x -> y) -> --y)). [hyper(2,a,19609,a,b,19603,a)].

26321 P((x -> y) -> (--x -> --y)). [hyper(2,a,3180,a,b,20528,a)].

27746 P((x -> y) -> (-y -> -x)). [hyper(2,a,71,a,b,26321,a)].

27747 $F. [resolve(27746,a,6,a)].