# Aren't constructive math proofs more “sound”?

Since constructive mathematics allows us to avoid things like Russell's Paradox, then why don't they replace traditional proofs? How do we know the "regular" kind of mathematics are free of paradox without a proof construction?

-
I'm voting down as I don't think this question makes sense. As far as I know there's no relationship between Russell's paradox and constructive mathematics, so I don't understand what the question is asking. – Noah Snyder Jul 21 '10 at 5:21
@Noah: There is, at least historically - Weyl (1921) "On the New foundational Crisis of Mathematics" talks of paradoxes threateneing the chorence of mathematics as an enterprise, and recommending intuitionistic or predicative mathematics as the solution. – Charles Stewart Jul 21 '10 at 8:25
@Noah, they are related in a strong sense. I suggest you read about the history of constructivism. Intuitionists were trying to find a safer foundations that would avoid paradoxes arising in classical mathematics and set theory like Russell's paradox. – Kaveh Nov 12 '11 at 17:53
In fact the Russell paradox is perfectly constructive. It shows that naïve set theory is inconsistent, and does so in an entirely constructive way. No excluded middle is used, because even intuitionistically an equivalence $P\iff\lnot P$ is a contradiction (where $P$ is $R\in R$ for the set $R=\{x\mid x\notin x\}$): one has $(P\to\lnot P)\implies\lnot P$ and $(\lnot P\to P)\implies\lnot\lnot P$, and of course $\lnot P\land\lnot\lnot P\implies\bot$). The problem is with the axioms of naïve set theory, not with the logic used. – Marc van Leeuwen Mar 4 '13 at 12:53

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.

-

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.

-
While Hilbert's arguments regarding invariant theory were non-constructive, there are nowadays constructive proofs, I think. – Mariano Suárez-Alvarez Aug 4 '10 at 2:08
Any proper ideal is contained in a maximal ideal... – KCd Aug 17 '10 at 2:21
Fixed, thanks . – Akhil Mathew Aug 17 '10 at 6:34
Another perhaps less famous equivalence of AC is Tychonoff's_theorem (see en.wikipedia.org/wiki/Tychonoff's_theorem - also I recommend Kelly's paper to any interested student reading topology). – AD. Oct 28 '10 at 20:49

"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

-

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

