查看“︁选择公理”︁的源代码

[[分类:公理集合论]]
{{InfoBox
|name=选择公理
|eng_name=axiom of choice
|aliases=AC,AoC
}}
{{InfoBox
|name=选择映射
|eng_name=choice function
|aliases=选择子,selector,selection
}}
'''选择公理'''('''axiom of choice''')，缩写为 '''AC''' ，指[[:分类:公理集合论|公理集合论]]中的一个[[公理（逻辑）|公理]]，这一公理假设对任意多个[[集合]]，总是能找到一种取数方式，使得我们可以从中每个集合中取出刚好一个元素。即使这里涉及的集合有无限多个也可以找到。

选择公理在 [[ZF 公理系统]]下是一个[[独立性|独立]]的命题。换句话说，已证明添加了选择公理的公理系统（称为 [[ZFC 公理系统]]）和添加了其否命题的公理系统（称为 ZF¬C 公理系统）均是[[一致性|一致]]的。

== 公理 ==

对非空集合构成的集族 <math>X</math> ，存在 <math>X</math> 上的'''选择映射''' <math>f</math> ，使得 <math>\forall A \in X (f(A)\in A)</math> 。

或者使用符号

<math>\forall X [\varnothing \notin X \rightarrow \exists f: X\to \bigcup_{A\in X} A (\forall A \in X(f(A) \in A))]</math>

注：一般需要定义[[映射]]来表述选择公理，这里映射依赖于关系的定义，关系依赖于集合上的笛卡尔积，而笛卡尔积可以只依赖幂集公理、对集公理、并集公理定义。所以可以先通过 ZF 公理系统下其他公理构造出映射的定义后再次引入选择公理。

== 琐事 ==

最常见的等价命题是[[良序公理]]和 [[Zorn 引理]]。

=== 争议 ===

在 ZF 模型上，引入 AC 这一公理会给模型带来较好的性质。事实上，一系列有较好性质的公理在引入 ZF 时都等价于引入选择公理，即使是集合的势在超限基数范围内也需要选择公理才能被确认为不同大小的层级。但是由于已知 AC 独立于 ZF ， AC 不总是被看作必要的。需要选择公理时，往往涉及在任意结构的对象中以某种无法明确表达出的方式取得一个对象，导致这一对象无法被构造地存在；此外，在出现需要同时从不可数无穷个集合中选择元素的这一本身就反直觉的情况中，往往会给出无法确认的存在元素。这些都使得选择公理的使用存在争议。