超小小中大超大

Agda康托尔定理

好书推荐：多重宇宙：离婚后，为她一夜白头、喜美：朦胧梦境、梦断南宫、快穿之天生媚骨、清冷钓系美人每天都在修罗场、我在泰娱哦！、一个誓言走一世、穿书后恶毒女配只想修仙、小甜文双男主合集、我靠养鱼，日常变美、

Agda康托尔定理 ▹

前置知识 ▹

康托尔定理（直接证） ▹

Lawvere不动点定理 ▹

存在不可数集合 ▹

康托尔定理(用Lawvere不动点定理证） ▹

延伸阅读

康托尔的著名定理指出，幂集的基数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 是单例或空例。我可以看到劳维尔定理显然是正确的，但它是垃圾，因为它只在微不足道的情况下成立。最后一句有一个错误：正如我们很快将看到的，劳维尔定理在有趣的情况下是正确的，但是你（想象中的数学家，而不是本博客的读者......)只能在琐碎的情况下想象它，因为你懒得去看狭窄的集合论范围之外。

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

1.数字序列的集合 ℕ → ℕ 是不可数的，因为后继操作没有固定点。

2.没有连续的涌动 ℝ → C(ℝ，ℝ)从实线到连续实函数的Banach空间，配备了紧开放拓扑，因为实图 x↦x＋1 是连续的，没有固定点。

更有趣的是，劳维尔定理也有积极的结果：

1.为了对比上面的第二种情况，我们问是否有一个连续的推测 ℝ 上 C (ℝ，[0，1])，连续实函数在闭区间上取值的空间，并配备了超度量。如果存在这样的映射，则闭合区间具有定点性质，而且每个立方体 [0，1]ⁿ 也有定点属性（练习）。所以这可能是一个很好的方法来证明布劳尔不动点定理，即使它不起作用，它也是一个好主意，会让你思考空间填充曲线有一段时间。

2.在有效的托波斯的 c.e 集被表示为地图Σℕ其中 Σ 是一组半决定的真理价值观。因为有一个有效的枚举c.e.集合，在有效的拓扑图中，有一个onmap W：ℕ → Σℕ，这立即告诉我们Σ具有定点属性，也是 Σℕ 因为它同构于(Σℕ)ℕ因此，我们得到了可计算性理论中的一个定理，指出每枚举运算符有一个固定点。

最后，让我评论一下保罗·斯塔德曼的问题在FOM邮件列表中。他想知道分离的公理（又名）证明康托尔定理需要子集公理。如果我们只在直集理论中工作，那么有界的分离当然足够了。(这是分离的形式，定义谓词只有形式的有界量词∀x ∈ A 和 ∃x ∈ A，但没有任何形式∀x和∃x.)但是，有界分离只需要建立一个关于集合宇宙的一般事实，即它形成了一个笛卡尔闭范畴。在那之后，劳维尔定理就开始了，并完成了任务。所以我想说，分离在这里并不是以一种基本的方式使用的（例如，拓扑理论直接将指数公理化，因此在那里根本不需要分离）.

安德烈鲍尔

2008年3月5日00：01

我突然想到，我应该参考劳维尔的不动点定理。可在《范畴的

理论与应用再版》2006年第15期，第5页。1△13’，是可在线获取

EtienneJacques

2008年3月16日00：26

＜a href='http://xxx.lanl.gov/abs/math.LO/0305282"/rel="no跟随'＞

这是劳维尔论文的介绍。＜/a＞

EtienneJacques

2008年3月16日00：27

可通过以下网址在线获取：

http://xxx.lanl.gov/abs/math.LO/0305282