Hacker News Reader

Comment by User23 | Hacker News Reader

Well I guess nearly all of the reals must not exist since we can't construct them.

You sound to me like you think you're sarcastically saying something that's just so obviously false that it constitutes a devastating argument against the entire idea of constructive mathematics, but whether the reals "exist" depends a lot on your definition of "exist" and is still an ongoing debate for some definitions of "exist" that are relevant, even without bring constructive mathematics into it. And it's not that hard to draw a perfectly conventional mathematician into an interesting discussion about whether the real numbers deserve to be as fundamental as they are when we can't point to any of them. That is, it isn't just that we can't "construct" them for some definition of construct, but we can't even identify them for any definition of "identify".

Let me highlight again that the question isn't whether they are useful, or a mathematically valid construction; there are all kinds of other mathematically valid constructions far stranger than the "reals". The question is whether they deserve such a fundamental place in mathematics and education. I do recall even in high school that truly understanding the real numbers even at that level was definitely a dividing point for the advanced math class; there are some who really got the quirks, and there are some who never really did and just parroted their way through the tests wondering how the question of "numbers" got so complicated... and it was still a very partial and somewhat ad-hoc introduction to the topic ("Dedekind" doesn't come up, etc.) just enough to try to motivate limits.

It's self-evident that for everyday usage all you need are the rationals.

Bingo! From a computational perspective, the non-computable reals are objects that not only require an infinite amount of memory to represent a single one, but also require an infinite amount of memory to even describe an algorithm to produce a single one. How could such an object possibly be constructed?

Can't we just produce a function from Nat -> 0|1|2|3..9? Which in effect can represent reals?

Though addition might not be defined on some of the reals, if represent it like that.

But Proof checkers like lean/coq all use Cauchy sequences to represent reals. So they are in effect constructible.

You can easily do so (usually not that specific representation) but there "are" more reals in the classical construction than you can represent with computations. Constructive mathematics just lets you say "No, this is all of them."

It never says, its all of them (Sort of LEM is working in all of them). It just says, thats all you can work with.

It's all of them. You can't give an example of a real number that's not computable.

Chaitin's omega number? I can give you an exact but incomplete equation for it, and tell you how it starts. Not every non-computable number is "pretend you could choose a random normal number, somehow".

I'm not sure if this answer is relevant, but might as well mention it.

The real numbers, infinity, etc. are abstractions. Being able to think abstractly is one of the things that make the humans different from other animals.

So from that point of view, where the real numbers exist in the same way infinity exists -- they're not really numbers but ideas about numbers. Pi isn't a number but an idea about the circle, which isn't a shape but an idea about shapes. Is that where constructive math takes you? This is all quite fascinating but totally unfamiliar to me.

They can be numbers and abstractions. There's not really any definitive singular notion of what a number is, so it wouldn't be very useful to say something like pi isn't a number. (If you can do arithmetic on it, chances are it is a number, regardless of what else it represents)

Indeed, numbers are abstractions. Even the number ‘5’ is an abstraction, let alone the numbers that cannot even be measured precisely - not even in principle.

>idea about a circle

As if a circle is a real thing. (Circles do not exist, either - or, rather, they ‘exist’ in a very particular sense of the word, as they are themselves abstractions; round things do.)

> As if a circle is a real thing. (Circles do not exist, either - or, rather, they ‘exist’ in a very particular sense of the word, as they are themselves abstractions; round things do.)

Well, yes, exactly. The thing that intrigues me about this discussion is that it seems like mathematicians have a much clearer idea than I do about what the differences between these kinds of abstractions are.

Reply on news.ycombinator.com