Agda康托尔定理 (4-3)

延伸阅读

康托尔的著名定理指出，幂集的基数P(A)大于的基数 A有几种等同的配方，我想考虑的是

定理（康托尔）：地图上没有A → P(A).

在这篇文章中，我想分析康托尔定理的通常证明，并提出一个有洞察力的重新表述，它在集合论之外具有应用。这里写的所有内容都很容易，远非新的，但在我看来，仍然足够有趣，可以呈现给更多的观众。

如果我们打开一本关于集合论的书，我们会发现康托尔定理的证明，它明确地表明，对于每个映射e：A → P(A)有一个子集A在其形象之外，即

S＝{x ∈A│x ∉ e(x)}

如果我们有S＝e(y)对于一些人来说y∈A它将遵循这两个y是，也不是S.第一个观察是，这是一个构造有效的证明，因此康托尔定理在直觉集合论中同样成立。但这个定理的范围到底有多宽呢？让我们尽可能抽象地重新设计它，使它具有更广泛的适用性。

首先我们更换电源组 P(A) 使用函数集 Ωᴬ 其中 Ω 是真理值的集合。在经典逻辑的情况下Ω＝{0，1}但没有必要依赖这个事实。我们更愿意考虑真值对应于单例集子集的一般情况{0}，使Ω＝P({0}).之间的双射P(A)和 Ωᴬ 然后，只是子集和它们的特征映射之间的通常一个：一个子集 SsubseteqA对应于地图 χs(x)＝{u ∈ {0}│x ∈ S}，而一张地图χ：A → Ω 对应于子集

{x ∈ A│0 ∈ χ(x)}.

逻辑取反 ¬ 可以看作是一张地图 N：Ω → Ω 定义由N(p)＝{u ∈ {0}│0 ∉ p}.请注意 N 没有固定点，因为如果有 p∈Ω 使得 N(p)＝p 那我们就两个都有了 0∈p 和0 ∉ p.

现在我们的证明如下：假设我们有一张地图e：A → Ωᴬ 考虑地图 s：A → Ω 定义由

s(x)＝N(e(x)(x)).如果有y∈A使得s＝e(y)，我们会 e(y)(y)＝s(y)＝N(e(y)(y))，矛盾。因此 e不在。QED。这怎么比我们以前好？它给了我们一个机会来思考 正的情况的各个方面：如果e然后，我们就开始了 Ω 没有固定点就不能有内图。因为证据中没有任何东西特别依赖于 Ω 作为通过值的集合，我们可以用一般集合替换它，以获得：

定理（劳维尔）：如果有地图 e：A → Bᴬ 然后每 f：B → B 有一个固定点。

我们已经知道如何证明这一点：考虑地图s：A → B 定义由s(x)＝f(e(x)(x)).因为 e 是上，有y∈A使得e(y)＝s.那么我们有 e(y)(y)＝s(y)＝f(e(y)(y))，因此 e(y)(y) 是一个固定点 f.

QED。

康托尔定理是劳维尔定理的推论B＝Ω而观察比否定没有不动点。

现在孤立地考虑劳维尔定理，以及如何证明它，也许是这样的：我怎么能有这样的地图e：A → Bᴬ?当然 B 不能有太多的元素，事实上，只有在 B 是单例或空例。我可以看到劳维尔定理显然是正确的，但它是垃圾，因为它只在微不足道的情况下成立。最后一句有一个错误：正如我们很快将看到的，劳维尔定理在有趣的情况下是正确的，但是 你（想象中的数学家，而不是本博客的读者......)只能在琐碎的情况下想象它，因为你懒得去看狭窄的集合论范围之外。

劳维尔定理是康托尔定理的核心对角线化技巧的积极重新表述。它可以在任何笛卡尔闭范畴中表述，它的证明只使用了方程推理和少量的一阶逻辑。我们应该期望它比康托尔定理有更广泛的适用性。事实上，我们立即看到，其他众所周知的对角线证明是推论，例如：

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。