9
$\begingroup$

I was reading an introductory book on logic and it mentioned in passing that the Law of Excluded Middle is somewhat controversial. I looked into this and what I got was the intuistionists did not accept it in contrasts to the formalists. I'm curious but I'm only taking an introductory course in logic though very informally and vaguely I do know the history of mathematics upto Godel's incompleteness and Hilbert's program.

Can anyone tell me what is the nature of the controversy in a way that suits my level of understanding about mathematics? Further, what is an example of constructive mathematics or constructive mathematical proof and why do the intuistionists say that LEM is no good for it(if that's right)? Thanks!

$\endgroup$
  • 2
    $\begingroup$ At its heart, constructivism is about what it means for a mathematical object to exist. A materialist might already object that mathematical objects don't "exist" - they're just thoughts. At a stretch, you might say they exist because you can imagine them, that is, construct them. And now you come along with an object that not only is purely imaginary, but you can't even describe it or construct it in any way. What sort of "existence" is that? If I understand correctly, excluding the LEM makes non-constructive existence proofs impossible. Someone else will have to explain why. $\endgroup$ – Jack M Feb 2 '16 at 21:35
6
$\begingroup$

Basically, the "issue" is, that with LEM you can "decide" things that a machine or (a person) could never decide on their own.

Pick two random reals $a,b$. Then obviously $a<b, a>b$ or $a=b$, right? But if $a=b$, how would you ever know that? You start comparing the digits of $a$ and $b$ and find that they are all the same, but you can never know for sure, because the sequences of digits are infinite. Hence, the program comparing two numbers would never halt, if they are the same.

That is the basic idea of constructive mathematics: If a program can't decide, then it is simply undecidable. And so, it is constructively not a theorem, that for all reals $a,b$ we have $a<b, a>b$ or $a=b$.

Another issue is, that in the same fashion for any property $\phi$, there is an $x$ with $\phi(x)$ or there is no $x$ with $\phi(x)$, according to LEM. But this makes no sense constructively: "there exists" means "I can find one", but for example: Given a continuous function $f : [a,b] \to \mathbb{R}$ with $f(a) < 0$ and $f(b)>0$, you know that, classically, there is an $\xi$ with $f(\xi) = 0$, but you cannot necessarily find that exact $\xi$, you can only approximate it. This is why this theorem fails constructively (but it works if you only claim that a zero can be approximated)

I should mention: the axiom of choice implies the non-constructive existence of various objects, so it should come as no surprise, that it implies LEM in constructive mathematics (Diaconescu's theorem).

$\endgroup$
  • $\begingroup$ Your first example reminds me of a lecture by Gregory Chaitan talking about noncomputable reals(link is here if you're interested: youtube.com/watch?v=2a_h2Jw7g00). But how big of a consequence does this have in higher mathematics either way, if you don't use LEM and do? $\endgroup$ – Red Feb 2 '16 at 21:50
  • $\begingroup$ @Red Category theory, logic, discrete mathematics and a lot of algebra are not much affected. Field theory, for example, is another story: here things "break apart" quite a bit (you get many different notions of "field"). Analysis is, well, considerably different. For example, now there is a difference between Dedekind-reals and Cauchy-reals. Point-set topology does really not work anymore, neither does classical measure theory; here alternatives are needed (in the case of topology for example "locale theory"). But don't take my word for it, I am no expert. $\endgroup$ – Stefan Perko Feb 2 '16 at 21:57
  • $\begingroup$ Your 2nd paragraph got me wondering whether this equality issue still arises if we restrict ourselves to comparing two rational numbers each known to have a finite decimal expansion, and the rational numbers are presented to us in that form. Or even whether this issue arises when comparing two positive integers given in decimal form. Note that no matter how many digits we've checked and found to agree for the two positive integers, we wouldn't know whether the integers are different because we don't know when the digits will end. Maybe not as problematic, but I can still see issues with this. $\endgroup$ – Dave L. Renfro Feb 2 '16 at 22:10
  • $\begingroup$ @DaveL.Renfro The case with the rational numbers in decimal expansion (!) seems to be a problem indeed, but I am really not sure. It is curious, that in general you can always compare two rationals (given as integer fractions). But integers should not be problem: their decimal expansion is finite. $\endgroup$ – Stefan Perko Feb 3 '16 at 8:12
  • 1
    $\begingroup$ To be fair, I should mention that the axiom of choice on its own does not imply nonconstructive principles - for example Martin-Lof type theory and higher-order Heyting Arithmetic both include the axiom of choice, and it is accepted in Bishop's constructive analysis. The combination of the axiom of choice with certain extensionality principles does imply LEM, as Diaconescu's theorem shows. But this could equally well be blamed on extensionality - constructive mathematics is often more attuned to setoids than sets. $\endgroup$ – Carl Mummert Feb 4 '16 at 19:21
3
$\begingroup$

The law of excluded middle (LEM) is the crucial ingredient in any proof by contradiction (as opposed to proof of contrapositive). The objection to LEM is most easily understood in this context.

Some proofs by contradiction establish the existence of this or that mathematical object. Constructively speaking, the problem with a proof by contradiction is that it does not provide any indication of how such a mathematical object is to be found or described specifically.

Briefly put, the constructivist claim is that existence is construction, rather than proof of impossibility of nonexistence.

The constructive mindset leads one quite far afield and leads to startling conclusions, such as the idea that the traditional extreme value theorem could be false constructively.

To understand this concept intuitively, notice that there is no way to find an approximation to such a claimed extremum. This is because the extremum is not a continuous function of the input function, as one easily convinces onself by looking at simple examples of a function with two "humps" of about the same height.

$\endgroup$
  • 4
    $\begingroup$ While I agree with everything you say, I must point out, that proof of contradiction has two meanings and that only one type of proof of contradiction is actually invalid constructively; meaning the other one (called proof of negation by some constructivists) is perfectly fine and necessary. See also my answer here: math.stackexchange.com/a/1259017/166694 $\endgroup$ – Stefan Perko Feb 4 '16 at 18:57
  • $\begingroup$ @StefanPerko, The other type of proof is called proof by contrapositive (not by negation). $\endgroup$ – Mikhail Katz Feb 5 '16 at 8:16
  • 2
    $\begingroup$ That is incorrect. Proof by contrapositive is another rule, which simply does not work constructively. See also this blog post by Andrej Bauer: math.andrej.com/2010/03/29/… $\endgroup$ – Stefan Perko Feb 5 '16 at 8:27
  • $\begingroup$ It does work, but it only proves the contrapositive statement :-) $\endgroup$ – Mikhail Katz Feb 5 '16 at 8:32
  • 1
    $\begingroup$ well yeah. I would call this proof of contrapositive rather than proof by contrapositive. Okay, maybe this is not standard terminology. My point is, that you can "do" less with contrapositives constructively. $\endgroup$ – Stefan Perko Feb 5 '16 at 8:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.