5 ms·

Ok I think what happens here is that we assume for the real numbers an increasing sequence which is bounded converges. I think that a number system with this pr

Ok I think what happens here is that we assume for the real numbers an increasing sequence which is bounded converges. I think that a number system with this property is probably already hard to construct in constructive math.

Davidzheng 6y ago
So the problem that constructive math has for real numbers is that it's hard to show real numbers exist at all, not that it's uncountable if you have its properties. Also the deeper point is that you have all the properties of the real numbers you can actually derive the law of excluded middle. (Coming from the supremum axiom)
- adamnemecek 6y ago
  This is really interesting. I'm not surprised by axiom of choice being based on real numbers. I've been thinking about that lately but I don't have a good intuition why. Do you have a link?
  - Smaug123 6y ago
    I'd be very surprised if it were true in general. But there certainly has to be some non-computational component to the reals being a complete totally ordered Archimedean field, because the question of deciding the equality of two reals is uncomputable, so there is no procedure to decide the total order.
- ogogmad 6y ago
  > So the problem that constructive math has for real numbers is that it's hard to show real numbers exist at all No. They exist in any topos with a Natural Number Object. In other words, they exist in all varieties of constructive mathematics that admit a set of natural numbers.
  - chongli 6y ago
    Brouwer (father of intuitionism) rejected actual infinity. He would not admit the axiom of infinity and therefore reject the set of all natural numbers. Tough to do things that way though.
    - mike00632 6y ago
      If there isn't an actual infinity of Natural numbers, which is the largest?
      - chongli 6y ago
        Brouwer distinguished between actual infinity and potential infinity, with the former inadmissible in intuitionism. He would say “the largest natural number” is a meaningless statement. You could only have the “largest so far”. Intuitionism invites you to construct as large of a natural number as you want. It simply does not admit “the complete set of all natural numbers”. The point of intuitionism is the idea that all mathematics is constructed by human creativity and logic. Brouwer rejected the idea that mathematics was “already out there, waiting to be discovered”. This is a subtle point. It says that mathematical objects do not exist in some mind-independent realm of truth. It has the nice property of avoiding some of the problems of classical mathematics that Hilbert got caught up in.
        mike00632 6y ago
        Ok, so what is the largest Natural number so far?
        chongli 6y ago
        “So far” with respect to some particular problem you’re solving or process you’re following. If you’re talking about all problems, you’d have to do some research. Perhaps OEIS [1] could help you. Or you could interview some number theorists to find out who is working in large numbers and ask them. Asking the question in general, though, is equivalent to asking “what is the largest number anyone has thought of?” I would have to interrogate your motives to know why you would want to ask such a question. Intuitionists would scoff at the idea of a “number larger than anyone could describe.” That’s heading into the territory of the interesting number paradox [2]. Intuitionism avoids this paradox by stating that numbers (and sets of numbers) have no existence independent of their construction. [1] https://oeis.org/ https://oeis.org/ [2] https://en.wikipedia.org/wiki/Interesting_number_paradox https://en.wikipedia.org/wiki/Interesting_number_paradox
- Smaug123 6y ago
  Certainly in Agda I've personally proved that the "Cauchy sequences of rationals" formulation is a partially ordered ring. However, I believe (but have not tried it and have not proved) that if you stick with Agda's incredibly strict and purely computational logic, the proof does indeed fall over. The problem is that Bob can't identify in general whether one real is less than another (indeed, this would imply solving the halting problem), so he can't know whether he's allowed to pick s_n at time n or not: he can't know whether s_n is less than his current number and hence a valid choice.
ogogmad 6y ago
No. The real numbers are constructed as located Dedekind cuts, or modulated Cauchy sequences. There are no issues with this construction in constructive mathematics. You are indeed right that you can't show that an increasing and bounded sequence of real numbers has a limit. But you can prove constructively that if a sequence of real numbers is Cauchy then it has a limit. And it is that last property which is the defining property of the real numbers (Cauchy completeness).

Davidzheng 6y ago

So the problem that constructive math has for real numbers is that it's hard to show real numbers exist at all, not that it's uncountable if you have its properties. Also the deeper point is that you have all the properties of the real numbers you can actually derive the law of excluded middle. (Coming from the supremum axiom)

adamnemecek 6y ago
This is really interesting. I'm not surprised by axiom of choice being based on real numbers. I've been thinking about that lately but I don't have a good intuition why. Do you have a link?
- Smaug123 6y ago
  I'd be very surprised if it were true in general. But there certainly has to be some non-computational component to the reals being a complete totally ordered Archimedean field, because the question of deciding the equality of two reals is uncomputable, so there is no procedure to decide the total order.
ogogmad 6y ago
> So the problem that constructive math has for real numbers is that it's hard to show real numbers exist at all No. They exist in any topos with a Natural Number Object. In other words, they exist in all varieties of constructive mathematics that admit a set of natural numbers.
- chongli 6y ago
  Brouwer (father of intuitionism) rejected actual infinity. He would not admit the axiom of infinity and therefore reject the set of all natural numbers. Tough to do things that way though.
  - mike00632 6y ago
    If there isn't an actual infinity of Natural numbers, which is the largest?
    - chongli 6y ago
      Brouwer distinguished between actual infinity and potential infinity, with the former inadmissible in intuitionism. He would say “the largest natural number” is a meaningless statement. You could only have the “largest so far”. Intuitionism invites you to construct as large of a natural number as you want. It simply does not admit “the complete set of all natural numbers”. The point of intuitionism is the idea that all mathematics is constructed by human creativity and logic. Brouwer rejected the idea that mathematics was “already out there, waiting to be discovered”. This is a subtle point. It says that mathematical objects do not exist in some mind-independent realm of truth. It has the nice property of avoiding some of the problems of classical mathematics that Hilbert got caught up in.
      - mike00632 6y ago
        Ok, so what is the largest Natural number so far?
        chongli 6y ago
        “So far” with respect to some particular problem you’re solving or process you’re following. If you’re talking about all problems, you’d have to do some research. Perhaps OEIS [1] could help you. Or you could interview some number theorists to find out who is working in large numbers and ask them. Asking the question in general, though, is equivalent to asking “what is the largest number anyone has thought of?” I would have to interrogate your motives to know why you would want to ask such a question. Intuitionists would scoff at the idea of a “number larger than anyone could describe.” That’s heading into the territory of the interesting number paradox [2]. Intuitionism avoids this paradox by stating that numbers (and sets of numbers) have no existence independent of their construction. [1] https://oeis.org/ https://oeis.org/ [2] https://en.wikipedia.org/wiki/Interesting_number_paradox https://en.wikipedia.org/wiki/Interesting_number_paradox
Smaug123 6y ago
Certainly in Agda I've personally proved that the "Cauchy sequences of rationals" formulation is a partially ordered ring. However, I believe (but have not tried it and have not proved) that if you stick with Agda's incredibly strict and purely computational logic, the proof does indeed fall over. The problem is that Bob can't identify in general whether one real is less than another (indeed, this would imply solving the halting problem), so he can't know whether he's allowed to pick s_n at time n or not: he can't know whether s_n is less than his current number and hence a valid choice.

ogogmad 6y ago

No. The real numbers are constructed as located Dedekind cuts, or modulated Cauchy sequences. There are no issues with this construction in constructive mathematics. You are indeed right that you can't show that an increasing and bounded sequence of real numbers has a limit. But you can prove constructively that if a sequence of real numbers is Cauchy then it has a limit. And it is that last property which is the defining property of the real numbers (Cauchy completeness).