14
$\begingroup$

It is obvious that in constructive mathematics, you cannot use the law of excluded middle. What else would be the reasons for not adopting the constructive stance in mathematics?

  • 16
    Because it requires more work, and mathematicians are by nature lazy?2012-07-22
  • 16
    Because it’s incompatible with much of the mathematics that I like.2012-07-22
  • 0
    @Marc van Leeuwen : Some of us are by nature masochists, and those of us who are actually do constructive mathematics. But there are a few of them, not so many, fair enough... =)2012-07-22
  • 7
    Because proofs by contradiction are always fun!2012-07-22
  • 5
    I tend to believe that things can exist, even if we are unable to describe them explicitly.2012-07-22
  • 4
    I wholeheartedly agree with the commented by Marc and Brian, yet there's one further reason important to me: the excluded middle makes a lot of sense in my mind. For me, it is a completely sound and "logical" assumption and I've no problem at all with it. Just as AC, but even easier to grasp.2012-07-22
  • 2
    Because those truths that we intuit outstrip those that we can prove, and even more so those, truths that we do actually prove.2012-07-22
  • 2
    Because classical logic doesn't lead to falsehoods. (On which even ituitionists would agree, though they may dispute whether all it leads to is truth).2012-07-22
  • 2
    @DonAntonio: I don't understand what you mean - the axiom of choice is obviously true! (On the other hand, the well-ordering principle is obviously false, and I personally don't believe Zorn's Lemma. It is silly.)2012-07-23
  • 1
    Well @user1729, if AC was "obviously true" why then there are *mathematicians* who don't accept it? Perhaps what's "obvious" to you isn't to others...? OTOH, in ZF, the well-ordering principle is equivalent with, oh paradox!, both AC and Zorn's Lemma, so your calling the last one "silly" doesn't make you look specially sharp, does it? Now, if you want to throw away ZF and work under other system go ahead and be anyone's guest.2012-07-23
  • 11
    @DonAntonio: "The Axiom of Choice is clearly true, the well-ordering principle is clearly false, and nobody really knows about Zorn's lemma" is an old math joke.2012-07-23
  • 0
    @MichaelGreinecker, I know that, thanks. Yet user 1729 changed in such a way (in particular the adding "it is silly") that made it look, at least in my eyes, as no particularly "jokely". Anyway I shall have my irony-sarcasm glands checked next week.2012-07-23
  • 1
    @DonAntonio: Deadpan humour is the best kind of humour. I was in a talk last week where Martin Bridson nonchalantly described studying the Nilpotent Genus, I believe it was, of a group as "a disease he caught from Baumslag". Que shock then laughter from us graduate students hiding at the back...2012-07-23
  • 3
    @Brian M. Scott: most constructive logics have the property that the things they prove are a proper subset of the things provable classically. These logics are not in any way incompatible with usual mathematics, they are just weaker.2012-07-23
  • 1
    @BrianM.Scott: I think that holds true for much of what i done under the banner of constructivism, especially the things in the tradition of Bishop. But Brouwers intuitionism was very different.2012-07-23
  • 0
    @Carl: Weak enough to be incompatible with what I want to do. I like non-constructive existence proofs. I insist on the axiom of choice.2012-07-23
  • 1
    @Brian M. Scott: many constructive systems include the axiom of choice, it's a completely separate issue.2012-07-23
  • 0
    @Carl: Not in the sense of *constructive* with which I’m familiar and was using the term. (And I certainly wouldn’t apply the term to anything that permitted the use of AC.)2012-07-23
  • 0
    @Carl, or arguably sometimes stronger since we can interpret classical logic in intuitionistic logic. It is a more expressive language so there are more distinctions and more unprovable equivalences. (I sometimes wonder what would have happened if constructivists used new logical symbols in place of classical ones. :)2012-07-24
  • 4
    I find the wording of the question a little strange. I have no *stance* myself on any of these issues. I request different kinds of proofs of facts depending on what I want. Sometimes I want a constructive procedure, sometimes I don't care. It really depends on the purpose of the proposition as to which type of proof you want or which kind of formalism you want to live in.2012-07-24
  • 0
    what is constructive mathematics?2013-09-14
  • 0
    i think by constructive (and excluded middle) you refer to intuitionism specifically, which accepts excluded middle but not un-critically. For example for very large sets where it is not at all obvious or inferable that this holds..2014-05-27
  • 0
    "Supporting" and "adopting" are not synonyms. It would be helpful if you could reconcile the title of your question with the question. I support constructive mathematics, but I don't adopt constructivism as a dogma.2016-08-01

