Lean序数与基数

引言

在数学基础与形式化验证中，序数（Ordinals）和基数（Cardinals）是描述集合顺序与大小的核心概念。Lean定理证明器通过类型论和集合论公理（如ZFC）的形式化，提供了对这些概念的严格定义与操作支持。本章将逐步介绍序数与基数在Lean中的表示、性质及实际应用。

基本定义

序数（Ordinals）

序数是良序集合的同构类，用于表示顺序（如自然数的顺序）。在Lean中，序数定义为满足传递性（transitivity）和良序性（well-ordering）的集合： $\text{Ordinal}=\{\alpha \mid \alpha \text{ is transitive and well-ordered by }\in \}$

基数（Cardinals）

基数是集合等势类的代表，用于衡量集合的大小（如自然数的基数ℵ₀）。在Lean中，基数是序数中不与任何前驱等势的最小序数： $\text{Cardinal}=\{\kappa \in \text{Ordinal}\mid \mathrm{\forall }\alpha <\kappa ,|\alpha |<|\kappa |\}$

Lean中的实现

序数的定义与操作

Lean的`Mathlib`库中，序数通过归纳类型和公理化定义实现。以下是一个简化示例：

  
import Mathlib.SetTheory.Ordinal.Basic  

-- 定义序数的基本操作  
def ω : Ordinal := mk ℕ -- 自然数集的序数  

#check ω + 1 -- 后继序数  
#check ω * 2 -- 序数乘法（非交换）

输出与解释：

• `ω`表示最小的无限序数（自然数集）。
• `ω + 1`是ω的后继，表示ω之后的下一个序数。
• `ω * 2`表示两个ω的串联（顺序为0,1,2,...,0,1,2,...）。

基数的定义与操作

基数通过序数的等势性定义，以下是Lean中的示例：

  
import Mathlib.SetTheory.Cardinal.Basic  

#check Cardinal.aleph0 -- ℵ₀，可数无限的基数  
#check 2 ^ Cardinal.aleph0 -- 连续统的基数（实数集的势）

输出与解释：

• `aleph0`表示可数无限的基数（如自然数集的势）。
• `2 ^ aleph0`表示实数集的基数（连续统假设的对象）。

实际案例

案例1：序数算术

在游戏理论中，序数用于描述无限回合的顺序。例如，`ω + 1`表示无限回合后追加一个回合：

graph LR A[回合0] --> B[回合1] --> C[回合2] --> D[...] --> E[回合ω] --> F[回合ω+1]

案例2：基数比较

验证两个集合的等势性：

  
import Mathlib.Data.Real.Basic  

-- 证明整数集与自然数集等势  
theorem Z_equiv_N : Cardinal.mk ℤ = Cardinal.mk ℕ := by  
  apply Cardinal.eq.2  
  exact ⟨⟨Int.toNat, Int.toNat_injective⟩⟩

解释：通过构造双射函数（如整数到自然数的映射），证明两者基数相同。

进阶主题

序数递归

序数支持超限递归（transfinite recursion），用于定义无限结构：

  
def factorial : Ordinal → Ordinal  
  | 0 => 1  
  | succ n => (factorial n) * succ n  
  | limit a => sSup (factorial '' a)

连续统假设

在Lean中，连续统假设（CH）可以形式化为： $2^{{\mathrm{\aleph }}_0}={\mathrm{\aleph }}_1$ 但需注意其独立于ZFC公理系统。

总结

• 序数描述顺序，基数描述大小。
• Lean通过类型论和`Mathlib`提供严格的形式化支持。
• 实际应用包括无限集合的比较、超限归纳等。