Chaitin's constant is this amazing example of a real number that we can define, however we can not compute. However, I have a doubt in the claim that the constant is well-defined.
If I understand correctly, however this might very well be the part where I'm wrong, the way Chaitin's constant is defined is by defining a sequence of programs, and then defining the $i$'th binary digit of our number to be $1$ if the $i$'th program halts, and $0$ otherwise. If this sequence enumerates every program, then, because the halting problem is provably undecidable, the constant is uncomputable.
My problem lies in the claim that every program either will halt or not. Take for example the algorithm that enumerates every even natural number greater than $2$ and tries to write it as the sum of two primes, until it finds a number that can not be written this way, at which point it will halt. This program will halt if, and only if, the Goldbach conjecture turns out to be wrong. However, we do not even know if the Goldbach conjecture might be independent of ZFC. If the Goldbach conjecture is independent of ZFC, then is the digit of Chaitin's constant corresponding to this program well-defined?
Even if the Goldbach conjecture turns out to be dependent of ZFC, I doubt that the halting problem is dependent of ZFC for every fixed program.
EDIT: So this apparently depends on the definition of a definable number. A number does not have to be dependent of your universe to be definable. However, then the following follow up question comes to my mind.
If we define a super-definable number to be a number both definable and dependent of ZFC, does there exist a super-definable uncomputable number? Is this known?
EDIT 2: I mean "dependent of ZFC" to say there is a string of symbols in ZFC that determines the value of each digit. But then we can write a program iterating through all strings of symbols until it finds such a string, so the number is computable.