For the definition of a semicomputable real, see An Introduction to Kolmogorov Complexity and its Applications by Li and Vitanyi (1997). In fact, it is not true that every Cauchy sequence for completion of rationals is semicomputable, we can not complete rationals by semicomputable Cauchy sequences.
My question:
1, how could in Constructivism way based on Cauchy sequence we complete the rational number system? specifically, how to overcom the non-computable problem of some (in fact,uncountably many) Cauchy sequence by which to complete rationals system?
2, Since we complete rational number system in several ways like Cauchy seqence,Dedekind cut or even by continued fraction, what is the common ideas (of approach,etc) among them?