>>19
　>>15-16 より
従属選択公理
従属選択公理(英語: axiom of dependent choice;
DCと略される)とは、選択公理(AC)の弱い形で、しかし実解析の大部分を行うのに十分な公理である
使用例
このような公理が無いとしても、各 nについて普通の帰納法によって最初の n項を有限列としてとることはできる。
従属選択公理が主張しているのは、その極限であるような可算無限列が取れるということである。
従属選択公理は可算選択公理を導き、それより真に強い公理である。[4][5]

可算選択公理
応用
ZF に ACωを付け加えた公理系では、可算集合の可算和が可算であることや、任意の無限集合がデデキント無限であることなどが証明できる[1]。
実数論においては選択公理ではなく可算選択公理で事足りる場合が多い[1]。
例えば集積点が極限点であること、すなわち「xが実数Rの部分集合Sの集積点ならば、xに収束する
S∖{x}の数列が存在する」という命題を証明したい場合にはACωを用いれば十分である。
(引用終り)

＜まとめ＞
1）有限では、『このような公理が無いとしても、各 nについて普通の帰納法によって最初の n項を有限列としてとることはできる』
　つまりは、無限列の構成には、なんらかの公理が必要
2）可算選択公理があれば、『実数論においては選択公理ではなく可算選択公理で事足りる場合が多い』
　『例えば集積点が極限点であること、すなわち「xが実数Rの部分集合Sの集積点ならば、xに収束する
S∖{x}の数列が存在する」という命題を証明したい場合にはACωを用いれば十分である』
3）『従属選択公理が主張しているのは、その極限であるような可算無限列が取れるということである』
　『従属選択公理は可算選択公理を導き、それより真に強い公理である』

結論
・無限列の構成には、なんらかの公理が必要
・最低限 可算選択公理、望ましくは 従属選択公理が ほしい
・そうすれば、可算無限列が取れる
・『集積点が極限点であること、すなわち「xが実数Rの部分集合Sの集積点ならば、xに収束する
S∖{x}の数列が存在する」という命題を証明したい場合にはACωを用いれば十分である』
・『実数論においては選択公理ではなく可算選択公理で事足りる場合が多い』が
・『従属選択公理(英語: axiom of dependent choice;DCと略される)とは、選択公理(AC)の弱い形で、しかし実解析の大部分を行うのに十分な公理である』

以上により、
Ｑ：つまり(ZFCではなく)ZF上で実数は定義不可能と言いたいのですか？
Ａ：ZFに 可算選択公理、望ましくは 従属選択公理を含んでいる必要がある
　補足：有限では、『このような公理が無いとしても、各 nについて普通の帰納法によって最初の n項を有限列としてとることはできる』が、それで終り■