The Law of Excluded Middle
- 13 May 2005
- Constructive math, Tutorial
Ordinary mathematicians usually posses a small amount of knowledge about logic. They know their logic is classical because they believe in the Law of Excluded Middle (LEM):
For every proposition `p`, either `p` or `not p` holds.
To many this is a self-evident truth. Therefore they cannot understand why someone would reject such a law, and a useful one at that, since many neat proofs depend on it. An equivalent law of logic is reductio ad absurdum or proof by contradiction:
For every proposition `p`, if `not p` does not hold, then `p` holds.
Constructive mathematicians do indeed reject LEM. But this does not mean they accept its negation! Unfortunately, many ordinary mathematicians seem to think precisely that, and so naturally they conclude that constructive mathematics is garbage. In fact, both classical and constructive mathematics prove quite easily that the negation of LEM is false. So what do constructive mathematicians believe?
To explain this a little better, let me phrase LEM in a form that is suitable for this discussion. Suppose we have a set `D` and a property `P(x)` which is defined for elements `x in D`. Then LEM says that, no matter which `D` and `P` we consider,
`forall x in D . P(x) or not P(x)`.
Constructive mathematician says that validity of this statement depends on what `P` is. It is fairly difficult to explain to a classical mathematician the reasons for rejecting LEM, because constructive and classical mathematicians use the same words to mean different things. The result is that
to classical mathematicians the constructive ones are like ascetic monks who took some LSD, while to constructive mathematicians the classical ones are like beings from a two-dimensional world who cannot grasp a third dimension. So take some LSD and imagine yourself sitting inside a sheet of paper.
Imagine that the set `D` in the above formulation of LEM is not just an ordinary set but a metric space, or more generally a topological space. Imagine furthermore that the property `P` is restricted to be an open subset of `D`, that `not P` means the topological exterior of `P`, and that `or` is union (which it is, actually). So now, is it necesssarily the case that `P or not P` covers all of `D`? It depends on `P`, does it not? For example, if we take `D = RR`, the real numbers with the usual metric, and `P = {x in RR ; x > 0}` then `not P = {x in RR ; x < 0}` so `P or not P = RR - {0} != RR`! But if we take `D = NN`, the natural numbers with discrete topology, then no matter what `P` we choose `P` and its exterior cover `NN`.
What constructive mathematicians know is that there are mathematical universes in which sets are like topological spaces and properties are like open sets. In fact, these universes are well-known to classical mathematicans (they are called toposes), but they look at them from “the outside”. When we consider what mathematicians who live in such a universe see, we discover many fascinating kinds of mathematics, which tend to be constructive. The universe of classical mathematics is special because in it all sets are like discrete topological spaces. In fact, one way of understanding LEM is “all spaces/sets are discrete”. Is this really such a smart thing to assume? If for no other reason, LEM should be abandonded because it is quite customary to consider “continuous” and “discrete” domains in applications in computer science and physics. So what gives mathematicians the idea that all domains are discrete?
Of course, classical mathematicians will easily produce counter-arguments to my explanation of LEM. They will say that sets are not topological spaces, and that those who want to consider discrete and continuous domains are welcome to use topology. But this advice is like telling
a cur buyer that he cannot buy the Porche, which is ok because a Yugo with a turbo-thrusther attached to it will get him wherever he wants to go just as fast. Why not let computer scientists use the cool sets of constructive mathematics which already behave like the domains they meet in practice? Why force them to use classical sets which then they have to equip with topologies and metrics to get where they want to be?
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.
Comments
New Logic(ish) Blog
Andrej Bauer of Carnegie Mellon has started a new blog called mathematics and computation. So far he has interesting posts about typesetting math on the web and the law of the excluded middle. Looks like there's a lot of blogs...
Here's a good, practical justification for adopting a constructive approach:
Suppose you've built an online marketplace, and you invite me to join it. In response, I ask you if the market mechanism (eg, an auction or negotiation mechanism) you are using is guaranteed to reach an equilibrium state, a situation where demand and supply are equal. You respond with a statement that you have proved that an equilibrium is always achieved. When I ask you for your proof, you present me with a non-constructive proof (eg, a proof using a fixed point theorem which itself relies on reductio ad absurdem). Why should I accept this proof? Well, IMO, I should not accept it. Unless you can construct the (path which leads to the) equilibrium state, then IMO, you haven't demonstrated adequately that your system can reach it.
The same is true of any other relevant properties of the system, eg, that the mechanism is fair to all participants.
That is a good example. I would just like to point out that it is logically equivalent (on the face of it) to a simpler and well-known example in programming. Since being in equilibrium is expressed as an equation, proving that a system is in equilibrium is like proving that a certain number is zero. Now a proof by contradiction will show that it is impossible for the number to be different from zero. Can we conclude from that that the number is zero? Is it constructively the case, for
x in RR, thatnot not (x = 0) => x = 0? (If it is impossible for a system not to be in equilibrium, must it be in equilibrium?)This is a well-known question. It is usually expressed in the following form: if a sequence
a_nof 0's and 1's is not always 0, does it contain a 1?The affirmative answer to this question is known as Markov principle. PeterMcB is telling us he does not believe in it. But it is very hard not to believe in it, in my opinion, when you ask it in the following form: if a program does not run forever, does it terminate? PeterMcB says "not necessarily".
Thanks, Andrej.
Call your final question Q1:
Q1: "If a program does not run forever, does it terminate?"
Certainly, if I potentially had money at stake in some online marketplace, I would want an affirmative answer to a second question:
Q2(X): "If a program does not run forever, does it terminate within time X?" (eg, X = my expected lifetime).
If all you can tell me is that the answer to question Q1 is YES, but you cannot give me an answer to Q2(X), then I would not participate in your marketplace. An answer of YES to Q1 is not necessarily an answer of YES to Q2(X). And, for any given X, a non-constructive proof-by-contradiction of Q1=YES will provide no information on the answer of Q(X). (I believe this; it should be possible to prove it, I imagine.)
A constructive proof of Q1=YES, on the other hand, may well provide information on the answer to Q2(X), at least for some values of X.
From this I conclude that all venture capitalists should be constructivists. :-)
It appears that mathematicians as well as philosophers are perpetually tip-toeing around the excluded middle, trying to weaken it without rejecting it entirely. Perhaps a logic that can deal directly and consistently with equivocation would clarify matters.
In response to Thad, a great deal of attention in AI over the last 30 years has been on logics for defeasible reasoning -- ie, logics in which one can reach conclusions which can be subsequently defeated in the light of new information, or on the basis of further reasoning, or due to some change in the environment. This work has led AI researchers to look at argumentation, the theories of argument and debate first developed in philosophy. In this area, a key figure has been Aristotle, so it is nice to see his ideas finally being applied in contemporary AI.
Nice explaination.
When I explain my construtivism I say that I study what is provable, while classical mathematicians study what is true. Thus P ∨ ¬P states that either P is provable or ¬P is provable, and every knows that isn’t provable (it isn’t even true).
My explaination is not incompatable with yours.
Hi Andrej.
I once told you that my brain can handle only classical logic (to which you of course disagreed). But now I have come across a real-life phenomenon that I simply cannot grasp; so maybe you can make non-classical sense of it.
In the old days I often used to go cycling but now, with family and kids, find it difficult to get around to it. Specificially each time I want to go, my wife says: you can cycle whenever you like, just not now.
I tried to formalize this as the statement forall t: forall s: ( st P(s) ) on the predicate P(t) := "I can go cycling at instant t" and found it (at least classically) paradoxical.
So can NON-classical logic help understanding women ? (Notice that, if so, this would make an ultimate selling point!)