0

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.

ternary
  • 371
  • 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 Jan 23 '19 at 10:32
  • 1
    @lhf: It's not a surprise indeed. But I'm wondering if there are particular cases where this fact has most impact. – ternary Jan 23 '19 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. – Carl Mummert May 02 '19 at 22:31

1 Answers1

1

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}$.

William Bell
  • 447
  • 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. – ternary May 06 '19 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. – William Bell May 07 '19 at 19:17
  • More generally, look in a textbook of Constructive Analysis and I'm sure you can find some. – William Bell May 07 '19 at 19:17
  • The problem is that constructive math textbooks don't list the classical proofs. So I was wondering whether someone who did a lot of comparative work between both would know a good example. – ternary May 11 '19 at 08:28
  • 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. – ternary May 11 '19 at 08:32
  • You're being a little pedantic, I gave you an example where the same proof was made much longer by requiring it to be constructive, even if there is another proof (which took much longer to find), which proves the same proposition without the extra trouble. – William Bell May 12 '19 at 17:12
  • My apologies for expecting an actual example. If I should consider the example with $a=\sqrt{2}^{\sqrt{2}}$ and $b=\sqrt{2}$, why not provide a pointer to the constructive proof. I must say I'm not yet convinced that it can actually be proven constructively. – ternary May 13 '19 at 21:08
  • To be honest, algebra is not my area of expertise, but what I am seeing suggests it can be proved using the proof method for the Gelfond-Schneider Theorem that $\sqrt{2}^\sqrt{2}$.

    I'm reading Bishop and Bridges' Constructive Analysis, if I spot an arduous proof that otherwise wouldn't be, I will let you know.

     – William Bell May 14 '19 at 14:31
  • Recall that transcendental just means not algebraic, so when researching it, remember that is actually a fact that can be proved by contradiction even on a constructive account. – William Bell May 14 '19 at 14:32