Aren't constructive math proofs more "sound"?

Solution 1:

Proof theorists have obtained several "relative consistency" proofs between classical and constructive theories. These show that if certain theories of classical mathematics are inconsistent, then corresponding theories of constructive mathematics are also inconsistent. These relative consistency results are proved constructively. They show that the consistency problem does not simply disappear if we switch to constructive mathematics.

One of the more famous relative consistency techniques uses a "double negation translation". This method assigns each formula $\phi$ of a system a corresponding formula $\phi^N$ (the "translation" of $\phi$). The exact definition of the translation varies from author to author, depending on the system at hand. But the name is somewhat accurate: the definition of $\phi^N$ involves adding additional negation symbols to $\phi$ in the right places.

In 1933, Gödel proved there is a translation $N$ of formulas of Peano arithmetic so that whenever a formula $\phi$ is provable in Peano arithmetic, the corresponding formula $\phi^N$ is provable in the constructive system of Heyting arithmetic. Moreover, if $\phi$ is of the form $A \land \lnot A$ then Gödel's translation assigns it the formula $\phi^N = A^N \land \lnot A^N$, which is still contradictory. This means that if Peano arithmetic is inconsistent, so is its constructive counterpart Heyting arithmetic. Gödel's proof is constructive, like you would hope.

So if we were only worried about consistency, there would be no advantage to working in Heyting arithmetic instead of Peano arithmetic. But people who work in constructive mathematics do not do it only for the sake of consistency. Constructive proofs carry more information than classical proofs, so constructive provability is interesting even to classical mathematicians.

You can read a little more about Gödel's result at this wikipedia article.

Solution 2:

A whole bunch of things in mathematics are inherently nonconstructive. For instance, invariant theory--recall the famous quote by Gordan that Hilbert's mathematics was "theology." (A quote which, I believe, was in jest.) The Hahn-Banach theorem, a fundamental tool in functional analysis (and a great tool for proving all sorts of results, like approximation results--Runge's theorem, the Stone-Weierstrass theorem, and more) relies on the axiom of choice, and is consequently nonconstructive. The fact that any proper ideal in a ring is contained in a maximal ideal is frequently used in algebra, and yet it needs the axiom of choice. The use of ultraproducts in logic (or the construction of hyperreal numbers) is inherently nonconstructive: you can't just exhibit a nonprincipal ultrafilter on the natural numbers.

Basically, a lot of mathematics just doesn't work without Zorn's lemma, and this is equivalent to the axiom of choice.

Solution 3:

"Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists. To prohibit existence statements and the principle of excluded middle is tantamount to relinquishing the science of mathematics altogether."

-David Hilbert

Solution 4:

The distinction between constructive mathematics and traditional mathematics has nothing to do with Russell's Paradox.

Constructive mathematics simply requires working with one less basic postulate that many mathematicians have believed to be sensible and on which some proofs are based, namely the Axiom of Choice