＞補題 任意の実数αと任意の正整数 k に対して、
＞α を小数第 k 位まで表現することができる。

任意の実数として、整数部は0で、小数第ｋ桁目が
ゲーデル数ｋの命題が真なら1、偽なら0である二進展開を持つものを選ぶと、
計算量云々ではなくて、第ｋ桁目を決定できる如何なる「算法」も存在しない。
つまり任意に与えたｋに対してそのような実数を小数第ｋ位まで表現することは
構成的には「不可能」なんだよ。カントールの対角論法の証明では、
対角線上の数字を並べて「構成した」実数が表に現れないので矛盾を引き起こす
などといっているが、そのような「構成」をすることはできない。

　だからおそらく、選択公理を密輸しているのじゃないかと思うのだよ。