# (A → B) → (¬B → ¬A)

Well I think it is about time we have another question.

This time we are going to prove the well known logical truth

$$\(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)\$$

To do this we will use Łukasiewicz's third Axiom Schema, an incredibly elegant set of three axioms that are complete over propositional logic.

Here is how it works:

# Axioms

The Łukasiewicz system has three axioms. They are:

$$\\phi\rightarrow(\psi\rightarrow\phi)\$$

$$\(\phi\rightarrow(\psi\rightarrow\chi))\rightarrow((\phi\rightarrow\psi)\rightarrow(\phi\rightarrow\chi))\$$

$$\(\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\phi)\$$

The axioms are universal truths regardless of what we choose for $$\\phi\$$, $$\\psi\$$ and $$\\chi\$$. At any point in the proof we can introduce one of these axioms. When we introduce an axiom you replace each case of $$\\phi\$$, $$\\psi\$$ and $$\\chi\$$, with a "complex expression". A complex expression is any expression made from Atoms, (represented by the letters $$\A\$$-$$\Z\$$), and the operators implies ($$\\rightarrow\$$) and not ($$\\neg\$$).

For example if I wanted to introduce the first axiom (L.S.1) I could introduce

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

or

$$\(A\rightarrow A)\rightarrow(\neg D\rightarrow(A\rightarrow A))\$$

In the first case $$\\phi\$$ was $$\A\$$ and $$\\psi\$$ was $$\B\$$, while in the second case both were more involved expressions. $$\\phi\$$ was $$\(A\rightarrow A)\$$ and $$\\psi\$$ was $$\\neg D\$$.

What substitutions you choose to use will be dependent on what you need in the proof at the moment.

## Modus Ponens

Now that we can introduce statements we need to relate them together to make new statements. The way that this is done in Łukasiewicz's Axiom Schema (L.S) is with Modus Ponens. Modus Ponens allows us to take two statements of the form

$$\\phi\$$

$$\\phi\rightarrow \psi\$$

and instantiate a new statement

$$\\psi\$$

Just like with our Axioms $$\\phi\$$ and $$\\psi\$$ can stand in for any arbitrary statement.

The two statements can be anywhere in the proof, they don't have to be next to each other or any special order.

Your task will be to prove the law of contrapositives. This is the statement

$$\(A\rightarrow B)\rightarrow(\neg B\rightarrow\neg A)\$$

Now you might notice that this is rather familiar, it is an instantiation of the reverse of our third axiom

$$\(\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\phi)\$$

However this is no trivial feat.

## Scoring

Scoring for this challenge is pretty simple, each time you instantiate an axiom counts as a point and each use of modus ponens counts as a point. This is essentially the number of lines in your proof. The goal should be to minimize your score (make it as low as possible).

## Example Proof

Ok now lets use this to construct a small proof. We will prove $$\A\rightarrow A\$$.

Sometimes it is best to work backwards since we know where we want to be we can figure how we might get there. In this case since we want to end with $$\A\rightarrow A\$$ and this is not one of our axioms we know the last step must be modus ponens. Thus the end of our proof will look like

φ
φ → (A → A)
A → A       M.P.


TeX

Where $$\\phi\$$ is an expression we don't yet know the value of. Now we will focus on $$\\phi\rightarrow(A\rightarrow A)\$$. This can be introduced either by modus ponens or L.S.3. L.S.3 requires us to prove $$\(\neg A\rightarrow\neg A)\$$ which seems just as hard as $$\(A\rightarrow A)\$$, so we will go with modus ponens. So now our proof looks like

φ
ψ
ψ → (φ → (A → A))
φ → (A → A)        M.P.
A → A              M.P.


TeX

Now $$\\psi\rightarrow(\phi\rightarrow(A\rightarrow A))\$$ looks a lot like our second axiom L.S.2 so we will fill it in as L.S.2

A → χ
A → (χ → A)
(A → (χ → A)) → ((A → χ) → (A → A)) L.S.2
(A → χ) → (A → A)                   M.P.
A → A                               M.P.


TeX

Now our second statement $$\(A\rightarrow(\chi\rightarrow A))\$$ can pretty clearly be constructed from L.S.1 so we will fill that in as such

A → χ
A → (χ → A)                         L.S.1
(A → (χ → A)) → ((A → χ) → (A → A)) L.S.2
(A → χ) → (A → A)                   M.P.
A → A                               M.P.


TeX

Now we just need to find a $$\\chi\$$ such that we can prove $$\A\rightarrow\chi\$$. This can very easily be done with L.S.1 so we will try that

A → (ω → A)                                     L.S.1
A → ((ω → A) → A)                               L.S.1
(A → ((ω → A) → A)) → ((A → (ω → A)) → (A → A)) L.S.2
(A → (ω → A)) → (A → A)                         M.P.
A → A                                           M.P.


