Well I think it is about time we have another proof-golf 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.
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.
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.
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.
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.
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.
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.
((P → Q) → R) → ((R → P) → (S → P))\$\endgroup\$