4 Answers 4

15

This is a philosophical question rather than a mathematical one, although mathematical results can provide significant insight.

On its own, not being able to use excluded middle is not a justification for constructive logic any more than being able to use excluded middle is a justification for classical logic. The justification comes in the benefits that are derived from avoiding excluded middle, or are derived from using it.

Classical logic is the logic of structures - of things that "exist" in some sense, or at least have objective properties independent of whether we can verify those properties. Thus, for example, if I have a function that assigns each real number either "red" or "blue", then either every real number is assigned "red" or some real number is assigned "blue". That latter fact is not "constructively provable" - because constructive mathematics is not about what is true as much as it is about what we can verify (of course, anything we can verify to be true is true). Just because I know that "not every real number is assigned red" does not mean that I actually know a specific real number that is assigned "blue", and thus I have no way to verify that some real number is assigned "blue" even though I know, classically, that there must be one.

Thus, in a sense, classical logic is the logic of truth and constructive logics are logics of verification. By verification I mean more than just "proof"; I mean the sort of thing that is captured in the BHK interpretation. In settings where we are interested in that sort of verification - for example, in computable mathematics - a constructive logic will work well. In settings where we simply want to reason about truth, rather than about concrete verification, classical logic is better. Most mathematicians are interested in reasoning about mathematical objects, and because of this they use classical logic.

  • 1
    your comment above: "because constructive mathematics is not about what is true as much as it is about what we can verify" is equally valid in nonconstructive mathematics. Classical statements also have to be verified; classical theorems are accompanied by proofs which are the verifications of the statements contingent the on assumptions.2012-07-23
  • 1
    My point is that classical logic is designed to reason about truth values of statements (its rules preserve truth) while constructive logics reason about verification (their rules preserve not only truth [usually], but various kinds of concrete verifiability). By "verifiability" I mean more than just provability; the BHK interpretation gives one precise sense of what I mean.2012-07-23
  • 0
    I don't know what BHK is, but there are truth values in Boolean algebras and truth values in Heyting algebras. The former model classical logic, while the latter constructive logic. Both evolve in the same way, but the latter only use Modus Ponens as axiom - that's the only difference. They are both about reasoning about truth values.2012-07-23
  • 3
    As far as I’m concerned, being able to use excluded middle **is** a justification for classical logic.2012-07-23
  • 3
    @Brian M. Scott: that's like saying a fork is better than a spoon because a fork has tines. It's not a justification, it's just a description.2012-07-23
  • 0
    Obviously I don’t see it that way.2012-07-23
  • 0
    I'm no expert in the field, but the whole intuitionist program seems to me to be a gross over-reaction to contradictions of naive set theory -- throwing the baby (LEM) out with the bathwater.2012-07-29
  • 0
    @Dan Christensen: I think the end of Kaveh's answer is relevant to that.2012-07-29
  • 0
    You do not mention that exactly this classical logic in mathematics results in many paradoxes which are not present in constructive mathematics in general (and this to a large extend) beats the purpose of classical maths.2014-05-27
6

Historically the main reason that Hilbert and others have rejected constructive mathematics was because it mean that they have to use more restricted ways of reasoning and some felt that forbidding PEM in mathematics is to tie the hands of mathematician. Or in another colorful language due to Hilbert, it felt as being expelled from "Cantorian Paradise" of set theory (Mathematicians are very conservative people regarding mathematics).