TeX

Now since all of our steps our justified we can fill in $$\\omega\$$, as any statement we want and the proof will be valid. We could choose $$\A\$$ but I will choose $$\B\$$ so that it is clear that it doesn't need to be $$\A\$$.

A → (B → A)                                     L.S.1
A → ((B → A) → A)                               L.S.1
(A → ((B → A) → A)) → ((A → (B → A)) → (A → A)) L.S.2
(A → (B → A)) → (A → A)                         M.P.
A → A                                           M.P.


TeX

Try it online!

And that is a proof.

## Resources

### Verification program

Here is a Prolog program you can use to verify that your proof is in fact valid. Each step should be placed on its own line. -> should be used for implies and - should be used for not, atoms can be represented by any string of alphabetic characters.

### Metamath

Metamath uses the Łukasiewicz system for its proofs in propositional calculus, so you may want to poke around there a bit. They also have a proof of the theorem this challenge asks for which can be found here. There is an explanation here of how to read the proofs.

### The Incredible Proof Machine

@Antony made me aware of a tool called The Incredible Proof machine which allows you to construct proofs in a number of systems using a nice graphical proof system. If you scroll down you will find they support the Łukasiewicz system. So if you are a more visual oriented person you can work on your proof there. Your score will be the number of blocks used minus 1.

• Hold on, let me go fetch my Discrete Math notebook... Apr 3, 2018 at 15:38
• @DigitalTrauma I'm a undergrad now and this was a homework assignment I had (minus the golf part), so its very possible that you may have studied it. I encourage you to give it a try even if you lack "expertise", I think this challenge is approachable even for people who's background is mostly in programming. Apr 3, 2018 at 19:42
• @mbomb007 You cannot use the Deduction Theorem, and since the Łukasiewicz system is complete you do not need to use it. Apr 4, 2018 at 16:20
• Well at least you didn't limit the axioms to a single, universal schema: ((P → Q) → R) → ((R → P) → (S → P)) Apr 4, 2018 at 16:31
• The Incredible Proof Machine is all drag and drop and supports Łukasiewicz's. Scroll almost to the bottom and look for "Hilbert system". For example here is the proof @user56656 gave that A→A Apr 4, 2018 at 22:05

# 888277 72 steps

Thanks to H.PWiz for better combinator conversions that saved 10 steps!

### Explanation

You might be familiar with the Curry–Howard correspondence, in which theorems correspond to types and proofs correspond to programs of those types. The first two axioms in the Łukasiewicz system are actually the K and S combinators, and it’s well known that we can translate lambda calculus expressions into the SK combinatory expressions.

So let’s write down some expressions corresponding to our axioms (the following is valid Haskell syntax, which is convenient because we can quite literally check our proofs using the Haskell compiler):

data Not φ

k :: φ -> (ψ -> φ)
k x _ = x

s :: (φ -> (ψ -> χ)) -> ((φ -> ψ) -> (φ -> χ))
s x y z = x z (y z)

c :: (Not φ -> Not ψ) -> (ψ -> φ)
c = error "non-computational axiom"


Then we can write a proof of the desired statement as a program in terms of c (this part takes a bit of cleverness, but it’s much easier to write this than an 72-line axiomatic proof):

pf :: (a -> b) -> (Not b -> Not a)
pf x y = c (\z -> c (\_ -> y) (x (c (c (\_ -> z)) x))) k


and convert it into an SK combinatory expression:

pf' :: (a -> b) -> (Not b -> Not a)
pf' =
s (k (s (k (s c (k k)))))
(s (k (s (s (k s) (s (k k) (s (k c) k)))))
(s (k k) (s (k (s s (s (s (k c) (s (k c) k))))) k)))


The 17 k, 16 s, and 4 c combinators above correspond to the 16 LS1, 16 LS2, and 4 LS3 invocations in the proof below, and the 38 applications of a function to a value above correspond to the 38 MP invocations below.

Why only 16 LS1 invocations? It turns out one of the k combinators above has a free type variable, and instantiating it carefully turns it into a duplicate of another one that has already been derived.

### The proof

