编辑“︁Lean序数与基数”︁

{{DISPLAYTITLE:Lean序数与基数}}  
[[Category:Lean数学基础]]  

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

== 基本定义 ==  

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

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

== Lean中的实现 ==  

=== 序数的定义与操作 ===  
Lean的`Mathlib`库中，序数通过归纳类型和公理化定义实现。以下是一个简化示例：  
<syntaxhighlight lang="lean">  
import Mathlib.SetTheory.Ordinal.Basic  

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

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

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

=== 基数的定义与操作 ===  
基数通过序数的等势性定义，以下是Lean中的示例：  
<syntaxhighlight lang="lean">  
import Mathlib.SetTheory.Cardinal.Basic  

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

'''输出与解释'''：  
* `aleph0`表示可数无限的基数（如自然数集的势）。  
* `2 ^ aleph0`表示实数集的基数（连续统假设的对象）。  

== 实际案例 ==  

=== 案例1：序数算术 ===  
在游戏理论中，序数用于描述无限回合的顺序。例如，`ω + 1`表示无限回合后追加一个回合：  
<mermaid>  
graph LR  
    A[回合0] --> B[回合1] --> C[回合2] --> D[...] --> E[回合ω] --> F[回合ω+1]  
</mermaid>  

=== 案例2：基数比较 ===  
验证两个集合的等势性：  
<syntaxhighlight lang="lean">  
import Mathlib.Data.Real.Basic  

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

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

== 进阶主题 ==  

=== 序数递归 ===  
序数支持超限递归（transfinite recursion），用于定义无限结构：  
<syntaxhighlight lang="lean">  
def factorial : Ordinal → Ordinal  
  | 0 => 1  
  | succ n => (factorial n) * succ n  
  | limit a => sSup (factorial '' a)  
</syntaxhighlight>  

=== 连续统假设 ===  
在Lean中，连续统假设（CH）可以形式化为：  
<math>2^{\aleph_0} = \aleph_1</math>  
但需注意其独立于ZFC公理系统。  

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

{{提示|进一步学习可探索`Mathlib`中的`SetTheory.Ordinal`和`SetTheory.Cardinal`模块。}}

[[Category:计算机科学]]
[[Category:Lean]]