構成的数学での実数の構成について
この記事は ブログ に書いた内容の写しです。
目標
可算選択公理を仮定しない構成的数学でCauchy列に基づく実数を構成する。特に、可算選択公理を使わずに完備性を証明したい。
実数を有理数の列の同値類として構成すると完備性の証明に可算選択公理が必要になりそうなので、ここでは実数を「有理数の集合の列」の同値類として定義する。
実数の構成
有理数の集合からなる列$X=(X_n)_n$, $Y=(Y_n)_n$に対し、関係$\sim$を次により定める：
$$X\sim Y\Leftrightarrow
\forall m\in\Natural.\ \forall n\in\Natural.\ \forall x\in X_m.\ \forall y\in Y_n.\ \abs{x-y}\leq 2^{-m}+2^{-n}
$$
有理数の集合からなる列$A=(A_n)_n$（ただし$A_n\subset\Rational$）が次の条件を満たすとき、正則列 (regular sequence) であるという。
- 各$A_n$は元を持つ。
- $A\sim A$
正則列に対し、$\sim$は同値関係である。
対称律は明らかで、反射律は正則列の定義である。推移律を確認する。$X\sim Y$, $Y\sim Z$とする。$x\in X_m$, $z\in Z_n$を任意に取る。$\abs{x-z}>2^{-m}+2^{-n}$と仮定して矛盾を導く（これは背理法だが、有理数に対しては大小の場合分けができる（$x< y$, $x=y$, $x>y$のうち、ちょうど一つが成り立つ）ので問題ない。）。$\abs{x-z}-2^{-m}-2^{-n}>2^{-k}$となる自然数$k$を取り、$y\in Y_{k+1}$を任意に取る。すると
\begin{align*}
\abs{x-z}=\abs{x-y+y-z}
&\leq\abs{x-y}+\abs{y-z} \\
&\leq (2^{-m}+2^{-(k+1)})+(2^{-(k+1)}+2^{-n}) \\
&=2^{-m}+2^{-k}+2^{-n}
\end{align*}
を得るが、これは$\abs{x-z}-2^{-m}-2^{-n}>2^{-k}$に反する。
正則列のなす集合を$\sim$で割ったものを$\Real$で表し、$\Real$の元を実数と呼ぶ。
$$\Real:=\{X\mid \text{$X$は正則列である}\}/{\sim}$$
実数$x$に対し、ある代表元$x=[X]$についての$X_n$の元を、$x$の第$n$有理数近似と呼ぶ。
$$\text{$a$が$x$の第$n$有理数近似である}\Leftrightarrow \exists X.\ (x=[X]\land a\in X_n)$$
実数$x$についてそれぞれの$n$に対し、第$n$有理数近似が存在するが、すべての$n$ついて一斉に選べるとは限らない（可算選択公理を仮定しないので）。
実数$x$の第$n$有理数近似からなる集合を$\Approx(x,n)$と書くことにする。
$$\Approx(x,n):=\{a\mid \exists X.\ (x=[X]\land a\in X_n)\}$$
気持ちとしては、$x=[X]$の第$n$有理数近似$a$に対して、$\abs{x-a}\leq 2^{-n}$が成り立つ（実数と有理数の差の絶対値$\abs{x-a}$はまだ定義していないので、これはあくまで「気持ち」である）。つまり、$X_n$は$x$を中心とする半径$2^{-n}$の閉区間の部分集合であるが、「実数」に言及せずに有理数の言葉だけで「正則列」を定義できているのがポイントである。
実数$x$の第$n$有理数近似のなす集合$\Approx(x,n)$は有界で、特に、すべての有理数近似の絶対値をある$K\in\Natural$を使って$\forall n.\ \forall a\in\Approx(x,n).\ \abs{a}\leq 2^K$と上から抑えられる。具体的には、ある$a_0\in \Approx(x,0)$に対して$\abs{a_0}+2\leq 2^L$となる自然数$L$に対して$K:=L$と取ることができる
（理由：$x=[X]$, $b\in X_n$に対し、
$$\abs{b}\leq\abs{b-a_0}+\abs{a_0}\leq (2^{-n}+2^0)+\abs{a_0}\leq \abs{a_0}+2\leq 2^L$$
だから）。集合の言葉で書けば、次の集合$\Bound(x)$は元を持つ：
$$\Bound(x):=\{K\in\Natural\mid\forall n.\ \forall a\in\Approx(x,n).\ \abs{a}\leq 2^K\}$$
$k\in\Bound(x)$であれば$k$以上の自然数$l$ ($l\geq k$) も$l\in\Bound(x)$である（上に閉じている）。
実数$x=[X]$, $y=[Y]$に対して、$-x$, $x+y$, $x-y$, $x\times y$, $\max\{x,y\}$, $\min\{x,y\}$, $0_\Real$, $1_\Real$を次のように定める。ただし、$k$は任意に取った$\Bound(x)\cap\Bound(y)$の元である。
\begin{align*}
-x&:=[(\{-x'\mid x'\in X_n\})_n], \\
x+y&:=[(\{x'+y'\mid x'\in X_{n+1},y'\in Y_{n+1}\})_n], \\
x-y&:=x+(-y), \\
x\times y&:=[(\{x'y'\mid x'\in X_{n+k+1},y'\in Y_{n+k+1}\})_n], \\
\max\{x,y\}&:=[(\{\max\{x',y'\}\mid x'\in X_n,y'\in Y_n\})_n], \\
\min\{x,y\}&:=[(\{\min\{x',y'\}\mid x'\in X_n,y'\in Y_n\})_n], \\
\abs{x}&:=\max\{x,-x\}, \\
0_\Real&:=[(\{0\})_n]=[(\{0\},\{0\},\{0\},\dotsc)], \\
1_\Real&:=[(\{1\})_n]=[(\{1\},\{1\},\{1\},\dotsc)].
\end{align*}
def:basic-operationsはwell-definedである。
$x\times y$だけwell-defined性を確認しておく。正則列であることの条件のうち、元を持つことは明らかである。以下では、正則列の残りの条件と、代表元（正則列）および$k$の選び方に依存しないことの確認をまとめて行う。
$X\sim X'$, $Y\sim Y'$とし、$k,k'\in\Bound(x)\cap\Bound(y)$とする。
$$Z_n=\{x'y'\mid x'\in X_{n+k+1},y'\in Y_{n+k+1}\},\quad
Z'_n=\{x'y'\mid x'\in X'_{n+k'+1},y'\in Y'_{n+k'+1}\}$$
として、$Z\sim Z'$を示せばよい。$x\in X_{m+k+1}$, $y\in Y_{m+k+1}$, $x'\in X'_{n+k'+1}$, $y'\in Y'_{n+k'+1}$, $z=xy\in Z_m$, $z'=x'y'\in Z'_n$として、
\begin{align*}
\abs{z-z'}&=\abs{xy-x'y'} \\
&=\abs{x(y-y')+(x-x')y'} \\
&\leq\abs{x}\cdot\abs{y-y'}+\abs{x-x'}\cdot\abs{y'} \\
&\leq 2^{\min\{k,k'\}}\cdot(2^{-(m+k+1)}+2^{-(n+k'+1)})+(2^{-(m+k+1)}+2^{-(n+k'+1)})\cdot 2^{\min\{k,k'\}} \\
&=2^{\min\{k,k'\}}\cdot(2^{-(m+k)}+2^{-(n+k')}) \\
&\leq 2^{-m}+2^{-n}
\end{align*}
を得る。ただし、$k$, $k'$の選び方より$\abs{x},\abs{y}\leq 2^{\min\{k,k'\}}$となることを使った。
普通の数学の慣習のように、$x\times y$のことを$x\cdot y$あるいは$xy$と表記することがある。
実数は可換環をなす。
- $(x+y)+z=x+(y+z)$
- $x+y=y+x$
- $x+0_\Real=0_\Real+x=x$
- $x+(-x)=(-x)+x=0_\Real$
- $(xy)z=x(yz)$
- $xy=yx$
- $x\times 1_\Real=1_\Real\times x=x$
- $x(y+z)=xy+xz$
- $(x+y)z=xz+yz$
有理数$q$に対して、実数$\inQR(q)$を
$$\inQR(q):=[(\{q\})_n]=[(\{q\},\{q\},\{q\},\dotsc)]$$
により定める。
$\inQR$は単射な環準同型である。つまり、有理数$x,y\in\Rational$に対して、以下が成り立つ：
- $\inQR(x)=\inQR(y)$ならば$x=y$
- $\inQR(0)=0_\Real$, $\inQR(1)=1_\Real$
- $\inQR(x+y)=\inQR(x)+\inQR(y)$
- $\inQR(-x)=-\inQR(x)$
- $\inQR(xy)=\inQR(x)\inQR(y)$
実数$x=[X]$, $y=[Y]$に対して、関係$<$および$\leq$を次のように定める：
\begin{align*}
x< y&:\Leftrightarrow \exists n.\ \exists a\in X_n.\ \exists b\in Y_n.\ 2^{-n+2}\leq b-a, \\
x\leq y&:\Leftrightarrow \forall n.\ \forall a\in X_n.\ \forall b\in Y_n.\ {-2^{-n+1}}\leq b-a,
\end{align*}
$<$と$\leq$はそれぞれwell-definedである。
$<$について：$X\sim X'$, $Y\sim Y'$として、$[X]<[Y]$ならば$[X']<[Y']$であることを示す。$[X]<[Y]$より、ある$n$と$a\in X_n$, $b\in Y_n$に対して$2^{-n+2}\leq b-a$となる。$a'\in X'_{n+2}$, $b'\in Y'_{n+2}$を一つずつ取る。
\begin{align*}
b'-a'&=(b'-b)-(a'-a)+(b-a) \\
&\geq -(2^{-(n+2)}+2^{-n})-(2^{-(n+2)}+2^{-n})+2^{-n+2} \\
&=-2^{-(n+2)}+2^{-n+1} \\
&\geq 2^{-(n+1)}+2^{-n} \\
&>2^{-n}=2^{-(n+2)+2}
\end{align*}
よって、$[X']<[Y']$である。
$\leq$について：$X\sim X'$, $Y\sim Y'$として、$[X]\leq[Y]$ならば$[X']\leq[Y']$であることを示す。$a'\in X'_n$, $b'\in Y'_n$を任意に取る。$b'-a'<-2^{-n+1}$と仮定して矛盾を導く（比較対象が有理数なのでこの背理法も問題ない。）。$b'-a'+2^{-m+2}<-2^{-n+1}$となるような自然数$m$を取って固定する。$a\in X_m$, $b\in Y_m$を取って固定する。すると
\begin{align*}
b'-a'&=(b'-b)-(a'-a)+(b-a) \\
&\geq -(2^{-n}+2^{-m})-(2^{-n}+2^{-m})-2^{-m+1} \\
&=-(2^{-n+1}+2^{-m+2})
\end{align*}
となるが、これは$m$の選び方に反する。よって、$b'-a'\geq-2^{-n+1}$である。
実数$x$, $y$, $z$について、以下が成り立つ。
- $x< y$と$y\leq x$は両立しない。$x< y$ならば$\lnot(y\leq x)$で、$y\leq x$ならば$\lnot(x< y)$である。
- $\lnot(x< y)$ならば$y\leq x$である。
- $x\leq x$である。
- $x< y$ならば$x\leq y$である。
- $x< y$かつ$y< z$ならば$x< z$である。
- $x< y$かつ$y\leq z$ならば$x< z$である。
- $x\leq y$かつ$y< z$ならば$x< z$である。
- $x\leq y$かつ$y\leq z$ならば$x\leq z$である。
1について：$x=[X]$, $y=[Y]$に対して、$x< y$かつ$y\leq x$と仮定する。$x< y$より、$\forall a\in X_n.\ \forall b\in Y_n.\ 2^{-n+2}\leq b-a$となる$n$が存在する。そのような$n$を一つ固定し、$a\in X_n$, $b\in Y_n$も固定する。一方、$y\leq x$より、$-2^{-n+1}\leq a-b$で、合わせて
$$2^{-n+2}\leq b-a\leq 2^{-n+1}$$
となり、矛盾する。
2について：$x=[X]$, $y=[Y]$に対して、$\lnot(x< y)$と仮定する。$n$を任意に取り、$c\in Y_n$, $d\in X_n$を任意に取る。$d-c<-2^{-n+1}$と仮定して矛盾を導く。$d-c+2^{-m}<-2^{-n+1}$となる$m$を取って固定する。仮定より、任意に取った$a\in X_{m+3}$, $b\in Y_{m+3}$に対して$b-a<2^{-m-1}$である。すると、
\begin{align*}
d-c&=(d-a)-(c-b)-(b-a) \\
&>-(2^{-n}+2^{-m-3})-(2^{-n}+2^{-m-3})-2^{-m-1} \\
&>-2^{-n+1}-2^{-m}
\end{align*}
となり、$d-c+2^{-m}<-2^{-n+1}$に反する。よって、$d-c\geq-2^{-n+1}$である。
3について：$x=[X]$とする。$n$を任意に取り、$a\in X_n$, $b\in X_n$も任意に取る。正則列の定義より
$$\abs{b-a}\leq 2^{-n}+2^{-n}=2^{-n+1}$$
で、これは$-2^{-n+1}\leq b-a$を意味する。
4について：$x=[X]$, $y=[Y]$に対して、$x< y$と仮定する。$x< y$より、$2^{-n+2}\leq b-a$となる$n\in\Natural$, $a\in X_n$, $b\in Y_n$が存在するので、それらを一つ固定する。自然数$m$を任意に取り、$a'\in X_m$, $b'\in Y_m$を任意に取る。
\begin{align*}
b'-a'&=(b'-b)-(a'-a)+(b-a) \\
&\geq -(2^{-m}+2^{-n})-(2^{-m}+2^{-n})+2^{-n+2} \\
&=-2^{-m+1}+2^{-n+1} \\
&>-2^{-m+1}
\end{align*}
よって、$x\leq y$である。
以降は省略する。
有理数$a$, $b$に対して、以下が成り立つ。
- $a< b\Leftrightarrow\inQR(a)<\inQR(b)$
- $a\leq b\Leftrightarrow\inQR(a)\leq\inQR(b)$
以後、有理数$a$に対して$\inQR(a)$のことを単に$a$と表記することがある。また、$x< y$のことを$y>x$とも書き、$x\leq y$のことを$y\geq x$とも書く。
実数$x$, $y$, $z$について、以下が成り立つ：
- $0\leq x$, $0\leq y$ならば$0\leq x+y$, $0\leq xy$である。
- $0< x$, $0< y$ならば$0< x+y$, $0< xy$である。
- $0< x$, $0\leq y$ならば$0< x+y$である。
- $0\leq\abs{x}$である。
- $0< x$ならば$0<\max\{x,y\}$である。
- $0\leq x$ならば$0\leq\max\{x,y\}$である。
- $0\leq x$かつ$0\leq y$ならば$0\leq\min\{x,y\}$である。
- $0< x$かつ$0< y$ならば$0<\min\{x,y\}$である。
- $x< y$ならば、$x+z< y+z$である。
- $x\leq y$ならば、$x+z\leq y+z$である。
実数$x=[X]$の第$n$有理数近似$a\in X_n$について、
$$\abs{x-a}\leq 2^{-n}$$
である。
任意の$m\in\Natural$, $b\in X_m$に対して$-2^{-m+1}\leq 2^{-n}-\abs{b-a}$を示したい。これは$X$が正則列であることから
$$\abs{b-a}\leq 2^{-m}+2^{-n}<2^{-m+1}+2^{-n}$$
より成り立つ。
古典的な数学では、0ではない実数は逆数を持つ。しかし、構成的には「0でない」つまり「0と等しいと仮定すると矛盾する」では逆数を構成する条件としては弱く、割る数は「0から離れた実数」であって、「0との距離」を具体的な正の数として見積もれる必要がある。そこで、実数同士が「離れていること (apartness)」を表す関係$\ineq$を導入する。
実数上の関係$\ineq$を次のように定める：
$$x\ineq y:\Leftrightarrow x< y\mathrel{\text{または}}y< x$$
$x=[X]$, $y=[Y]$に対し、$x\ineq y$は
$$\exists n.\ \exists a\in X_n.\ \exists b\in Y_n.\ 2^{-n+2}\leq\abs{b-a}$$
と同値である。
実数$x=[X]$が$x\ineq 0$を満たすとき、$x$の逆数$x^{-1}$を次のように定義する：
\begin{align*}
x^{-1}&:=[Y], \\
Y_n&:=\{a^{-1}\mid a\in X_{2N+\max\{n,N\}}\}
\end{align*}
ただし、ある$a_0\in X_N$について$2^{-N+2}\leq\abs{a_0}$が成り立つように$N$を取る（$x\ineq 0$よりそのような$N$を取れる）。
$x\ineq 0$のとき、
- $x^{-1}$はwell-definedである。つまり、$a\in X_{2N+\max\{n,N\}}$は0ではなく、$Y$は正則列であり、$x^{-1}$は$X$と$N$の選び方に依存しない。
- $xx^{-1}=1$である。
- $0< x$ならば$0< x^{-1}$である。
- $x<0$ならば$x^{-1}<0$である。
1について：まず、$a\in X_{2N+\max\{n,N\}}$が0でないことを確認する。
\begin{align*}
\abs{a}&\geq\abs{(a_0-a)+a}-\abs{a_0-a} & (\text{三角不等式}) \\
&=\abs{a_0}-\abs{a_0-a} \\
&\geq 2^{-N+2}-(2^{-(2N+\max\{n,N\})}+2^{-N}) \\
&\geq 2^{-N+2}-(2^{-N}+2^{-N}) \\
&=2^{-N+1}
\end{align*}
より、$a\neq 0$である。
次に、$Y$が正則列であることの条件のうち、各$Y_n$が元を持つことは明らかである。
最後に、$Y\sim Y$と、$[Y]$が$a_0$と$N$の選び方に依存しないことをまとめて示す。$a_0\in X_M$について$2^{-M+2}\leq\abs{a_0}$が成り立ち、$b_0\in X_N$について$2^{-N+2}\leq\abs{b_0}$が成り立つとする。一般性を失わずに$M\leq N$と仮定する。
$$Y_n:=\{a^{-1}\mid a\in X_{2M+\max\{n,M\}}\},\quad
Z_n:=\{b^{-1}\mid b\in X_{2N+\max\{n,N\}}\}$$
とおいて、$Y\sim Z$を示したい。$m$, $n$, $a^{-1}\in Y_m$, $b^{-1}\in Z_n$を任意に取った時に、$\abs{a^{-1}-b^{-1}}\leq 2^{-m}+2^{-n}$が成り立つことを示せば良い。まず、
$$\abs{a-a_0}\leq 2^{-(2M+\max\{m,M\})}+2^{-M}\leq 2^{-M+1}$$
に注意すると、
\begin{align*}
\abs{a}&\geq\abs{(a_0-a)+a}-\abs{a_0-a} & (\text{三角不等式}) \\
&=\abs{a_0}-\abs{a_0-a} \\
&\geq 2^{-M+2}-2^{-M+1} \\
&=2^{-M+1}
\end{align*}
である。$b$についても、$M\leq N$より
$$\abs{b-a_0}\leq 2^{-(2N+\max\{n,N\})}+2^{-M}\leq 2^{-M+1}$$
に注意すると同様に$\abs{b}\geq 2^{-M+1}$を得る。これらを使うと、
\begin{align*}
\abs{a^{-1}-b^{-1}}
&=\abs{\frac{b-a}{ab}} \\
&\leq \frac{2^{-(2N+\max\{n,N\})}+2^{-(2M+\max\{m,M\})}}{2^{-M+1}\cdot 2^{-M+1}} \\
&\leq \frac{2^{-(2M+n)}+2^{-(2M+m)}}{2^{-M+1}\cdot 2^{-M+1}} \\
&=\frac{2^{-n}+2^{-m}}{4} \\
&<2^{-m}+2^{-n}
\end{align*}
を得る。よって$Y\sim Z$である。
残りは面倒なので省略する。
$y\ineq 0$のとき、$xy^{-1}$のことを$x/y$あるいは$\frac{x}{y}$と表記することもある。
実数$x$, $y$について$x+y>0$ならば、$x>0$または$y>0$が成り立つ。
仮定$x+y>0$より、ある$m$について、ある$a\in X_{m+1}$, $b\in Y_{m+1}$が取れて、$2^{-m+2}\leq a+b$となる。このとき、有理数の性質より$2^{-m+1}\leq a$または$2^{-m+1}\leq b$が成り立つ。前者ならば$x>0$で、後者ならば$y>0$である。
実数$x$, $y$, $z$について、$y< z$が成り立つならば、$x< z$または$y< x$が成り立つ。
仮定より$0< z-y=(z-x)+(x-y)$なので、prop:plus-gtより$0< z-x$または$0< x-y$が成り立つ。
古典的には実数全体の集合$\Real$は非可算で、Bishopの構成的数学でも同等の命題が証明できる。しかし、証明の中で「与えられた可算列に対して被らない実数を構成する」ためには従属選択公理か弱ケーニヒの補題（Weak Kőnig's Lemma; WKL）に相当する何かが必要と思われる。そのため、ここでは「実数の非可算性」の証明は試みない。実際のところ、可算選択公理やWKLが成り立たない環境では実数が可算であっても不思議ではないが、筆者の力量不足のため、「実数が可算となるモデルを作る」こともここでは試みない。
実数列の収束
ここまでで、実数の四則演算ができるようになった。しかし、実数の応用、例えば指数関数や三角関数の定義の際には、有限回の四則演算だけでは足りず、何らかの極限操作が必要になる。そこで、実数列の収束と極限を定義する。
実数列$(x_n)_n$と実数$X$が以下の条件を満たすとき、$(x_n)_n$は$X$に収束する (converge) という：任意の$k\in\Natural$に対し、ある$N_k\in\Natural$が存在し、$n\geq N_k$を満たす任意の$n\in\Natural$について
$$\lvert x_n-X\rvert\leq 2^{-k}$$
このとき、$X$を$(x_n)_n$の極限 (limit) といい、
$$\lim_{n\to\infty} x_n=X$$
あるいは「$n\to\infty\mathrel{\text{のとき}}x_n\to X$」と表記する。
実数列$(x_n)_n$は極限を持つとき、収束するという。
この条件を記号で書けば、
$$\forall k\in\Natural.\ \exists N_k\in\Natural.\ \forall n\in\Natural.\ (n\geq N_k\Rightarrow \lvert x_n-X\rvert\leq 2^{-k})$$
となる。
実数列$(x_n)_n$の極限は存在すれば一意である。つまり、$n\to\infty$のとき$x_n\to X$かつ$x_n\to X'$であれば、$X=X'$である。
実数を導入する動機の一つが、「収束しそうな有理数列（有理数のCauchy列）の極限が有理数の中にない」というものだった。そして、そういう数列の極限は実数として構成できるのだった。次に気になるのは、「収束しそうな実数列（実数のCauchy列）の極限が実数の中にあるか」という問題である。古典的にはこれは当たり前なのだが、可算選択公理を仮定しないような弱い体系では自明ではない。そもそも、Cauchy列の定義が複数種類に分裂するのである。
なお、実数を定義するのに使った「正則列」は集合の列として定義したが、ここで定義する「実数のCauchy列」は点列として定義する。
実数列$(x_n)_n$がCauchy列であるとは、以下が成り立つことを言う：
$$\forall\varepsilon>0.\ \exists N_0\in\Natural.\ \forall m\geq N_0.\ \forall n\geq N_0.\ \lvert x_m-x_n\rvert<\varepsilon$$
実数のCauchy列$(x_n)_n$に対する収束の尺度 (modulus of convergence) あるいは収束率とは、自然数から自然数への写像$M\colon\Natural\to\Natural$であって以下を満たすもののことである：
$$\forall k\in\Natural.\ \forall m,n\geq M(k).\ \lvert x_m-x_n\rvert<2^{-k}$$
“modulus of convergence” の日本語の訳語は、筆者の知る限り、標準的なものはまだない。「収束率」はどこかのWeb記事で見かけた訳である。「収束の尺度」は筆者が考えた直訳である。
可算選択公理の下では、実数のCauchy列は収束の尺度を持つ。
実数のCauchy列$(x_n)_n$とその収束の尺度$M$および自然数$k$, $l$について、
$$\abs{x_{M(k)}-x_{M(l)}}\leq 2^{-k}+2^{-l}$$
が成り立つ。
$M(k)\leq M(l)$ならば
$$\abs{x_{M(k)}-x_{M(l)}}<2^{-k}<2^{-k}+2^{-l}$$
となる。$M(k)\geq M(l)$ならば
$$\abs{x_{M(k)}-x_{M(l)}}<2^{-l}<2^{-k}+2^{-l}$$
となる。
$(x_n)_n$が収束するならば$(x_n)_n$はCauchy列である。
逆に、実数列$(x_n)_n$がCauchy列であり、$M$が$(x_n)_n$の収束の尺度であれば、$(x_n)_n$は収束する。
（収束するならばCauchy列）$X=\lim_{n\to\infty} x_n$とする。$\varepsilon>0$が与えられたとする。$2^{-k}<\varepsilon$を満たす自然数$k$を取る。収束の定義より、$n\geq N\Rightarrow\lvert x_n-X\rvert\leq 2^{-(k+1)}$となるような自然数$N$を取れる。$m,n\geq N$の時、
\begin{align*}
\lvert x_m-x_n\rvert
&\leq\lvert x_m-X\rvert+\lvert X-x_n\rvert \\
&\leq 2^{-(k+1)}+2^{-(k+1)} \\
&=2^{-k}<\varepsilon
\end{align*}
である。
（収束の尺度を持つCauchy列は収束する）有理数の集合の列$(Y_n)_n$を次のように定める：
$$Y_n:=\Approx(x_{M(n+1)},n+1)$$
主張．$(Y_n)_n$は（有理数の）正則列である。
$a\in Y_m$, $b\in Y_n$に対して、prop:rational-approximationにより、
\begin{align*}
\lvert a-b\rvert
&\leq \lvert a-x_{M(m+1)}\rvert+\lvert x_{M(m+1)}-x_{M(n+1)}\rvert+\lvert x_{M(n+1)}-b\rvert \\
&\leq 2^{-(m+1)}+2^{-(m+1)}+2^{-(n+1)}+2^{-(n+1)} \\
&\leq 2^{-m}+2^{-n}
\end{align*}
を得る。
（主張の証明終わり）
$y:=[Y]$とおく。
主張．$y=\lim_{n\to\infty} x_n$である。
$n\geq M(k+3)$、$a\in Y_{k+2}$とした時、
\begin{align*}
\lvert y-x_n\rvert
&\leq \lvert y-a\rvert+\lvert a-x_{M(k+3)}\rvert+\lvert x_{M(k+3)}-x_n\rvert \\
&\leq 2^{-(k+2)}+2^{-(k+2)}+2^{-(k+3)}
<2^{-k}
\end{align*}
なので、$N_k=M(k+3)$と取れる。
古典的には実数の集合について「上に有界な非空集合には上限が存在する」ことが言えるが、構成的にはこれは証明できない。詳しくはSpecker列 (Specker sequence) で調べてほしい。
雑感
構成的数学では集合を第一級の対象として扱うことに躊躇がある気がする（例：同値類による商集合の構成の代わりに、setoidを使う。もっと一般に言うと、冪集合公理を制限する）。そういう場合に「集合からなる列」という代物を気軽に使って良いものか。まあ、集合を自在に扱えないならmulti-valued functionみたいな概念を使えば良い話なので、本質的な制限にはならないと信じたい。
いくつかの命題の証明は退屈なので省略した。そういう命題は手元で真面目に証明したわけではないが、他の定義に大きな変更を加えることなく成立すると信じている。真面目にやるのであれば、そういう退屈な命題の証明を定理証明支援系で与えておくべきなのかもしれない。
可算選択公理を仮定しない環境下で実数（もっと言うと、距離空間的なものの完備化）を構成するために集合の列を使うというアイディアは、Handbook_of_Constructive_Mathematics, FTA_Constructiveを参考にした。これらにはさらに元ネタ（Stolzenberg, G. Sets as Limits）があるらしいが、入手困難で辿れていない。