1. (A → B) → (¬¬A → (A → B)) LS1
2. ¬¬A → (¬¬(A → B) → ¬¬A) LS1
3. (¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B)) LS3
4. ((¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B))) → (¬¬A → ((¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B)))) LS1
5. ¬¬A → ((¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B))) MP 4,3
6. (¬¬A → ((¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B)))) → ((¬¬A → (¬¬(A → B) → ¬¬A)) → (¬¬A → (¬A → ¬(A → B)))) LS2
7. (¬¬A → (¬¬(A → B) → ¬¬A)) → (¬¬A → (¬A → ¬(A → B))) MP 6,5
8. ¬¬A → (¬A → ¬(A → B)) MP 7,2
9. (¬A → ¬(A → B)) → ((A → B) → A) LS3
10. ((¬A → ¬(A → B)) → ((A → B) → A)) → (¬¬A → ((¬A → ¬(A → B)) → ((A → B) → A))) LS1
11. ¬¬A → ((¬A → ¬(A → B)) → ((A → B) → A)) MP 10,9
12. (¬¬A → ((¬A → ¬(A → B)) → ((A → B) → A))) → ((¬¬A → (¬A → ¬(A → B))) → (¬¬A → ((A → B) → A))) LS2
13. (¬¬A → (¬A → ¬(A → B))) → (¬¬A → ((A → B) → A)) MP 12,11
14. ¬¬A → ((A → B) → A) MP 13,8
15. (¬¬A → ((A → B) → A)) → ((¬¬A → (A → B)) → (¬¬A → A)) LS2
16. (¬¬A → (A → B)) → (¬¬A → A) MP 15,14
17. (¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)) LS2
18. ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))) → (((¬¬A → (A → B)) → (¬¬A → A)) → ((¬¬A → (A → B)) → (¬¬A → B))) LS2
19. ((¬¬A → (A → B)) → (¬¬A → A)) → ((¬¬A → (A → B)) → (¬¬A → B)) MP 18,17
20. (¬¬A → (A → B)) → (¬¬A → B) MP 19,16
21. ((¬¬A → (A → B)) → (¬¬A → B)) → ((A → B) → ((¬¬A → (A → B)) → (¬¬A → B))) LS1
22. (A → B) → ((¬¬A → (A → B)) → (¬¬A → B)) MP 21,20
23. ((A → B) → ((¬¬A → (A → B)) → (¬¬A → B))) → (((A → B) → (¬¬A → (A → B))) → ((A → B) → (¬¬A → B))) LS2
24. ((A → B) → (¬¬A → (A → B))) → ((A → B) → (¬¬A → B)) MP 23,22
25. (A → B) → (¬¬A → B) MP 24,1
26. (¬¬A → B) → (¬B → (¬¬A → B)) LS1
27. ((¬¬A → B) → (¬B → (¬¬A → B))) → ((A → B) → ((¬¬A → B) → (¬B → (¬¬A → B)))) LS1
28. (A → B) → ((¬¬A → B) → (¬B → (¬¬A → B))) MP 27,26
29. ((A → B) → ((¬¬A → B) → (¬B → (¬¬A → B)))) → (((A → B) → (¬¬A → B)) → ((A → B) → (¬B → (¬¬A → B)))) LS2
30. ((A → B) → (¬¬A → B)) → ((A → B) → (¬B → (¬¬A → B))) MP 29,28
31. (A → B) → (¬B → (¬¬A → B)) MP 30,25
32. ¬B → (¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) LS1
33. (¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) LS3
34. ((¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ((¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) LS1
35. ¬B → ((¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 34,33
36. (¬B → ((¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((¬B → (¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B)) → (¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) LS2
37. (¬B → (¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B)) → (¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 36,35
38. ¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) MP 37,32
39. (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) LS1
40. ((B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → (¬B → ((B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS1
41. ¬B → ((B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 40,39
42. (¬B → ((B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) → ((¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS2
43. (¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 42,41
44. ¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 43,38
45. (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) LS2
46. ((¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → (¬B → ((¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS1
47. ¬B → ((¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 46,45
48. (¬B → ((¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) → ((¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → (¬B → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS2
49. (¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → (¬B → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 48,47
50. ¬B → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 49,44
51. (¬B → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) LS2
52. (¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 51,50
53. ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((A → B) → ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS1
54. (A → B) → ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 53,52
55. ((A → B) → ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) → (((A → B) → (¬B → (¬¬A → B))) → ((A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS2
56. ((A → B) → (¬B → (¬¬A → B))) → ((A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 55,54
57. (A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 56,31
58. (¬¬A → (¬¬(A → B) → ¬¬A)) → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (¬¬(A → B) → ¬¬A))) LS1
59. (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (¬¬(A → B) → ¬¬A)) MP 58,2
60. (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ((¬¬A → (¬¬(A → B) → ¬¬A)) → ¬A) LS3
61. ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ((¬¬A → (¬¬(A → B) → ¬¬A)) → ¬A)) → (((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (¬¬(A → B) → ¬¬A))) → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A)) LS2
62. ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (¬¬(A → B) → ¬¬A))) → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A) MP 61,60
63. (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A MP 62,59
64. ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A) → (¬B → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A)) LS1
65. ¬B → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A) MP 64,63
66. (¬B → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A)) → ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A)) LS2
67. (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A) MP 66,65
68. ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A)) → ((A → B) → ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A))) LS1
69. (A → B) → ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A)) MP 68,67
70. ((A → B) → ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A))) → (((A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((A → B) → (¬B → ¬A))) LS2
71. ((A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((A → B) → (¬B → ¬A)) MP 70,69
72. (A → B) → (¬B → ¬A) MP 71,57

Try it online!

• Wow, this is amazing. Jul 14, 2018 at 15:08
• I can't tell if it's shorter in steps, and have to go right now. But I got s(s(k s)(s(k(s(k c)))(s(k(s(s(k s)(s(k k)(s(k c)k)))))(s(k k)(s(k(s s(s(s(k c)(s(k c)k)))))k)))))k  which is similar to yours but with a slightly shorter ending Jul 14, 2018 at 16:35
• @H.PWiz Neat, that actually corresponds to a slightly different proof program. Updated. Jul 14, 2018 at 17:28
• How about s(k(s(k(s c(k s)))))(s(k(s(s(k s)(s(k k)(s(k c)k)))))(s(k k)(s(k(s s(s(s(k c)(s(k c)k)))))k)))? Jul 14, 2018 at 18:45
• @H.PWiz That’s good for another −5 along with the free type variable trick. Jul 14, 2018 at 19:22

# 91 Steps

Full Proof:

1. (A → B) → (¬¬A → (A → B)) LS1
2. (¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)) LS2
3. ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))) → ((A → B) → ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)))) LS1
4. (A → B) → ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))) MP 3,2
5. ((A → B) → ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)))) → (((A → B) → (¬¬A → (A → B))) → ((A → B) → ((¬¬A → A) → (¬¬A → B)))) LS2
6. ((A → B) → (¬¬A → (A → B))) → ((A → B) → ((¬¬A → A) → (¬¬A → B))) MP 5,4
7. (A → B) → ((¬¬A → A) → (¬¬A → B)) MP 6,1
8. ¬A → (¬¬(B → (¬A → A)) → ¬A) LS1
9. (¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A))) LS3
10. ((¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A)))) → (¬A → ((¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A))))) LS1
11. ¬A → ((¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A)))) MP 10,9
12. (¬A → ((¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A))))) → ((¬A → (¬¬(B → (¬A → A)) → ¬A)) → (¬A → (A → ¬(B → (¬A → A))))) LS2
13. (¬A → (¬¬(B → (¬A → A)) → ¬A)) → (¬A → (A → ¬(B → (¬A → A)))) MP 12,11
14. ¬A → (A → ¬(B → (¬A → A))) MP 13,8
15. (¬A → (A → ¬(B → (¬A → A)))) → ((¬A → A) → (¬A → ¬(B → (¬A → A)))) LS2
16. (¬A → A) → (¬A → ¬(B → (¬A → A))) MP 15,14
17. (¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A) LS3
18. ((¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A)) → ((¬A → A) → ((¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A))) LS1
19. (¬A → A) → ((¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A)) MP 18,17
20. ((¬A → A) → ((¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A))) → (((¬A → A) → (¬A → ¬(B → (¬A → A)))) → ((¬A → A) → ((B → (¬A → A)) → A))) LS2
21. ((¬A → A) → (¬A → ¬(B → (¬A → A)))) → ((¬A → A) → ((B → (¬A → A)) → A)) MP 20,19
22. (¬A → A) → ((B → (¬A → A)) → A) MP 21,16
23. (¬A → A) → (B → (¬A → A)) LS1
24. ((¬A → A) → ((B → (¬A → A)) → A)) → (((¬A → A) → (B → (¬A → A))) → ((¬A → A) → A)) LS2
25. ((¬A → A) → (B → (¬A → A))) → ((¬A → A) → A) MP 24,22
26. (¬A → A) → A MP 25,23
27. ¬¬A → (¬A → ¬¬A) LS1
28. (¬A → ¬¬A) → (¬A → A) LS3
29. ((¬A → ¬¬A) → (¬A → A)) → (¬¬A → ((¬A → ¬¬A) → (¬A → A))) LS1
30. ¬¬A → ((¬A → ¬¬A) → (¬A → A)) MP 29,28
31. (¬¬A → ((¬A → ¬¬A) → (¬A → A))) → ((¬¬A → (¬A → ¬¬A)) → (¬¬A → (¬A → A))) LS2
32. (¬¬A → (¬A → ¬¬A)) → (¬¬A → (¬A → A)) MP 31,30
33. ¬¬A → (¬A → A) MP 32,27
34. ((¬A → A) → A) → (¬¬A → ((¬A → A) → A)) LS1
35. ¬¬A → ((¬A → A) → A) MP 34,26
36. (¬¬A → ((¬A → A) → A)) → ((¬¬A → (¬A → A)) → (¬¬A → A)) LS2
37. (¬¬A → (¬A → A)) → (¬¬A → A) MP 36,35
38. ¬¬A → A MP 37,33
39. (¬¬A → A) → ((A → B) → (¬¬A → A)) LS1
40. (A → B) → (¬¬A → A) MP 39,38
41. ((A → B) → ((¬¬A → A) → (¬¬A → B))) → (((A → B) → (¬¬A → A)) → ((A → B) → (¬¬A → B))) LS2
42. ((A → B) → (¬¬A → A)) → ((A → B) → (¬¬A → B)) MP 41,7
43. (A → B) → (¬¬A → B) MP 42,40
44. ¬¬B → (¬¬(B → (¬¬B → ¬B)) → ¬¬B) LS1
45. (¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B))) LS3
46. ((¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B)))) → (¬¬B → ((¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B))))) LS1
47. ¬¬B → ((¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B)))) MP 46,45
48. (¬¬B → ((¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B))))) → ((¬¬B → (¬¬(B → (¬¬B → ¬B)) → ¬¬B)) → (¬¬B → (¬B → ¬(B → (¬¬B → ¬B))))) LS2
49. (¬¬B → (¬¬(B → (¬¬B → ¬B)) → ¬¬B)) → (¬¬B → (¬B → ¬(B → (¬¬B → ¬B)))) MP 48,47
50. ¬¬B → (¬B → ¬(B → (¬¬B → ¬B))) MP 49,44
51. (¬¬B → (¬B → ¬(B → (¬¬B → ¬B)))) → ((¬¬B → ¬B) → (¬¬B → ¬(B → (¬¬B → ¬B)))) LS2
52. (¬¬B → ¬B) → (¬¬B → ¬(B → (¬¬B → ¬B))) MP 51,50
53. (¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B) LS3
54. ((¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B)) → ((¬¬B → ¬B) → ((¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B))) LS1
55. (¬¬B → ¬B) → ((¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B)) MP 54,53
56. ((¬¬B → ¬B) → ((¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B))) → (((¬¬B → ¬B) → (¬¬B → ¬(B → (¬¬B → ¬B)))) → ((¬¬B → ¬B) → ((B → (¬¬B → ¬B)) → ¬B))) LS2
57. ((¬¬B → ¬B) → (¬¬B → ¬(B → (¬¬B → ¬B)))) → ((¬¬B → ¬B) → ((B → (¬¬B → ¬B)) → ¬B)) MP 56,55
58. (¬¬B → ¬B) → ((B → (¬¬B → ¬B)) → ¬B) MP 57,52
59. (¬¬B → ¬B) → (B → (¬¬B → ¬B)) LS1
60. ((¬¬B → ¬B) → ((B → (¬¬B → ¬B)) → ¬B)) → (((¬¬B → ¬B) → (B → (¬¬B → ¬B))) → ((¬¬B → ¬B) → ¬B)) LS2
61. ((¬¬B → ¬B) → (B → (¬¬B → ¬B))) → ((¬¬B → ¬B) → ¬B) MP 60,58
62. (¬¬B → ¬B) → ¬B MP 61,59
63. ¬¬¬B → (¬¬B → ¬¬¬B) LS1
64. (¬¬B → ¬¬¬B) → (¬¬B → ¬B) LS3
65. ((¬¬B → ¬¬¬B) → (¬¬B → ¬B)) → (¬¬¬B → ((¬¬B → ¬¬¬B) → (¬¬B → ¬B))) LS1
66. ¬¬¬B → ((¬¬B → ¬¬¬B) → (¬¬B → ¬B)) MP 65,64
67. (¬¬¬B → ((¬¬B → ¬¬¬B) → (¬¬B → ¬B))) → ((¬¬¬B → (¬¬B → ¬¬¬B)) → (¬¬¬B → (¬¬B → ¬B))) LS2
68. (¬¬¬B → (¬¬B → ¬¬¬B)) → (¬¬¬B → (¬¬B → ¬B)) MP 67,66
69. ¬¬¬B → (¬¬B → ¬B) MP 68,63
70. ((¬¬B → ¬B) → ¬B) → (¬¬¬B → ((¬¬B → ¬B) → ¬B)) LS1
71. ¬¬¬B → ((¬¬B → ¬B) → ¬B) MP 70,62
72. (¬¬¬B → ((¬¬B → ¬B) → ¬B)) → ((¬¬¬B → (¬¬B → ¬B)) → (¬¬¬B → ¬B)) LS2
73. (¬¬¬B → (¬¬B → ¬B)) → (¬¬¬B → ¬B) MP 72,71
74. ¬¬¬B → ¬B MP 73,69
75. (¬¬¬B → ¬B) → (B → ¬¬B) LS3
76. B → ¬¬B MP 75,74
77. (B → ¬¬B) → (¬¬A → (B → ¬¬B)) LS1
78. ¬¬A → (B → ¬¬B) MP 77,76
79. (¬¬A → (B → ¬¬B)) → ((¬¬A → B) → (¬¬A → ¬¬B)) LS2
80. (¬¬A → B) → (¬¬A → ¬¬B) MP 79,78
81. ((¬¬A → B) → (¬¬A → ¬¬B)) → ((A → B) → ((¬¬A → B) → (¬¬A → ¬¬B))) LS1
82. (A → B) → ((¬¬A → B) → (¬¬A → ¬¬B)) MP 81,80
83. ((A → B) → ((¬¬A → B) → (¬¬A → ¬¬B))) → (((A → B) → (¬¬A → B)) → ((A → B) → (¬¬A → ¬¬B))) LS2
84. ((A → B) → (¬¬A → B)) → ((A → B) → (¬¬A → ¬¬B)) MP 83,82
85. (A → B) → (¬¬A → ¬¬B) MP 84,43
86. (¬¬A → ¬¬B) → (¬B → ¬A) LS3
87. ((¬¬A → ¬¬B) → (¬B → ¬A)) → ((A → B) → ((¬¬A → ¬¬B) → (¬B → ¬A))) LS1
88. (A → B) → ((¬¬A → ¬¬B) → (¬B → ¬A)) MP 87,86
89. ((A → B) → ((¬¬A → ¬¬B) → (¬B → ¬A))) → (((A → B) → (¬¬A → ¬¬B)) → ((A → B) → (¬B → ¬A))) LS2
90. ((A → B) → (¬¬A → ¬¬B)) → ((A → B) → (¬B → ¬A)) MP 89,88
91. (A → B) → (¬B → ¬A) MP 90,85


