# What are the reasons for not supporting constructive mathematics

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

-
Because it requires more work, and mathematicians are by nature lazy? – Marc van Leeuwen Jul 22 '12 at 8:04
Because it’s incompatible with much of the mathematics that I like. – Brian M. Scott Jul 22 '12 at 8:08
Because proofs by contradiction are always fun! – Asaf Karagila Jul 22 '12 at 8:36
I tend to believe that things can exist, even if we are unable to describe them explicitly. – mrf Jul 22 '12 at 9:38
@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. – Michael Greinecker Jul 23 '12 at 13:08

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.

-
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. – alancalvitti Jul 23 '12 at 15:00
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. – Carl Mummert Jul 23 '12 at 15:03
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. – alancalvitti Jul 23 '12 at 17:18
As far as I’m concerned, being able to use excluded middle is a justification for classical logic. – Brian M. Scott Jul 23 '12 at 19:16
@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. – Carl Mummert Jul 23 '12 at 19:30

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).

-
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 – Nikos M. May 27 '14 at 20:35
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. – Nikos M. May 27 '14 at 20:44
FYI, there are no known paradoxes in classical logic, you are confusing naïve set theory with classical logic. – Kaveh May 27 '14 at 21:52
How about the Banach–Tarski paradox, and other related to (classical concepts of) infinity – Nikos M. May 27 '14 at 21:54
Since you mention classical logic, how about Russell's paradox? A classical non-constructive paradox – Nikos M. May 27 '14 at 21:56

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.

-
classical maths = lots of paradoxes, here is one reason for you :) – Nikos M. May 27 '14 at 20:40

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.

-
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. – Carl Mummert Jul 23 '12 at 14:59
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. – Nikos M. May 27 '14 at 20:37