38
\$\begingroup\$

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.

Task

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.

\$\endgroup\$
  • 8
    \$\begingroup\$ Hold on, let me go fetch my Discrete Math notebook... \$\endgroup\$ – mbomb007 Apr 3 '18 at 15:38
  • 5
    \$\begingroup\$ @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. \$\endgroup\$ – Sriotchilism O'Zaic Apr 3 '18 at 19:42
  • 1
    \$\begingroup\$ @mbomb007 You cannot use the Deduction Theorem, and since the Łukasiewicz system is complete you do not need to use it. \$\endgroup\$ – Sriotchilism O'Zaic Apr 4 '18 at 16:20
  • 1
    \$\begingroup\$ Well at least you didn't limit the axioms to a single, universal schema: ((P → Q) → R) → ((R → P) → (S → P)) \$\endgroup\$ – mbomb007 Apr 4 '18 at 16:31
  • 2
    \$\begingroup\$ 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 \$\endgroup\$ – Antony Apr 4 '18 at 22:05
25
+1000
\$\begingroup\$

88 82 77 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!

\$\endgroup\$
  • 1
    \$\begingroup\$ Wow, this is amazing. \$\endgroup\$ – Zacharý Jul 14 '18 at 15:08
  • 2
    \$\begingroup\$ 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 \$\endgroup\$ – H.PWiz Jul 14 '18 at 16:35
  • \$\begingroup\$ @H.PWiz Neat, that actually corresponds to a slightly different proof program. Updated. \$\endgroup\$ – Anders Kaseorg Jul 14 '18 at 17:28
  • 1
    \$\begingroup\$ 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)))? \$\endgroup\$ – H.PWiz Jul 14 '18 at 18:45
  • \$\begingroup\$ @H.PWiz That’s good for another −5 along with the free type variable trick. \$\endgroup\$ – Anders Kaseorg Jul 14 '18 at 19:22
24
\$\begingroup\$

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)
\$\endgroup\$
  • \$\begingroup\$ 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? \$\endgroup\$ – caird coinheringaahing Apr 5 '18 at 13:08
  • \$\begingroup\$ @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. \$\endgroup\$ – Sriotchilism O'Zaic Apr 5 '18 at 13:14
  • \$\begingroup\$ 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. \$\endgroup\$ – mbomb007 Apr 5 '18 at 13:39
  • 1
    \$\begingroup\$ 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? \$\endgroup\$ – mbomb007 Apr 5 '18 at 13:47
  • \$\begingroup\$ 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. \$\endgroup\$ – Antony Apr 5 '18 at 16:38
14
\$\begingroup\$

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 enter image description here

png svg

\$\endgroup\$
  • \$\begingroup\$ 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 \$\endgroup\$ – H.PWiz Aug 19 '18 at 21:48
  • \$\begingroup\$ @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.) \$\endgroup\$ – Anders Kaseorg Aug 19 '18 at 22:13
  • \$\begingroup\$ @AndersKaseorg Yeah, I just found that and extracted out the useful theorems: here \$\endgroup\$ – H.PWiz Aug 19 '18 at 22:41
  • \$\begingroup\$ @H.PWiz, sorry, no you didn't suggest that format. I meant that (stripped of the margin) it is compatible with your Prolog verifier. \$\endgroup\$ – Antony Aug 20 '18 at 6:44
  • 1
    \$\begingroup\$ 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 \$\endgroup\$ – Antony Aug 20 '18 at 9:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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