It also seemed that by accepting constructivism one needs to throwing away a considerable amount of mathematics developed by that time. Even more troubling for them was the fact that some classical results become not just unprovable but false in their literal constructive reading! (Not very surprising after all, you can't expect much if you try to read an English sentence as if it is written in French.)

For that matter, the rejection was not as philosophical as it might seem. Hilbert himself was a finitist. He saw ideal objects as means that help one prove results, but he thought that they are not really needed. One of the goals of his proof theory program was to make sure that using "ideal" objects like abstract sets and real numbers does not lead to incorrect results about "real" objects like natural numbers.

In addition, stating or proving results in a constructive way is often not straight forward. The constructive language takes into account information when we talk about mathematical objects. How an object is represented and given becomes important. Classically equivalent concepts (e.g. $\lnot (\lnot p \land \lnot q)$ vs. $p \lor q$, Dedekind real numbers vs. Cauchy real numbers, etc.) become distinct.

I would suggest having a look at Bishop style constructive mathematics. Bishop tried to address these issues and obtain a constructive mathematics which is compatible with classical mathematics and would be more acceptable for classically minded mathematicians.

Another issue, as mentioned in the comments, was that at some point Godel proved that from the perspective of security of mathematical foundations, there is not much difference between classical and constructive. Simplified, this means that proving a result classically is the same as proving the Godel translation of the result constructively. So the main original supportive argument for constructive mathematics (i.e. it is more secure) became useless.

Constructive mathematics suffered a continuous decline among mathematicians until its relevance to computers become clear. It seems to me that eventually the relation with computational mathematics (e.g. Martin-Löf style type-theory) was a more important factor in revival of constructive mathematics that philosophical issues. (Bishop style constructivism also had a considerable effect).

  • 1
    unf. cannot link, copy-pasting. *You do not mention that exactly this classical logic in mathematics results in many paradoxes which are not present in constructive mathematics in general (and this to a large extend) beats the purpose of classical maths*2014-05-27
  • 1
    Goedel provided a translation ("Dialectica Interpretation") of classical logic *inside* intuitionistic logic. Importantly the negative translation is **not** applicable in all cases. In fact the answer seems to forget that some classical results are false in intuitionism.2014-05-27
  • 0
    FYI, there are no known paradoxes in classical logic, you are confusing naïve set theory with classical logic.2014-05-27
  • 0
    How about the [Banach–Tarski paradox](http://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox), and other related to (classical concepts of) infinity2014-05-27
  • 0
    Since you mention classical logic, how about [Russell's paradox](http://en.wikipedia.org/wiki/Russell%27s_paradox)? A classical non-constructive paradox2014-05-27
  • 0
    But you have a point, if classical logic is taken out of context, by itself has no paradoxes. But in classical mathematics there are many non-constructive paradoxes, and this was my initlal point. Setting the record straight.2014-05-27
  • 0
    Quoting your answer "*It also seemed that by accepting constructivism one needs to throwing away a considerable amount of mathematics developed by that time*". This was what my comment was about. Lets not leave traces of misunderstanding, based on shades of meaning.2014-05-27
  • 1
    I am satisfied with my answer as it is. I don't have time to reply of your misunderstandings or get into a debate with you right now, sorry. (Please feel free to "do science" wherever you please.)2014-05-27
  • 0
    Thank you. Yet, still bypassing Kaveh. Anyway i dont want to get personal, have a nice time.2014-05-27
  • 0
    PS. in a strictly friendly way, whenever you want and have time we can always have a chat about maths (and whatelse). No hard feelings2014-05-27
  • 0
    @Nikos M.: the Russell paradox applies equally well to constructive systems; cf. http://publish.uwo.ca/~jbell/russ.pdf2017-11-20
2

One justification I've heard goes something like this: one of the purposes of constructive mathematics is that it is closer to being applicable in the real world. But non-constructive methods are useful for getting to results more expediently. Once a result is proven non-constructively, its constructive content (and hence is real-world applicability) can be investigated.

  • 3
    This is indeed a justification that some give, but it relies on a very reductive meaning of "real world" that would not be shared by e.g. mathematical realists.2012-07-23
  • 0
    This is exaclty opposite to Archimedes' method of finding a mathematical proof (*On the mechanical theorems*). Archimedes used to construct a physical/mechanical model which "proved" by its construction and operation the needed principle and then used as guide to formalize it to mathematical symbolism.2014-05-27
1

Since:

  1. classical mathematics seems to work, and
  2. its a lot simpler than constructive mathematics, and
  3. its still not clear to me how and in what sense my mathematics would be better if it were constructive,

for these reasons I'm sticking with classical mathematics for the moment.

On the other hand, I support constructive mathematics, in the sense that I think its great that people are working these things out.

  • 1
    classical maths = lots of paradoxes, here is one reason for you :)2014-05-27
  • 0
    @Nikos M.: there are no paradoxes in classical mathematics, as it's usually practiced, that aren't also present in constructive mathematics (e.g. Curry's paradox).2017-11-20