Try it online!

A more human-readable version using 5 lemmas:

Lemma 1: From A → B and B → C, instantiate A → C. (5 steps)

1. B → C                                         given
2. (B → C) → (A → (B → C))                       L.S.1
3. A → (B → C)                                   M.P. (1,2)
4. (A → (B → C)) → ((A → B) → (A → C))           L.S.2
5. (A → B) → (A → C)                             M.P. (3,4)
6. A → B                                         given
7. A → C                                         M.P. (6,5)

Lemma 2: ¬A → (A → B) (7 steps)

1. ¬A → (¬B → ¬A)                                L.S.1
2. (¬B → ¬A) → (A → B)                           L.S.3
3. ¬A → (A → B)                                  Lemma 1 (1,2)

Lemma 3: From A → (B → C) and A → B, instantiate A → C. (3 steps)

1. A → (B → C)                                   given
2. (A → (B → C)) → ((A → B) → (A → C))           L.S.2
3. (A → B) → (A → C)                             M.P. (1,2)
4. A → B                                         given
5. A → C                                         M.P. (4,3)

Lemma 4: ¬¬A → A (31 steps)

1. ¬A → (A → ¬(B → (¬A → A)))                    Lemma 2
2. (¬A → (A → ¬(B → (¬A → A)))) →
((¬A → A) → (¬A → ¬(B → (¬A → A))))           L.S.2
3. (¬A → A) → (¬A → ¬(B → (¬A → A)))             M.P. (1,2)
4. (¬A → ¬(B → (¬A → A))) →((B → (¬A → A)) → A)  L.S.3
5. (¬A → A) → ((B → (¬A → A)) → A)               Lemma 1 (3,4)
6. (¬A → A) → (B → (¬A → A))                     L.S.1
7. (¬A → A) → A                                  Lemma 3 (5,6)
8. ¬¬A → (¬A → A)                                Lemma 2
9. ¬¬A → A                                       Lemma 1 (8,7)

