良序集上的选择公理与依赖选择公理的强度比较问询

嘿，这个问题问到点子上了，咱们把核心逻辑理清楚：

首先，你提到的这个命题：

If a set A has well order, then there exist function f s.t. for each non-empty set B ∈ A, f(B)∈B.

其实这个结论完全不需要额外的选择公理加持，在ZF集合论内部就能证明！是不是有点出乎意料？原因很简单：因为A是良序的，我们可以用ZF中自带的超限归纳法来构造这个选择函数f：

• 先取A的最小元对应的非空集合B₀，因为B₀非空，ZF公理保证我们能从中选一个元素x₀，令f(B₀)=x₀；
• 假设对于A中所有排在B前面的非空集合，我们都已经给f选好了对应元素，那对当前的非空集合B，同样因为B非空，我们能从中选一个元素x，令f(B)=x；
• 由于A是良序的，不存在“无穷递降的未定义集合”，所以这个构造能覆盖A里的所有非空集合，最终得到我们需要的选择函数f。

接下来对比它和依赖选择公理（DC）的强度：

• 刚才说的这个命题是ZF的定理，也就是说只要你接受ZF的基本公理，这个结论就必然成立，它根本算不上一个“额外的选择类公理”；
• 而依赖选择公理DC是比可数选择公理（AC_ω）更强的公理，并且DC是独立于ZF的——ZF既不能证明DC，也不能反驳DC；
• 换句话说，你的这个命题的强度远弱于DC，它甚至不需要跳出ZF的框架就能成立，而DC是需要额外添加的、比它强得多的公理。

你提到它类似可数选择公理（AC_ω），这里也可以补个小澄清：AC_ω是说“可数个非空集合构成的族存在选择函数”，而你的命题中A可以是任意良序集（哪怕基数远大于ℵ₀）。不过AC_ω在ZF中不可证，这和你的命题的ZF可证性并不矛盾——AC_ω要求覆盖所有可数集合族，而你的命题只针对本身被赋予良序的集合族；虽然可数集合族在ZF中“可以”被良序化，但AC_ω的独立性是关于“统一存在选择函数”的问题，和你的命题的局部构造逻辑不冲突。

备注：内容来源于stack exchange，提问作者l4m2