无限基数：比大小，不称重
Infinite CardinalityCantor 研究傅里叶级数时被逼出一门新学问：怎么比较两个无限集合的大小？他的妙招是不给"大小"下定义，只比较——沿用第四章的映射规则：A bij B 叫"一样大"，A surj B 叫"不小于"，A strict B（即 NOT(A surj B)）叫"严格更小"。
有限集的直觉大量失效：无限集加一个元素，还是一样大（引理 8.1.7）——ℕ bij ℕ∪{周一周二…}；ℤ 与 ℕ 一样大（0,1,−1,2,−2,…）；连 ℕ×ℕ、ℚ⁺ 都可数（推论 8.1.10）。"可数（countable）"= 能排成清单 c₀, c₁, c₂, …（有限集也算，可重复列举）。
这条直觉的经典可视化就是"无限旅馆"：
对任意集合 A：A strict pow(A)——幂集永远严格更大。Cantor 的惊人发现在于：无穷与无穷之间也有大小之分，且幂集塔可以无限攀升：ℕ ≺ pow(ℕ) ≺ pow(pow(ℕ)) ≺ ⋯
对角论证剧场
The Diagonal Argumentpow(ℕ) ≈ {0,1}^ω（无限位串全体）。假设有人宣称已把所有无限位串排成了清单 A₀, A₁, A₂, …——对角论证当场上演：取清单的对角线，逐位翻转，得到的串 C 与清单里每一行都至少有一位不同，却也是合法位串。矛盾：清单不全。这招直接证明 pow(ℕ)、{0,1}^ω、ℝ 全都不可数。亲手揪一次：
停机问题：对角论证的 CS 杀伤弹
The Halting Problem把每个程序看成字符串。定义 No-halt ::= { s | 程序 Pₛ 跑在自己身上永不停机 }。定理 8.2.2：No-halt 不可识别——不存在程序能认出所有"自跑不停"的程序。证明就是 Cantor 对角论证的换装：假设分析器 P̂ 识别 No-halt，把清单表换成"程序 × 是否停在自身"的表，P̂ 所在的对角线一翻转，构造出的 s₀ 立刻自相矛盾。
集合的逻辑：Russell 悖论与 ZFC
The Logic of Sets1890 年代，Frege 的集合公理化刚要完工，Russell 用同一个对角思路把它打穿：W ::= { S | S ∉ S }——"所有不包含自身的集合"之集。问：W ∈ W 吗？是 ⇒ 它不该在 W 里；否 ⇒ 它就该在 W 里。数学的根基轰然作响。Russell 与 Whitehead 花了十二年写《数学原理》试图自救，最终由更简洁的 ZFC 公理体系接管（第一章提过的 ZFC 在此正式露面）。
ZFC 共九条公理：外延、配对、并、无穷、概括（Subset，更常叫 Comprehension：从已有集合 x 中按性质 φ 筛出子集——不许凭空搜集）、幂集、替换、基础（Foundation：禁止 ⋯ ∈ xₙ ∈ ⋯ ∈ x₀ 的无限降链，于是没有集合是自己的成员）、选择。Russell 悖论的现代解法（8.3.3）干净利落：Foundation 保证一切 S 都满足 S ∉ S，于是 W 包含每个集合——它若是集合，就是自己的成员，矛盾。所以 W 根本不是集合，悖论消散。
而对角论证的 CS 杀伤弹与 Russell 悖论是同一个论证：W 的定义里那句 "S ∉ S"，就是停机悖论里"程序对自己的判断取反"。下面装置④把这个"同一个论证"做成有限沙盘——Cantor 定理 8.1.12 的证明内核，亲手推一遍：
三朵乌云：① ZFC 是人定的公理，可能有一天被"下一个 Russell"打穿；② 连续统假设（ℕ 与 pow(ℕ) 之间没有别的无穷）在 ZFC 中不可判定——Gödel 与 Cohen 证明两边都能自洽；③ Gödel 不完备性：任何一致的系统都无法证明自身的一致性。数学的"真相"并未完全尘埃落定。
选择公理 ⟹ Banach–Tarski 定理：一个实心球可分成 6 块，刚体重排成两个与原球等大的实心球——ZFC 的推论并不都"符合直觉"。而 8.4.1 给计算机人递了颗定心丸：主流数学与 CS 只玩可数集（常常只是有限集），"太大"的搜集自有逻辑学家操心；但对这些遥远东西的较真，恰恰通向 8.2 节计算的逻辑极限——这才是本章真正要带走的。
习题实战：双射练习与可数清单
8.1/8.3, Playable8.3 的映射关系练习 + 亲手把 ℤ 与 ℕ×ℕ 排成可数清单。
终局自测
Final Check六题，覆盖全章与第一部分收官。
彩蛋与课后挑战
Easter Eggs & ProblemsCantor 的流放与"康托乐园"（原书 8.1 节）
Cantor 本是研究傅里叶级数收敛的，被无穷集"带偏"后遭到当时数学界主流的怀疑与排斥，同侪讥其研究的是"康托乐园里的OutOfInfinity"。他去世后，这门学问成了数学与计算机科学共同的地基——你的每次类型检查失败，都是对角论证在工作。另外：连续统假设在 ZFC 中不可判定（Gödel 1940 / Cohen 1963），Cohen 因此获 1966 年 Fields 奖。
Schröder-Bernstein 定理（原书 8.1.4 定理 8.1.4）
若 A surj B 且 B surj A，则 A bij B——有限集上显然，无限集上是要真证的（把两个单射“缝”成一个双射，习题 8.10）。配角的深度的最好例子：随手一写的"显然"，可能藏着一页纸的机关。
课后挑战（均出自原书习题）
- 8.1 证明有限二进制串集 {0,1}* 可数（按长度分层列举）。
- 8.2 构造两个不可数集合 A、B，使 A、B 之间不存在双射——"不可数"也分大小。
- 8.3 A strict ℕ 等价于下列哪些？"A 可数无限""A 不可数""A 有限"——小心，有陷阱。
- 8.8 证明：A 无限且 B 可数 ⇒ A surj B（可数集是"最小的无穷"）。
- 8.24 证明 ℕ ≺ pow(ℕ) ≺ pow(pow(ℕ)) ≺ ⋯ 的并集比塔里每一层都大——无穷的无穷塔没有顶。
第一部分（Part I · Proofs）就此收官 🎓
八章走完：命题与证明的骨架（1）→ 良序（2）→ 逻辑语言（3）→ 数据类型（4）→ 归纳双璧（2、5）→ 状态机与不变量（6）→ 递归类型（7）→ 无穷与可计算性的边界（8）。接下来原书进入 Part II · Structures（数论、图论、通信网络），后续章节按同样流程续作——说"继续"即可。