-
Although you're right that constructive mathematics has nothing to do with Russell's paradox, my understanding is that the key point that constructivists deny is the law of the excluded middle (not the Axiom of Choice, though most constructivists don't use that either). – Noah Snyder Jul 21 '10 at 0:19
@Noah: I've browsed the ultimate authority on everything (wikipedia) and it seems you're right on this. Grad school was a long time ago! I just remember one faculty member walking out on my thesis defense when I admitted to using the axiom of choice. – donroby Jul 21 '10 at 2:48
@Noah: There isn't really such a thing as "the" axiom of choice constructively. Higher-order intuitionistic logic has the existence of Skolem functions for all Pi-0-2 sentences, which over ZF is equivalent to the axiom of choice, and this choice principle is generally known as the axiom of choice in intuitionistic type theory, and is much used. – Charles Stewart Jul 21 '10 at 8:42
if we deal only with finite sets, there is no real difference between constructive and non-constructive proofs. – mau Jul 21 '10 at 8:49

when dealing with infinite sets, many propositions cannot be proved mithout using non-constructive proofs. Axiom of Choice (AC, in brief) or an equivalent proposition is required. Russell's paradox is not a problem per se, you just rule out certain collections of things as sets; Banach-Tarski paradox (you may take a ball, "divide" it in a finite number of parts, translate and rotate them and obtain two balls equal to the first) may be worse indeed. But few mathematicians would prefer not to do a lot of maths because AC is not allowed!

-

Here is one elementary result you can't prove without the Axiom of Choice (that I used to think was not part of constructive mathematics): let $\left\{X_i\right\}_{i\in I}$ be an arbitrary family of non-empty sets. Then its product $\prod_{i\in I} X_i$ is a non-empty set.

Everybody knows how to prove that for a family of two sets. If two sets $X$ and $Y$ are non-empty, then their cartesian product $X \times Y$ is non-empty too: since $X$ is non-empty, you can choose one element from it: $x \in X$. For the same reason, you can choose also one $y \in Y$. So you have an element $(x,y) \in X\times Y$ and therefore it is non-empty. Right?

For a finite family of non-empty sets $X_1, \dots , X_n$ this procedure still works: you choose one element in each set starting from the first: $x_1 \in X_1$. And then keep on doing the same for the rest: choose $x_2$ in the second set $X_2$, $x_3$ in the third one $X_3$,... And so on, till you reach $x_n \in X_n$. You have thus produced an element of the cartesian product: $(x_1, \dots , x_n) \in X_1 \times \dots \times X_n$.

Even if you had an infinite countable family of non-empty sets $X_1, X_2, \dots , X_n, \dots$, you could produce an element of their product $\prod_{n=1}^{\infty} X_n$ this way: choose successively elements $x_1 \in X_1$, $x_2 \in X_2$,..., $x_n \in X_n$... And you would obtain your element $(x_n)$ of your infinite cartesian product. Hence $\prod_{n=1}^{\infty} X_n$ is non-empty too if all the $X_n$, $n=1, 2, \dots$ are non-empty.

Now, try to do the same with an arbitrary family of sets $X_i$, with the indexes $i$ belonging to an arbitrary indexing set $I$. That is, set $I$ can be infinite and not countable. This kind of cartesian products do exist in "nature". For instance: $I$ could be the set of real numbers $\mathbb{R}$. Take $X_i = \mathbb{R}$ for all $i \in \mathbb{R}$ too. This cartesian product $\prod_{i\in \mathbb{R}} X_i = \mathbb{R}^\mathbb{R}$ is the same as the set of all (not necessarily continuous) functions from $\mathbb{R}$ to $\mathbb{R}$.

Of course, you can prove that $\mathbb{R}^\mathbb{R}$ is non-empty by showing an element of it (for instance, $f(x) = x$ for all $x\in \mathbb{R}$), but how can you prove, in general, that the product of an arbitrary family of non-empty sets $\prod_{i\in I}X_i$ is non-empty too?

If you try to imitate what you have just done in the finite or countable cases, you'll find asking yourself: where do I start? Which is the first $\ i \in I$? Assuming there is a first $i$, which is the next one?

The answer is that, for an infinite, non-countable, set of indexes $I$ there is in general no such a thing as a first index $i$, nor a next one. So you can't use the previous algorithm in order to produce an element of the product $\prod_{i\in I} X_i$...

Except you have something that allows you to choose, one particular element of each set $x_i \in X_i$ -no matter how, even with no precise constructive algorithm as in the finite or countable cases.

If you were able to do that for no matter which set of indexes $I$, then you would have your element $(x_i)_{i\in I}$ and you would have proved that, if every $X_i \neq \emptyset$, so is their cartesian product $\prod_{i\in I} X_i$.

What do allow you for an infinite, non-countable, set of indexes $I$ to choose those $x_i \in X_i$ for every $i\in I$? Well, this is exactly what the Axiom of Choice says.

-
People often say that the axiom of choice is "nonconstructive", but many systems of constructive math include the axiom of choice. One example is Martin-Lof type theory, which has very strong intuitionist bona fides. Errett Bishop famously wrote that the axiom of choice "is unique in its ability to trouble the conscience of the classical mathematician, but in fact it is not a real source of nonconstructivity in classical mathematics. A choice function exists in constructive mathematics, because a choice is implied by the very meaning of existence." The classical "or" is much more problematic. – Carl Mummert Aug 4 '10 at 19:42
@Carl. Ok. I've changed the first sentence. – a.r. Aug 5 '10 at 11:25
A very interesting and detailed exposition for how a "constructive" proof seems to require AOC. But surely you don't need AOC simply to prove that an uncountable product of nonempty sets is non-empty. Once you prove it for finite or countably infinite products, an injective mapping of any of those into the uncountable product should suffice, no? – DavidW Aug 5 '10 at 19:59
@DavidW: Thanks. As for your question: I'm afraid not. Think about the case of the product of two sets X x Y. There is no map X ---> X x Y. For products you only have maps in the opposite direction X x Y ---> X. In fact, if you look at the proof of an arbitrary product being non-empty it is just the Axiom of Choice. I mean: the fact that an arbitrary product is non-empty, if all its components are non-empty, is equivalent to the Axiom of Choice since elements of the product are, by definition, choice functions! :-) – a.r. Aug 6 '10 at 1:06
@DavidW: Partial correction to my previous statement. When I said "there is no map X ---> X x Y", I actually meant "no canonical map". Of course there are plenty of them: choose one element of Y, y_0, and you have one: x \mapsto (x, y_0). But focus on what I needed to do: I had to choose an element of Y ! In the uncontable case you would need to do this... an infinite (uncontable) number of times. So you are using what? :-) – a.r. Aug 6 '10 at 1:12