>>519
>有理コーシー列全体の集合X上の同値関係〜を「{an}〜{bn}⇔lim[n→∞](an-bn)=0」で定義し、商集合X/〜上の加法・乗法・全順序・極限を適当に定義すればX/〜が完備順序体であることを示せる。
>上記において何らの選択公理も不要。

ご苦労さま

(google検索)
有理コーシー列と選択公理の関係
AI による概要
1. 実数構成におけるコーシー列と選択公理
選択公理の役割: 可算個の空でない集合の族から、それぞれの集合の元を1つずつ選ぶ関数が存在することを保証するのが「可算選択公理」です。コーシー列を用いた完備性の証明などで、この公理が背景にあると解釈されます
2. 公理を仮定しない場合（構成的数学）
可算選択公理を仮定しない「構成的数学」の文脈では、Cauchy列に基づいた実数の構成において、通常の完備性が示せなくなる、あるいは構造が弱まる可能性があります
Modulated Cauchy列: 可算選択公理を使わずに実数を構成するため、コーシー列に「どのくらいの速さで収束するか」という情報（モジュラス）を含めた「modulated Cauchy列」が使われることがあります
結論として、有理コーシー列を用いた実数の定義は、現代的な数学の集合論（ZF）において、コーシー列の収束性と完備性を示す際に可算選択公理の助けを借りる関係にあります

https://blog.miz-ar.info/2025/08/real-construction-without-countable-choice/
雑記帳
人生やっていき
可算選択公理を仮定しない構成的数学での実数の構成について
2025年8月16日
可算選択公理を仮定しない構成的数学では、Cauchy列に基づいた実数の構成をやるときに完備性が示せなくなる（らしい）。この弱点は、実数の構成に使うCauchy列を有理数の点列ではなく、有理数の集合の列とすれば克服できる。

このことは「Handbook of Constructive Mathematics」のFred Richmanの記事で示唆されているが、あまり詳しい取扱いはなかったので自分でやってみた。と言っても、地味な命題の証明は省略しているが……。

https://miz-ar.info/math/real-construction-without-choice-20250816.pdf
Mathlogにも書いてみた。
構成的数学での実数の構成について | Mathlog