# Derive: $(B\to A)\to(\neg A\to\neg B)$

I've been trying to find a solution to this problem for about two hours. Can't make any more progress as I find it hard to come up with new theorems.

Problem

$$(B \rightarrow A) \rightarrow (\lnot A \rightarrow \lnot B)$$

I need to prove this using the three logical axioms and/or modus ponens. I know how to use all of these, but I'm having difficulty laying out the correct order of and/or correct intermediary steps.

UPDATE

These are the three axioms

1st) $$A \rightarrow (B \rightarrow A)$$ 2nd) $$(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$$ 3rd) $$((\lnot B) \rightarrow (\lnot A)) \rightarrow (A \rightarrow B)$$

-
Can you post the three logical axioms? Thanks. –  Rudy the Reindeer Feb 20 '12 at 7:08
As Carl Mummert explains here: meta.math.stackexchange.com/questions/3555/… There is more than one possible choice of axioms, so you need to specify the three axioms you start with, or the question is ambiguous. –  Andres Caicedo Feb 20 '12 at 7:12
What is your definition of $\lnot A$? Is it $A \to \bot$? –  Zhen Lin Feb 20 '12 at 7:26

the definition of $X\to Y$ is: $Y\lor \neg X$

if you translate the $\neg A\to\neg B$ to its definition you will get the same as for $B \to A$.

-
Thank you. This helped me solve the problem in less than a minute. –  Mark13426 Feb 20 '12 at 7:26
@Mark13426: You said you need to use the three axioms or am I missing something? –  Gigili Feb 20 '12 at 7:34
@Gigili I should have added that translating a proposition to its definition is allowed, which I did according to hassan's answer. At one point in my proof, I had to use the first and second axioms as well as modus ponens. –  Mark13426 Feb 20 '12 at 7:41

Translating $A \to B$ to $\lnot A \lor B$ is, in my opinion, cheating. It's possible to do this directly from the axioms. In fact, you don't even need the third one. Let's call your first axiom K and your second axiom S. We can prove this without the third axiom. Your question amounts to asking the following question in combinatory logic: Can we find an expression in terms of K and S alone for the following lambda expression? $$\lambda x . \, \lambda y . \, \lambda z . \, y (x z)$$ The answer, by general theory, is yes. Explicitly, $$S(K(S(S(K S)K)))K x y z = y (x z)$$

Hence our proof takes the following form. For the sake of brevity, we write $$A = p \to q$$ $$B = \lnot q \to \lnot p$$

and more generally we write $[n]$ for the $n$-th expression in the list below.

1. (Axiom S) $(A \to [11]) \to ([14] \to [15])$
2. (Axiom K) $[11] \to (A \to [11])$
3. (Axiom S) $[10] \to [11]$
4. (Axiom S) $(\lnot q \to [6]) \to ([9] \to [10])$
5. (Axiom K) $[6] \to (\lnot q \to [6])$
6. (Axiom S) $(p \to (q \to \bot)) \to ((p \to q) \to (p \to \bot))$
7. (MP 5, 6) $\lnot q \to [6]$
8. (MP 4, 7) $[9] \to [10]$
9. (Axiom K) $\lnot q \to (p \to \lnot q)$
10. (MP 8, 9) $\lnot q \to (A \to \lnot p)$
11. (MP 3, 10) $(\lnot q \to A) \to B$
12. (MP 2, 11) $A \to [11]$
13. (MP 1, 12) $[14] \to [15]$
14. (Axiom K) $A \to (\lnot q \to A)$
15. (MP 13, 14) $A \to B$

In full gory detail:

1. (Axiom S) $(A \to ((\lnot q \to A) \to B)) \to ((A \to (\lnot q \to A)) \to (A \to B))$
2. (Axiom K) $((\lnot q \to A) \to B) \to (A \to ((\lnot q \to A) \to B))$
3. (Axiom S) $(\lnot q \to (A \to \lnot p)) \to ((\lnot q \to A) \to B)$
4. (Axiom S) $(\lnot q \to ((p \to \lnot q) \to (A \to \lnot p))) \to ((\lnot q \to (p \to \lnot q)) \to (\lnot q \to (A \to \lnot p)))$
5. (Axiom K) $((p \to \lnot q) \to (A \to \lnot p)) \to (\lnot q \to ((p \to \lnot q) \to (A \to \lnot p)))$
6. (Axiom S) $(p \to \lnot q) \to (A \to \lnot p)$
7. (MP 5, 6) $\lnot q \to ((p \to \lnot q) \to (A \to \lnot p))$
8. (MP 4, 7) $(\lnot q \to (p \to \lnot q)) \to (\lnot q \to (A \to \lnot p))$
9. (Axiom K) $\lnot q \to (p \to \lnot q)$
10. (MP 8, 9) $\lnot q \to (A \to \lnot p)$
11. (MP 3, 10) $(\lnot q \to A) \to B$
12. (MP 2, 11) $A \to ((\lnot q \to A) \to B)$
13. (MP 1, 12) $(A \to (\lnot q \to A)) \to (A \to B)$
14. (Axiom K) $A \to (\lnot q \to A)$
15. (MP 13, 14) $A \to B$

Exercise for enthusiasts. Find a shorter proof, or show that this proof is minimal.

-