Lemma 5: (A → B) → (¬¬A → B) (43 steps)

1. (A → B) → (¬¬A → (A → B))                     L.S.1
2. (¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))     L.S.2
3. (A → B) → ((¬¬A → A) → (¬¬A → B))             Lemma 1 (1,2)
4. ¬¬A → A                                       Lemma 4
5. (¬¬A → A) → ((A → B) → (¬¬A → A))             L.S.1
6. (A → B) → (¬¬A → A)                           M.P. (4,5)
7. (A → B) → (¬¬A → B)                           Lemma 3 (3,6)

Theorem: (A → B) → (¬B → ¬A)

1. (A → B) → (¬¬A → B)                           Lemma 5
2. ¬¬¬B → ¬B                                     Lemma 4
3. (¬¬¬B → ¬B) → (B → ¬¬B)                       L.S.3
4. B → ¬¬B                                       M.P. (2,3)
5. (B → ¬¬B) → (¬¬A → (B → ¬¬B))                 L.S.1
6. ¬¬A → (B → ¬¬B)                               M.P. (4,5)
7. (¬¬A → (B → ¬¬B)) → ((¬¬A → B) → (¬¬A → ¬¬B)) L.S.2
8. (¬¬A → B) → (¬¬A → ¬¬B)                       M.P. (6,7)
9. (A → B) → (¬¬A → ¬¬B)                         Lemma 1 (1,8)
10.(¬¬A → ¬¬B) → (¬B → ¬A)                       L.S.3
11.(A → B) → (¬B → ¬A)                           Lemma 1 (9,10)

