38
6
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.
Post Rock Garf Hunter
Posted 2018-04-03T15:31:51.943
Reputation: 55 382
8Hold on, let me go fetch my Discrete Math notebook... – mbomb007 – 2018-04-03T15:38:14.753
Is it possible that I studied this during Math undergraduate 20 years ago? If so, I sadly have no recollection :( Looks like an interesting challenge for those with the expertise to take it on... – Digital Trauma – 2018-04-03T19:39:20.913
5@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. – Post Rock Garf Hunter – 2018-04-03T19:42:55.220
Can we use the Deduction Theorem? It's unclear to me how to solve this without using it. It essentially follows from the first axiom, which may be worded "If we have a derivation of Y from a premise X then we are allowed to infer X→Y, provided that the premise X is discharged." Deduction makes things a lot easier, because then you can use assumptions to deduce implications. – mbomb007 – 2018-04-04T16:07:39.110
1@mbomb007 You cannot use the Deduction Theorem, and since the Łukasiewicz system is complete you do not need to use it. – Post Rock Garf Hunter – 2018-04-04T16:20:59.037
1Well at least you didn't limit the axioms to a single, universal schema:
((P → Q) → R) → ((R → P) → (S → P))– mbomb007 – 2018-04-04T16:31:33.8132The 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 – Antony – 2018-04-04T22:05:59.060
1@Antony Thanks for showing me that! I've gone ahead and added it to the resources section of the question. – Post Rock Garf Hunter – 2018-04-04T22:22:37.930
Can we replace ~~A with A? – Acccumulation – 2018-04-04T22:35:32.287
@Acccumulation No you cannot, you can prove that
~~A -> Aand use that but you cannot just substituteAfor~~A. – Post Rock Garf Hunter – 2018-04-04T23:07:31.073@user56656 Yeah, otherwise the proof would be trivial. That's basically what I've been working to prove. Most of my proofs would use deduction, though. Metamath has the way to use modus ponens to prove deduction, so I think in the end I'll have to use that and expand it in every occurrence if I can't work without it. – mbomb007 – 2018-04-04T23:55:34.550
Retina script to add line numbers and tabs to the output of the Prolog program. – mbomb007 – 2018-04-05T13:27:15.527
Wouldn't it be more fun to ask for code to search for short proofs? – Anush – 2018-07-01T19:59:01.643
1@Anush I don't know. Probably not, but that's not this challenge. – Post Rock Garf Hunter – 2018-07-01T20:01:08.917