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 → 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 → 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 → 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 → 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 → 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 → 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.
Fabulous adventures in coding 
Many languages have this:
something if something;
Used like this:
Debug.Assert(q) if (p);
Actually the “–>” syntax is already taken too:
int counter = 10;
while (counter–>0) // same as: if ((counter–) > 0)
{
// do stuff
}
The font (at least the one I’m seeing) runs the two dashes together. I meant: while (counter – – > 0)
http://blogs.msdn.com/b/ericlippert/archive/2010/04/01/somelastminutefeatures.aspx
🙂
Another use case:
int someInput = …;
bool shouldDoSomething = true &&
(someInput == 1) implies true &&
(someInput == 2) implies false &&
(someInput == 3) implies (someThingElse == “x”);
So its useful for case analysis. Note, that the conditions on the left side might be arbitrary and complicated so that switch/match do not necessarily apply.
I remember learning about this while studying mathematics in college. My track was theory-heavy, so this was essential to learn as this is the format in which mathematical theorems are stated. It didn’t really confuse me all that much (maybe I just had a decent professor). It just seems natural to say these statements combine to show that a theorem is true:
if p, then q.
if !p, then q is irrelevant.
while this one can be used to prove it is false:
if p, then !q.
“If two times two is five, then I’m the Pope”. 🙂
Exactly.
It is, for large values of 2. Liar!
I don’t know why, but this really cracked me up. Large values of 2. Classic.
If you know about implication, then having to rewrite it as ~p || q is no biggie. Unfortunately, people who don’t immediately grasp the idiom may spend some time reasoning it out (“so either p must be false, or p must be true but then q must be true as well”) which can easily trip them up if p and q aren’t simple expressions. If you can immediately read it as “if p then q must hold and if not p I don’t care”, that helps a lot.
“But other than cases like assertions and contracts and whatnot, under what circumstances would you use the operator?”
Every so often it’s useful if you can’t use an if — I know I’ve used it multiple times in SQL for writing constraints. That is, the form “NOT P OR Q” of course, since SQL has no IMPLIES either. Again, the operator itself is not really necessary, but knowing about implication does help with reading such expressions (and simplifying others).
I guess you could see a check constraint as an “assertion”, so it’s not a good counterexample. I checked two good-sized projects but couldn’t find any instance of ~p || q used as implication, so I guess that’s telling.
The mnemonic for memorizing “p=>q === !p | q” is “If you’re a real man, then wrestle a bear == Wrestle a bear, or you’re not a real man” or something like this.
A practical (ish) use for an implies operator…
if ( ! ThingMustBeValid || ThingIsValid)
/* Everything is fine. Either the thing is valid or it doesn’t matter. */
else
/* Error. Thing is not valid but must be. */
(PS. In the real world, I’d rename that first item to “ThingValidationIsOptional” and reverse its true/false meaning.)
I learned Visual Basic 17 years ago, yet, I only learned “Imp” operator exists today, thank you for this extra contribution for my knowledge.
For me the most convincing argument for truth values of implications with false antecedent is to consider statements with a free variable. “If n is odd, then n^2 is odd”. This is true beyond any questions, right? Now substitute n=2. The statement must remain true for this particular case, because it is true in general. “If n is even, then n*k is even”. True. Now substitute n=3, k=2. Still true.
That’s a nice way to explain it!
However, you can push your intuition the other way as well. Suppose I said ” (n == 0 implies n == 1) OR (n == 1 implies n == 0)”. Since one of the antecedents is clearly false no matter what value we choose for n, the value of that implication must be true, and therefore the value of the entire “or” predicate is always true. But plainly neither of the implications can be correct — n equaling something *never* implies that it equals something else.
I really like that last example because a key feature of implication, as commonly used, is that it doesn’t just say that there exists a combination of variables such that the antecedent is false or the consequent is true, but rather that for ALL combinations of variables such that the antecedent is true, the consequent is also true. One could say that for every value of N, either (!(n==0) || (n==1)) or (!(n==1) || (n==0)) will be true, but that does not mean that either of the statements, individually, is true for every value of n.
By the way, in some languages (e.g. in Kotlin http://kotlinlang.org) it just happens that there is an operator for implication. “x implies y” is (somewhat surprisingly) written as “x <= y". Just because booleans are ordered.
That just shows the ordering is wrong, then. 🙂
There is definitely mathematical precedent from algebra for making false > true: false is a stronger predicate since it implies everything. So if we read “>=” as “is at least as strong as” and we allow it to be written as “=>” then p => q would be a natural way to write implication.
Anyone who really doesn’t want to write your final example can just write an extension method:
public static class ImplicationExtensions
{
public static bool Implies(this bool antecedent, bool consequent)
{
return !antecedent || consequent;
}
}
Then you get to write this:
Debug.Assert(p.Implies(q));
At this point, the case for a built-in operator seems even slimmer.
Not that I particularly like this – the code sounds like it’s doing more than it is. If I write Debug.Assert(a == b) then I can be sure, if the assertion succeeds, that a is == to b. With implication it sort of suggests I’m asserting that p necessarily implies q, but all I’ve really done is verify that the current values of p and q do not contradict the assertion that p implies q. It may still be false in the general case, it’s just that the present values of p and q are not a counterexample.
I’m aware that this is simply how the implication operator is defined; this is an observation on what the code seems to say when you have the text ‘implies’ in there. And I think it arises because the implication operator’s name is unlike other logical operators: implication is named for you what you would know if you had proved that a particular logical statement using that operator is a tautology (e.g., if you had somehow formally proven that the streets are always wet when it is raining); the name overreaches when applied only to two particular operands – this operator really only tells me anything useful when it evaluates to false, and I can draw only a very limited inference if it is true. The others common logical operators are named for what you know after applying the operators to any particular pair of operands. (If, using informal language, I tell you A and B are true, that sounds like a statement about the values of A and B. If I tell you that A implies B, that sounds like I’m asserting a causal relationship – it does not sound like I’m talking just about the particular values A and B have in a specific context. I suspect this is part of the reason people are thrown when they first come across the implication operator.) Unless you’re looking at a logical expression that you have proven to be a tautology (and for typical uses of Debug.Assert you won’t be) then “Implies” is best informally described as “Does not directly contradict the assertion that P implies Q”.
So I actually prefer the !p || q formulation because it seems more obvious that I’m just running some truth values through an operator, and that the conclusions I can draw from successful assertion of implication are limited.
This way q would always be evaluated, right? So maybe let the parameter be
Func consequent
and call it like
Debug.Assert(p.Implies(() => q));
Not a very pretty syntax, though.
Func<bool> consequent?
Everybody understands
if (s == null || s.Length == 0) { … }
I agree with you, I too doubt that something like
if (s != null implies s.Length ==0) { … }
would make the meaning clearer to most readers.
A casual reader might think: well, either s != null implies that s.Length == 0 or not, but why would you have to test for this at runtime? The usage of the word “implies” makes it sound like an absolute truth about all possible values of s, not just about the current value.
Pingback: The Morning Brew - Chris Alcock » The Morning Brew #1964
Suppose you were to add Implies(Func,Func) to Debug. Then, to make usage more concise, allow variables (and possibly expressions) to be implicitly converted to a lambda when their type matches the Func return type. With this, you could at have the following statement:
Debug.Implies(p, q);
Otherwise, as things are now, you could also write “p implies q” as:
p?q:true
This is slightly more verbose than “!p||q”, but I think it’s easier to read and comprehend at a glance.
Hmm… that should have showed as
Implies(Func<bool>,Func<bool>)
It sometime helps to use other words:
P is sufficient for Q, means P implies Q
P is necessary for Q, means Q implies P
Pingback: Material Implication, Logical Implication & Causality | Know Moar!
Wouldn’t the ternary operator form be more readable?
(p ? q : true)
Rain boots explanation for P -> Q was pure genius…went through a lot of articles trying to make peace with P -> Q is True when, P is False, and now it makes sense. Thanks!
I would like to inform about two papers.
The first one is: T. J. Stepien and L. T. Stepien, “Atomic Entailment and Atomic Inconsistency and Classical Entailment”, J. Math. Syst. Sci. 5, No.2, 60-71 (2015); arXiv:1603.06621, where a new solution of the problem of entailment and of the problem of material implication, has been presented – there has been defined atomic entailment, and atomic logic has been formulated.
In the next paper: T. J. Stepien and L. T. Stepien, “The Formalization of The Arithmetic System on The Ground of The Atomic Logic”, J. Math. Syst. Sci. 5, No.9, 364-368 (2015) ; arXiv:1603.09334 ,
it has been showed that Arithmetic System can be based on the atomic logic.
The abstracts of these papers:
T. J. Stepien and L. T. Stepien, The Bulletin of Symbolic Logic 17, No. 2, 317-318 (2011). http://www.math.ucla.edu/~asl/bsl/1702-toc.htm
and
T. J. Stepien and L. T. Stepien, The Bulletin of Symbolic Logic 22 , No. 3, 434 – 435 (2016).
https://doi.org/10.1017/bsl.2016.22 .