A classical logic fairy tale
April 7, 2013(Selinger) Here is a fairy tale: The evil king calls the poor shepherd and gives him these orders. “You must bring me the philosophers stone, or you have to find a way to turn the philosopher’s stone to gold. If you don’t, your head will be taken off tomorrow!” What can the poor shepherd do to save his life?
Hat tip to Chris for originally telling me a different variant of this story. Unfortunately, this quote from Lectures on the Curry-Howard Isomorphism was the only reference I could find. What should the shepherd do? Is there something a little odd about this story?
One approach:
“Well, a real philosopher’s stone can be identified by the fact that if you tap it three times with a spoon, it turns to gold. If you give me a stone like that I will gladly turn it to gold for you.”
If you are in the realm of intuitionistic logic, please turn to page 4. If you are in the realm of classical logic, please turn to page 32.
Page 4: “What do you take me for, a fool?! Off with his head!” The shepherd’s head is chopped off. THE END.
Page 32: “Well, hm, uh. I suppose I did originally ask you to give me a philosopher’s stone. I suppose that will do.” The shepherd returns home, and the evil king never troubles him again. THE END.
(SonOfLilit wins!)
Aha! This old chestnut is like an El Niño over haskell blogs. I love all the variations:
Luke Palmer in 2007:
http://lukepalmer.wordpress.com/2007/10/26/computing-without-a-middle/
Wadler in 2003:
http://parametricity.net/b/2012/04/24/the-devil-of-the-excluded-middle/
> What should the poor shepherd do now?
He should do nothing. The king threatened to take his head on a date which passed years ago. The shepherd is therefore safe from that threat.
Of course, if the king makes new threats, that’s a new problem.
Amusingly, the King’s second demand appears to be a choice between two Cuts – either cut Stone against (Stone –o Gold), or cut Body against Body –o Head. SonOfLit’s classical shepherd creatively escapes via a different, cut-free derivation.
The intuitionist shepherd is effectively doomed – it’s such a sad tail [sic]. If only he could have boxed himself first, he wouldn’t have found his positioning weakening so abruptly. (In another time and place, tyrants of a different type would have bound him in concrete overshoes, with similar consequents.)
( With apologies to logicians, the pun-averse, and the waters so cavalierly muddled )