Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.


$$(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.


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) $$

share|cite|improve this question
Can you post the three logical axioms? Thanks. – Rudy the Reindeer Feb 20 '12 at 7:08
As Carl Mummert explains here:… 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. – Andrés E. 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
up vote 3 down vote accepted

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$.

share|cite|improve this answer
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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.