1
$\begingroup$

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

  • 0
    What is your definition of $\lnot A$? Is it $A \to \bot$?2012-02-20

2 Answers 2

3

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

  • 0
    @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.2012-02-20
3

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.