集合论（ZFC）之 选择公理（Axiom of Choice）注解

直观感受（Intuition）

        集合论（ZFC）中的 "C" 指的是选择公理（Axiom of Choice）中的"choice"。简单来说，对于任一非空集合 S，那么存在一个函数 f，选择出其中的元素 s ∈ S，即 s = f(S) ∈ S。

形式化（Formalization）  

        正式定义有，对于任一索引非空集合族（indexed family of non-empty set），记，{Sᵢ: i ∈ I}，其中，i for index。那么，存在一个索引集合，记，{xᵢ: i ∈ I}，使得 ∀i∈I. (xᵢ ∈ Sᵢ)。

        也就是说，存在一个选择函数 choice，使得，

∀i∈I. (choice( Sᵢ ∈ {Sᵢ: i ∈ I} ) ∈ Sᵢ )

其中，choice: {Sᵢ: i ∈ I} → Sᵢ

xᵢ = choice(Sᵢ)

注解（Annotation）

        初步看来，其实挺合理的，就是，一个非空的集合，意味着，该集合肯定包含了某些元素，又，既然包含了一些元素，那么，肯定能选取出一个元素来。

        可是，这里忽略了一点，就是，存在（existence）与能选出（choice）是两个区别的概念。而选择公理（Axiom of Choice）则规定了，只要是存在的（non-empty），那么，就能选出（choice），也就是，将这两概念等价起来了。

        这样，通过选择公理（AC），可以证明一些不可构建（non-constructable）的存在（existence）。例如，最为形象的是，Banach–Tarski 悖论。由此，也引申出不可测量集合（non-measurable sets）的概念。

        另外，选择公理（AC）隐含了（implies）排中律（Law of Excluded Middle），即，

AC → P∨¬P ≡ True

排中律，说的是，对于任一命题P，命题P为真，或∨，其反命题¬P为真。这里就产生了个有意思的逻辑。

        对于命题连接符，或∨，来说，其输出的值，由其输入决定，即，对于A∨B来说，A、B中，有一个为真（True），那么，或∨的输出为真（True）。这里有明确的输入，产生明确的输出。即，需要证明A是真，或者，B是真，才能得出， A∨B 是真。

        而对于排中律来说，不需要证明，P、¬P哪个是真，就能得出， P∨¬P 是真的。反过来说，当有 P∨¬P 为真，那么，通过 选择公理（AC），就能选择出其中为真的命题，是P，或则是¬P。即，

choice(P∨¬P) ∈ P∨¬P。

        这里，合理解析为，如果P是真，那么¬P肯定不为真；反之亦然。也就是说，对于命题P来说，不管是否能证明，命题P的真值只有真（True）与假（False）。就相当于，只要是非空集合（P∨¬P），那肯定存在一个元素，无论是 P 或 ¬P ，那么，该元素就是 choice(P∨¬P) ，使得（P∨¬P）非空，即 （P∨¬P）恒为真。即，通过，choice(P∨¬P) ，证明，P∨¬P ≡ True 。