[wiml]

Any HN comment is a finite expression, so it's impossible for me to specify a particular one. But the number of finite expressions is countable, and the number of reals is vastly more than a countable number, so most reals cannot be described in any human sense.

[bjourne]

If you can't specify it or describe it how do you know it exists?

[wiml]

I think (I am not a mathematician) that depends on whether you accept non-constructive proofs as valid. Normally you reason that any mapping from natural numbers onto the reals is incomplete (eg Cantor's argument), and that the sets of computable or describable numbers are countable, and therefore there exist indescribable real numbers. But if you don't like that last step, you do have company:

https://en.wikipedia.org/wiki/Constructivism_%28philosophy_o...

[afiori]

There are more infinite sequences than finite ones.

So not all infinite sequences can be uniquely specified by a finite description.

Like √2 is a finite description, so is the definition of π, but since there is no way to map the abstract set of "finite description" surjectively to the set of infinite sequences you find that any one approach will leave holes.

[bjourne]

But doesn't this assume what you intend to show? Of course you can't specify an infinite and non-repeating sequence, but how do you know that is a number?

[afiori]

> but how do you know that is a number?

Quick answer: math[0]

Slightly longer answer decimal numbers between 0 and 1 can be written as the sum of a_0*10^0 + a_1*10^1 + a_2*10^2 + ... + a_i*10^i + ... where a_i is one of 0,1,2,3,4,5,6,7,8,9. for series in this shape you can prove that the sum of two series is the same iff and only if the sequence of digits are all the same (up to the slight complication of 0.09999999 = 0.1 and similar)

[0] https://en.wikipedia.org/wiki/Series_(mathematics)

[hanche]

You can't know. However, it is a consequence of the axiom of choice (AC). You can't know if AC is true either; but mathematics without it is really really hard, so it usually assumed.