• Welcome to the site and impressive answer! Have you verified your answer with the Prolog script? If so, would you mind including a link to said verification? Apr 5, 2018 at 13:08
• @cairdcoinheringaahing I've added a tio link to the prolog script to the answer so that it can be verified (it does work). Usually I would comment the link but the link is too long to fit in a comment. Apr 5, 2018 at 13:14
• That's basically the proof I was in the process of making, except that you used different lemmas. I used the Principle of Identity. Also, I hadn't proved Double Negation Elimination yet, because the proof of that I was creating required Contradiction Realization. Apr 5, 2018 at 13:39
• Would you be able to cut out Lemma 5 and instead prove and use the Substitution Theorem to get from (¬¬A → ¬¬B) → (¬B → ¬A) to (A → B) → (¬B → ¬A) in fewer steps? Apr 5, 2018 at 13:47
• I think the very first step is redundant? I couldn't find anything referencing it so I tried running it on TIO without that line and didn't get any "Invalid step" warnings. Apr 5, 2018 at 16:38

59 steps

Norman Megill, author of Metamath has told me about a 59 step proof, which I'm going to post here in this community wiki. The original can be found in theorem 2.16 on this page.

http://us.metamath.org/mmsolitaire/pmproofs.txt

Norm says: This page would provide plenty of challenges for you to beat!

