# The price of constructivity

It is said that proofs in constructive math, if possible at all, tend to be more verbose than in classical math. I'm trying to get an intuition for this, so:

Are there any good example of theorems mathematicians use, for which the proof in constructive math is considerably larger that the proof in classical math?

I'm not looking for artificial examples like in this question (https://mathoverflow.net/questions/294092/g%c3%b6dels-speed-up-from-constructive-to-classical-logic), but rather for meaningful theorems.

• It's not a surprise constructive proofs are longer than classical proofs: every constructive proof is a classical proof and it usually proves more.
– lhf
Commented Jan 23, 2019 at 10:32
• @lhf: It's not a surprise indeed. But I'm wondering if there are particular cases where this fact has most impact. Commented Jan 23, 2019 at 10:34
• Most proofs in constructive math look just like proofs in classical math. That's not the same question as whether there are particular theorems that have longer constructive proofs than their classical proofs. Commented May 2, 2019 at 22:31

The proof that there are irrational numbers $$a$$, and $$b$$ such that $$a^b$$ is rational using $$a = \sqrt{2}^\sqrt{2}$$ and $$b = \sqrt{2}$$ is a good example. I believe it has a constructive proof that that is fairly long but the classical proof is short. However that's also a good case for showing that it need not always be that way, since there's a constructive proof that is almost as short as the non-constructive proof using $$a = \sqrt{2}$$ and $$b = \log_2{9}$$.
• My apologies if I made the question too unclear, but if the theorem to be proven is the "there are irrational numbers $a$ and $b$ so that...", then the constructive proof is, as you say, not necessarily longer, and therefore would not be an example of what I'm looking for. If, on the other hand, it is to be proven either that $\sqrt{2}^{\sqrt{2}}$ is rational, or that it is irrational, then I don't see yet how the constructive proof would be longer than a classical one. Commented May 6, 2019 at 17:24
• Well if you look for ages you can always shorten a proof, but the difficulty expanding the proof of "there are irrational numbers $a$ and $b$ so that..." using $\sqrt{2}^\sqrt{2}$ illustrates the point I think. Commented May 7, 2019 at 19:17
• Well, I think both the proof using $a=\sqrt{2}^{\sqrt{2}}$ and $b=\sqrt{2}$ and the one using $a=\sqrt{2}$ and $b=log_2 9$ are pretty much short beyond any shortening. And I would regard them as having a rather similar size (although proof size could be formalized for a less vague comparison). So you probably see that your answer, while being insightful, is not really an answer for the question about a significantly larger constructive proof for some theorem. Commented May 11, 2019 at 8:32