Wikipedia claims that there exist Cauchy sequences of definable numbers whose limit is not definable. Are there constructive proofs of this? If so, what is an example of a Cauchy sequence of definable reals whose limit is undefinable?
Also, does this claim hold for definable sequences of definable numbers? It makes sense to me that such sequences might exist if the Cauchy sequence itself is undefinable (an undefinable sequence of definable numbers), but if the definition of the Cauchy sequence can be specified with a finite amount of information, it seems somewhat paradoxical to me.
Yes so you answered your own question essentially. As David noted in his answer any real is the limit of a sequence of rationals, and all rationals are definable, but if you want a definable sequence of reals, then if it has a limit the limit too will be definable (under any reasonable definition of "definable").