Here's the proof

((P -> Q) -> (~ Q -> ~ P)); ! *2.16
((P -> Q) -> (~ Q -> ~ P)); ! Result of proof
DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311
; ! 59 steps


The proof is in Polish notation, so it starts from the conclusion and continues backwards until every term has been satisified by an axiom. The character mapping is as follows: "1" is LS axiom 1, "2" is LS axiom 2, "3" is LS axiom 3, and "D" is Modus Ponens.

Here's the proof in @W-W's suggested format

01 ax-1          $a |- ( ¬ ¬ ¬ B → ( ¬ B → ¬ ¬ ¬ B ) ) 02 ax-1$a |- ( ¬ ¬ ¬ B → ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) )
03 ax-3          $a |- ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) 04 ax-1$a |- ( ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) → ( ¬ ¬ ¬ B → ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) ) )
05 3,4 ax-mp     $a |- ( ¬ ¬ ¬ B → ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) ) 06 ax-2$a |- ( ( ¬ ¬ ¬ B → ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) ) → ( ( ¬ ¬ ¬ B → ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) ) → ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) ) )
07 5,6 ax-mp     $a |- ( ( ¬ ¬ ¬ B → ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) ) → ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) ) 08 2,7 ax-mp$a |- ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) )
09 ax-3          $a |- ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) 10 ax-1$a |- ( ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) → ( ¬ ¬ ¬ B → ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) ) )
11 9,10 ax-mp    $a |- ( ¬ ¬ ¬ B → ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) ) 12 ax-2$a |- ( ( ¬ ¬ ¬ B → ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) ) → ( ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) → ( ¬ ¬ ¬ B → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) ) )
13 11,12 ax-mp   $a |- ( ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) → ( ¬ ¬ ¬ B → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) ) 14 8,13 ax-mp$a |- ( ¬ ¬ ¬ B → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) )
15 ax-2          $a |- ( ( ¬ ¬ ¬ B → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) → ( ( ¬ ¬ ¬ B → ( ¬ B → ¬ ¬ ¬ B ) ) → ( ¬ ¬ ¬ B → ¬ B ) ) ) 16 14,15 ax-mp$a |- ( ( ¬ ¬ ¬ B → ( ¬ B → ¬ ¬ ¬ B ) ) → ( ¬ ¬ ¬ B → ¬ B ) )
17 1,16 ax-mp    $a |- ( ¬ ¬ ¬ B → ¬ B ) 18 ax-3$a |- ( ( ¬ ¬ ¬ B → ¬ B ) → ( B → ¬ ¬ B ) )
19 17,18 ax-mp   $a |- ( B → ¬ ¬ B ) 20 ax-1$a |- ( ( B → ¬ ¬ B ) → ( A → ( B → ¬ ¬ B ) ) )
21 19,20 ax-mp   $a |- ( A → ( B → ¬ ¬ B ) ) 22 ax-2$a |- ( ( A → ( B → ¬ ¬ B ) ) → ( ( A → B ) → ( A → ¬ ¬ B ) ) )
23 21,22 ax-mp   $a |- ( ( A → B ) → ( A → ¬ ¬ B ) ) 24 ax-1$a |- ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ( A → ¬ ¬ B ) ) )
25 ax-1          $a |- ( ¬ ¬ A → ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) ) 26 ax-3$a |- ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) )
27 ax-1          $a |- ( ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) → ( ¬ ¬ A → ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) ) ) 28 26,27 ax-mp$a |- ( ¬ ¬ A → ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) )
29 ax-2          $a |- ( ( ¬ ¬ A → ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) ) → ( ( ¬ ¬ A → ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) ) → ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) ) ) 30 28,29 ax-mp$a |- ( ( ¬ ¬ A → ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) ) → ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) )
31 25,30 ax-mp   $a |- ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) 32 ax-3$a |- ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) )
33 ax-1          $a |- ( ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) ) → ( ¬ ¬ A → ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) ) ) ) 34 32,33 ax-mp$a |- ( ¬ ¬ A → ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) ) )
35 ax-2          $a |- ( ( ¬ ¬ A → ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) ) ) → ( ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) → ( ¬ ¬ A → ( ( A → ¬ ¬ B ) → A ) ) ) ) 36 34,35 ax-mp$a |- ( ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) → ( ¬ ¬ A → ( ( A → ¬ ¬ B ) → A ) ) )
37 31,36 ax-mp   $a |- ( ¬ ¬ A → ( ( A → ¬ ¬ B ) → A ) ) 38 ax-2$a |- ( ( ¬ ¬ A → ( ( A → ¬ ¬ B ) → A ) ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → A ) ) )
39 37,38 ax-mp   $a |- ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → A ) ) 40 ax-2$a |- ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ( ¬ ¬ A → A ) → ( ¬ ¬ A → ¬ ¬ B ) ) )
41 ax-2          $a |- ( ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ( ¬ ¬ A → A ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) → ( ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → A ) ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) ) 42 40,41 ax-mp$a |- ( ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → A ) ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) )
43 39,42 ax-mp   $a |- ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) 44 ax-1$a |- ( ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) )
45 43,44 ax-mp   $a |- ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) 46 ax-2$a |- ( ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) → ( ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ( A → ¬ ¬ B ) ) ) → ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) )
47 45,46 ax-mp   $a |- ( ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ( A → ¬ ¬ B ) ) ) → ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) 48 24,47 ax-mp$a |- ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) )
49 ax-3          $a |- ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) 50 ax-1$a |- ( ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) → ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) )
51 49,50 ax-mp   $a |- ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) 52 ax-2$a |- ( ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) → ( ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) )
53 51,52 ax-mp   $a |- ( ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) 54 48,53 ax-mp$a |- ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) )
55 ax-1          $a |- ( ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) → ( ( A → B ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) ) 56 54,55 ax-mp$a |- ( ( A → B ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) )
57 ax-2          $a |- ( ( ( A → B ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) → ( ( ( A → B ) → ( A → ¬ ¬ B ) ) → ( ( A → B ) → ( ¬ B → ¬ A ) ) ) ) 58 56,57 ax-mp$a |- ( ( ( A → B ) → ( A → ¬ ¬ B ) ) → ( ( A → B ) → ( ¬ B → ¬ A ) ) )
59 23,58 ax-mp   \$a |- ( ( A → B ) → ( ¬ B → ¬ A ) )


Try it online!

Here it is in The Incredible Proof Machine

• I don't remember suggesting such a format... For what it's worth, the corresponding sk expression is s(k(s(k c)(s(k(s s(s(s(k c)(s(k c)k)))))k)))(s(k(c(s(s(k c)(s(k c)k))k)))). I don't have a way to convert that back to lambdas though Aug 19, 2018 at 21:48
• @H.PWiz It’s \x -> c (\y -> c (\z -> c (c (\_ -> z)) (\_ -> z)) (x (c (c (\_ -> y)) (\z -> c (\t -> c (c (\_ -> t)) (\_ -> t)) (x z))))). (Probably not what you’d write if you were approaching it from that direction.) Aug 19, 2018 at 22:13
• @AndersKaseorg Yeah, I just found that and extracted out the useful theorems: here Aug 19, 2018 at 22:41
• @H.PWiz, sorry, no you didn't suggest that format. I meant that (stripped of the margin) it is compatible with your Prolog verifier. Aug 20, 2018 at 6:44
• I'm sorry for mistaking you for OP, @H.PWiz I'm afraid your username looked like one in the succession of WW's many names i.imgur.com/VoSVoqI.png Aug 20, 2018 at 9:45