Logical implication

One of the early stumbling blocks people run into when learning traditional Aristotelian logic is the idea that "a false proposition implies any proposition". Let's briefly review material implication, and then I'll talk about what the implications of material implication are to programming.

First off, by a "proposition" I simply mean an expression that has a clear Boolean value. "It's raining". "The streets are wet." "Socrates is a cat." And so on. Propositions can be combined into larger propositions by using the "not", "and" and "or" operations that we are all familiar with. "Socrates is a cat or it is raining" is true if either of its sub-propositions are true, and false otherwise. I won't further explain the meanings of these operations. (Because the audience for this blog is mostly programmers from the C family of languages, I'll use !, & and | symbols for these operations.)

Those operators are all uncontroversial. But we run into big problems when we try to come up with a definition for a proposition of the form "if P then Q", or, as it is traditionally notated, P a' Q. P here is the "antecedent" and Q is the "consequent".

The first thing we have to emphasize is that the implication operation does not suggest that there is a causal relationship. We usually speak of implications that have a causal relationship: "if it is raining then the streets are wet". But the implication proposition "if it is raining then Minerva is a cat" needs to have a truth value irrespective of the fact that there is no obvious causal connection between the weather in Seattle and the name of my elderly cat. (There are logical systems with different kinds of implications that take causality into account, but that's not what I'm talking about today.)

So what then should be the rules for the truth value of P a' Q, given truth values for P and Q?

Plainly if P is true and Q is false then the implication was false. If we have a situation where the antecedent is true but the consequent is false then the implication was a false statement. That is, if some day it is raining but the streets are, bizarrely, not wet, then "if it is raining then the streets are wet" must have been false.

Similarly if P is true and Q is true then the implication was true. If it is the case that it is raining and Minerva is a cat then we can conclude that the implication proposition is true, end of story. Again, remember, the truth of the implication is simply that if the antecedent was true then the consequent turned out to be true, not that there was a causal connection.

That's pretty uncontroversial. The problems arise when the antecedent is false. What is the truth value of P a' Q when P is false? In traditional propositional logic an implication proposition with a false antecedent is considered a true statement, regardless of the truth of the consequent. That is, "if Socrates is immortal then the streets are wet" is a true proposition, regardless of whether the streets are wet or not.

Many people find this unsettling. I did myself for some time. But now it seems very natural to me. Rather than ask about the truth of a proposition, let me tweak it slightly. Suppose I tell you "if it is raining then I wear rubber boots". Under what circumstances could you reasonably call me a liar? If it is raining and I am not wearing rubber boots then clearly I am a liar. If it is raining and I am wearing rubber boots then clearly I am not a liar. If it is not raining then you have nothing upon which to deduce that I am a liar; my statement is true.

So what does this have to do with programming languages?

I now think of material implication like this:

if (p){ Debug.Assert(q); ...}

We will say that the program is correct (true) if the assertion never fires and incorrect (false) if the assertion fires. Under what circumstances would we say that the program is incorrect? Only if p is true and q is false. If p is false then the assertion never fires, and if both are true then the assertion never fires. So again, it makes sense to say that P a' Q is true when P is false.

Why then does C# not have an "implies" operator? Long-time readers will know that I cordially detest questions of the form "why does language X not have feature Y?" because it presupposes that features must be argued against, not argued for. So instead let's consider the feature on its merits and see if there are compelling points for or against the feature.

The first point against is that we can see that P a' Q would simply be a syntactic sugar for !P || Q - of course we do not want to evaluate Q in the case where P is false. Developers can already easily write that; the syntactic sugar is not very sweet.

Second, we'd need to come up with syntax. A design principle of C# is that every punctuation character that is meaningful in the language is found on a standard keyboard, so a' is out. The -> and => syntaxes are already taken. And if we went for --> then we still have the problem of trying to explain this syntax to developers who are unfamiliar with logical implication. And this is hard to do a web search on! And, as commenters point out, p-->q already means "decrement p and compare to q", which was the subject of my April Fools Day post in 2010. The best thing to do would be to simply use implies as the operator, which seems clear, but pretty long.

Third, under what circumstances would you actually use this thing? Pretty much the only situation I can come up with is shortening

if (p) Debug.Assert(q);

to

Debug.Assert(p implies q);

This has a nice property, that p is not evaluated when the assertion is removed! So this is a point in favour. But other than cases like assertions and contracts and whatnot, under what circumstances would you use the operator? It seems to be an operator for annotating programs, not for writing programs.

Finally, we can look at existing programming languages and see what they do. VB 6 and VBScript had an Imp operator. I worked on the VB compiler team for over a year before I even learned that this operator existed, and the only time I ever used it was in test cases for VBScript. It was removed from VB.NET and to my knowledge no one complained. Eiffel has an implies operator, but Eiffel was specifically designed to support contracts as a key language feature, so it makes sense to have this front-and-center; I don't think it makes a lot of sense in C#. Unfortunately this means that we are stuck writing

Debug.Assert(!p || q);

but that is perhaps not a very high price to pay.