I just watched a video that shows how real numbers are constructed using Dedekind cuts, and what I understood was that a real number is a subset of Q which, among a few other conditions, contains no greatest element. The video also shows an example of how this property can be proven for $\sqrt 2$. I also found these proofs for $pi$ and $e$.
I was wondering if there was another way to construct the reals using Turing machines, since the Dedekind cut feels a bit like a "by negation" kind of definition, and a Turing machine would be more of a procedural, actual way to construct them. But it turns out Turing machines are countable and reals are not, so there must be real numbers that can't be computed by Turing machines.
Which then led me to this other question, in which they give a few samples of non-computable real numbers. But now I wonder, given any of these numbers (say Chaitin's constant), can we prove that the Dedekind cut that corresponds to this number (and to every other number that we intuitively think of as a real number) has no greatest element? Or could it be the case that Chaitin's constant turns out to be a non-real number (which I have no idea what it'd even mean, since it definitely seems to be a point on the real line)?
I know there are other ways to construct real numbers that I haven't learned about yet, so perhaps one of them can be used to prove it?