In a recent preprint, Philip Wadler introduces intuitionistic logic using the comic opera The Gondoliers.
In Gilbert and Sullivan’s The Gondoliers, Casilda is told that as an infant she was married to the heir of the King of Batavia, but that due to a mix-up no one knows which of two individuals, Marco or Giuseppe, is the heir. Alarmed, she wails “Then do you mean to say that I am married to one of two gondoliers, but it is impossible to say which?” To which the response is “Without any doubt of any kind whatever.”
… Intuitionists … insist that a proof of A∨B must show which of A or B holds, and hence they would reject the claim that Casilda is married to Marco or Giuseppe until one of the two was identified as her husband. Perhaps Gilbert and Sullivan anticipated intuitionism, for their story’s outcome is that the heir turns out to be a third individual, Luiz, with whom Casilda is, conveniently, already in love.
It’s Barataria, not Batavia. Stupid auto-correct!
My only issue with intuitionistic logic is the name. Removing the law of excluded middle destroys all my intuition about how logic works.
Aaron: Good point! “Constructive” would be a more intuitive name.
It’s called “intuitionistic logic” because it’s a logical basis for intuitionism. Intuitionism is the philosophical position that mathematics is the product of human thought alone, not the discovery of truths about some objective reality.
This is the basis for the intuitionistic understanding of negation. For a “pre-intuitionist”, ¬A means that A is false. For an intuitionist, ¬A means that A is refutable.