人工智能研究是国家当前重大科技发展战略之一，夯实人工智能基础理论尤为重要，数学定理机器证明是人工智能基础理论的深刻体现.

选择公理是集合论里有关映射存在性的一条公理，最早于1904年由Zermelo提出，并用于对良序原则的证明^[1-2].选择公理在现代数学中有很重要的作用，与许多深刻的数学结论有着十分密切的联系.没有选择公理，甚至无法确定2个集合能否比较元素的多少、非空集的积是否非空、线性空间是否一定有一组基、环是否一定有极大理想等.选择公理有多个等价定理，Tukey引理是其常见和重要的一种.通过Tukey引理容易证明Hausdorff极大原则、极大元则、Zermelo假定、Zorn引理、良序定理等与选择公理等价的著名定理.拓扑学中重要的Tychonoff乘积定理同样依赖于Tukey引理，这是选择公理较为深刻的一个应用.

近年来数学定理形式化证明的研究，随着计算机科学的迅猛发展，特别是交互式定理证明辅助工具Coq^[3]、Isabelle、HOL Light等的出现，取得了长足的进展.国际计算机专家Gonthier^[4]成功基于Coq给出了著名的“四色定理”的计算机证明，进而，Gonthier等又经过6年努力，于2012年完成对有限单群分类定理的机器验证(该证明过程约有4 200个定义和1.5万条定理，约17万行的Coq代码)^[5]，使得证明辅助工具Coq在学术界的影响日益增强. Wiedijk指出全球各相关研究团队已经或计划完成包括Gödel不完全性定理、Jordan曲线定理、素数定理以及Fermat大定理等在内的100个著名数学定理的计算机形式化证明，目前已经完成其中93个定理的形式化证明^[6].

笔者在“公理化集合论”形式化系统基础上，通过调用该系统中的一些基本公理、定义和定理，给出选择公理与Tukey引理等价性的机器证明.创新研究在于利用交互式定理证明工具Coq，给出纯计算机形式化证明，体现了基于Coq的数学定理机器证明所具有的可读性、交互性和智能性等特点，机器证明的过程规范、严谨、可靠.

1 “公理化集合论”形式化系统

19世纪末和20世纪初，朴素集论中一些悖论的发现，使集合论之公理化研究成为必要.公理化集合论的出发点就是给出一组集合应该满足的公理，在此基础上研究集合的性质.集合论里普遍采用的公理体系是ZFC体系，它由策梅洛-弗兰克尔(ZF, Zermelo-Fraenkel)集合论公理化体系加上选择公理(AC, axiom of choice)构成.其他著名的公理化集合理论有冯·诺伊曼-博内斯-哥德尔(NBG, von Neumann-Bernays-Gödel)集合论和摩斯-凯利(MK, Morse-Kelley)集合论^[2].

“公理化集合论”形式化系统是基于MK集合论公理化体系搭建的. MK集合论公理化体系最早在1949年由王浩提出^[7]，1955年在Kelley的《一般拓扑学》中正式发表^[8]，此后在1965年由Morse完善.该公理系统构造了序数和基数，定义了非负整数，并把Peano公设当做定理给予了证明，在此基础上实数也可以由“整数类是一个集”和“利用归纳法在整数上定义一个函数是可能的”这两点事实以及Peano公设和无限性公理来构造.该公理化系统可用来迅速而又自然地给出一个数学基础，摆脱了集合论中较明显的悖论.由此，有限的公理体系被遗弃，而把整个理论建筑在8个公理和1个公理图示之上.该公理体系相当于承认存在比集合更广之类，与ZF公理化系统无矛盾.

“公理化集合论”形式化系统已经完成对MK集合论公理化体系的Coq形式化，包括8个公理和1个公理图示的形式化描述以及全部181条定义或定理的形式化描述或证明.完整的代码可见文献[9]. Tukey引理是“公理化集合论”形式化系统的一个重要应用.在该系统的基础上，现代数学主体的拓扑学和近世代数等理论可以快速地形式化构建.

下面介绍一些“公理化集合论”系统中的基本概念.首先，定义一个在系统中描述集合和元素的概念“类”.在Coq形式化中选择一般类型“Type”表示，其形式化定义如下：

Parameter Class: Type.

本系统除了“=”和基本逻辑概念之外，定义2个基本的常项.第1个是“∈”，它读作“属于”.因为在本系统中不区分集合与元素的类型，统一用Class来表示.因此“∈”的形式化定义如下：

Parameter In: Class → Class → Prop.

第2个常项是分类“{…:…}”，读作“{所有…的集使得…}”，其形式化定义如下：

Parameter Classifier:(Class→Prop)→Class.

通过“Notation”命令可以在Coq中添加数学符号，增强代码可读性.

Notation"\{ P \}" := (Classifier P) (at level 0).

在集合描述性定义基础上，引入分类公理图示，可避免明显的悖论，Coq形式化如下：

集x为一集当且仅当对于某一y，x属于y.

Definition Ensemble x:=exists y, In x y.

公理1(分类公理图式)  对于每一个β，β∈{α:P(α)}的充分必要条件是“β是集”和P(β)，这里P(·)是适定的公式.

Axiom AxiomS:forall b (P: Class → Prop),

In b\{P\} ↔ Ensemble b /\ (P b).

“公理化集合论”系统中共有8条公理，下面以外延公理为例展示如何在该系统中形式化描述公理.

公理2(外延公理)  对于每个x与y，x=y成立之充要条件就是对每一个z当且仅当z∈x时，z∈y.

Axiom Axiom_Extent : forall x y,

$ x = y \leftrightarrow ({\rm{forall}}\;z, {\rm{ In}}\;z\;x \leftrightarrow {\rm{In}}\;z\;y) $

表 1列出了该系统中一些重要概念的Coq定义、数学定义和数学符号.

为了形式化的完整性和独立性，笔者使用的集合论是“公理化集合论”系统的简化和修改版，其包含了系统中的8条公理、40个定义和50个定理.

2 基本定义

首先给出选择函数的定义，在其基础上可以完成选择公理的形式化.

定义1(选择函数)  设${\tilde X}$是一个集合，记X为由X的所有非空子集构成的集族.称函数f:${\tilde X}$→X (f的定义域为${\tilde X}$，f的值域为X的子集)为X的一个选择函数，如果它满足条件：对于任意A∈${\tilde X}$，有f(A)∈A.

Definition Choice_Function X f: Prop:=

  Function f /\ dom(f) = pow(X)~[Empty]

  /\Subclass ran(f) X /\(forall A, In A dom(f)

  → In f[A] A).

下面给出极大成员、套、有限特征集的定义，这些定义将在Tukey引理的描述和证明中使用.

定义2(极大成员)  设$\mathscr{F}$是一个集族，F是$\mathscr{F}$的一个成员.如果$\mathscr{F}$中没有任何成员以F为真子集，则称F为$\mathscr{F}$的一个极大成员.

Definition MaxMember F f : Prop :=

  f < > Empty → In F f /\ (forall E: Class,

  In E f → ~ (PSubclass F E)).

定义3(套)  设$\mathscr{F}$是一个集族，如果对于任意A，B∈$\mathscr{F}$有A⊂B或者B⊂A，则称$\mathscr{F}$为一个套.

Definition Nest f: Prop :=

  forall A B: Class, In A f /\ In B f →

  Subclass A B \/ Subclass B A.

定义4(有限特征集)  设$\mathscr{F}$是一个集族.如果F是$\mathscr{F}$的一个成员当且仅当F的每一个有限子集都是$\mathscr{F}$的成员，则称$\mathscr{F}$是一个具有有限特征的集族.

Definition FiniteSet f : Prop :=

  Ensemble f /\ (forall F, In F f →

  (forall z, Subclass z F /\ Finite z →

  In z f)) /\ (forall F, Ensemble F /\

  (forall z, Subclass z F /\ Finite z →

  In z f) → In F f).

3 Tukey引理形式化证明 3.1 选择公理及相关公式

选择公理可以通过选择函数定义，其具体概念及形式化描述如下.

选择公理  任何一个集合都有一个选择函数.

Axiom Choice_Axiom : forall (X: Class),

  Ensemble X →exists ε: Class,

  Choice_Function ε X.

Tukey引理是与选择公理相关的重要定理. Tukey引理的描述和形式化表达如下.

Tukey引理  非空的具有有限特征的集族中必有极大成员.

Theorem Tukey : forall (f: Class),

  FiniteSet f /\ f <> Empty → exists x,

  MaxMember x f.

假设$\mathscr{F}$为一个非空的具有有限特征的集族，因此X=∪$\mathscr{F}$是一个集合.根据选择公理，X有选择函数ε:${\tilde X}$→X使得对于任意A∈${\tilde X}$，ε(A)∈A.其中${\tilde X}$为X的所有非空子集构成的集族.对每一个F∈$\mathscr{F}$，构造一个更大的集合${\hat F}$为

$ \hat F = \{ x:x \in X \wedge F \cup \{ x\} \in \mathscr{F}\} $

(1)

对集合${\hat F}$的形式化定义记作Ex_F，以该公式为例，本文中的公式都已在Coq中形式化定义，具体如下：

Definition Ex_F (F f: Class) : Class :=

  \{fun x => In x (\cup f) /\ In (Union

  F[x]) f \}.

这里简单介绍一下之前定义的Classifier的使用方法. Classifier的输入项为Class→Prop类型.第1个参数Class代表分类中的变量，第2个参数Prop表示该变量满足的公式. λ演算的性质刚好能满足上述要求，在Coq中使用fun函数来实现.

根据集合${\hat F}$的定义可知，F⊂${\hat F}$或者F=${\hat F}$.因此根据${\hat F}$定义一个函数χ:$\mathscr{F}$→$\mathscr{F}$，该函数的具体描述为

$ \chi (F) = \left\{ {\begin{array}{*{20}{l}} {F \cup \{ \varepsilon (\hat F - F)\} , }&{\hat F - F \ne \emptyset }\\ {F, }&{\hat F - F = \emptyset } \end{array}} \right. $

(2)

对此函数的Coq形式化分为3部分完成：

1) 首先定义一个判定函数eq_dec，该函数对任意类型为Type的变量都满足.定义中会使用Coq库中的sumbool函数，

Inductive sumbool (P1 P2: Prop) : Set :=

  |left: P1 → {P1} + {P2}

  |right: P2 → {P1} + {P2}

通过构造子left和right可以直接得到P1和P2.函数eq_dec的形式化定义如下：

Definition eq_dec (A: Type): Prop :=

  forall x y: A, {x = y} + {x 〈〉 y}.

2) 将特定类型Class作为函数eq_dec中变元的类型，从而得到新的函数beq：

Parameter beq:eq_dec Class.

3) 在函数beq的基础上定义函数Fun_X.在Coq中通过模式匹配定义，具体实现如下：

Definition Fun_X F f ε: Class :=

  match beq ((En_F′ F f) ~ F) Empty with

  | left _ => F

  | right _ => Union F [ε[(En_F′ F f)~F]]

  end.

通过该函数的定义，将Tukey引理的证明目标转化为是否存在一个$\mathscr{F}$中的元F，使得χ(F)=F.下面在函数χ的基础上定义t-子集.

定义5(t-子集)  f是$\mathscr{F}$的t-子集，当且仅当f是$\mathscr{F}$的子集并且满足条件：

1) Ø∈f;

2) 若F∈f，则χ(F)∈f;

3) 若φ为f中的套，则∪φ∈f.

在Coq中对t-子集的形式化定义如下：

Definition tSubclass g f ε : Prop:=

  Subclass g f /\ In Empty g /\ (forall F,

  In F g →In (Fun_X F f ε) g)/\(forall L,

  Subclass L g /\ Nest L → In (\cup L) g).

下面通过上述t-子集的定义构造一些特殊集合，令f₀为$\mathscr{F}$中所有t-子集的交，

$ {f_0} = \cap \{ f:{\rm{ tSubclass }}f\;\mathscr{F}\;\varepsilon \} $

(3)

若证明了f₀是一个套，即可证明Tukey引理.对于每一个C∈f₀，都可以构建一个套，并且使得C为该套中的元素：

$ u(C) = \left\{ {A:A \in {f_0} \wedge (A \subset C \vee C \subset A)} \right\} $

(4)

通过式(3)和式(4)可以构建f₀中的套f₁：

$ {f_1} = \left\{ {C:C \in {f_0} \wedge \left( {u(C) = {f_0}} \right)} \right\} $

(5)

为了验证f₁满足t-子集定义中的条件(2)，对于每一个D∈f₁，如下构造集合v(D).只要证明v(D)是一个t-子集，即可完成全部证明.

$ v(D) = \left\{ {A:A \in {f_0} \wedge (A \subset D \vee \chi (D) \subset A)} \right\} $

(6)

上述公式的Coq形式化如下：

Definition En_f0 (f ε : Class) : Class :=

  \cap \{ fun g => tSubclass g f ε \}.

Definition En_u C (f ε : Class) : Class :=

  \{ fun A => In A (En_f0 f ε) /\

  (Subclass A C \/ Subclass C A) \}.

Definition En_f1 (f ε : Class) : Class :=

  \{ fun C => In C (En_f0 f ε) /\

  (En_u C f ε) = (En_f0 f ε) \}.

Definition En_v D (f ε : Class) : Class :=

  \{ fun A => In A (En_f′0 f ε) /\

  (Subclass A D\/Subclass(Fun_X D f ε)A)\}.

另外，容易证明关于f₀和函数χ的2个性质，二者均已在证明工具Coq中完成形式化验证，它们将在后面的定理证明中反复使用.性质的具体描述和Coq形式化定义如下.

性质1  有限特征集合$\mathscr{F}$中的任意元素F都包含于χ(F).

Lemma Property_x : forall (ε F f: Class),

  Choice_Function ε (\cup f)→ In F f→

  Subclass F (Fun_X F f ε).

性质2  f₀是$\mathscr{F}$最小的一个t-子集，亦即若f为一个t-子集，则f₀⊂f.

Lemma Property_f0 : forall (f ε : Class),

  FiniteSet f /\ f < > Empty →

  Choice_Function ε (\cup f) →

  tSubclass (En_f0 f c) f c /\ (forall g,

  Subclass g f /\ tSubclass g f ε →

  Subclass (En_f0 f ε) g).

下面将分5步完成Tukey引理的证明.前3步证明了f₀是一个套.第4步证明了当F=∪f₀时，χ(F)=F.最后，根据前4步证明的引理在第5步中证明Tukey引理.

3.2 预备引理证明

首先介绍证明中前四步证明的引理.第1步通过之前的定义和性质证明引理1.

引理1  如果D是集合f₁中的一个元素，则v(D)是非空有限特征集$\mathscr{F}$的一个t-子集.

在形式化过程中，当调用t-子集的形式化定义时，必须声明参数ε.因此在引理的条件中加入ε是∪$\mathscr{F}$的选择函数.具体描述如下：

  Lemma LemmaT1 : forall (f ε : Class),

  FiniteSet f /\ f < > Empty →

  Choice_Function ε (\cup f) → (forall D,

  In D (En_f1 f ε) → tSubclass (En_v D f

  ε) f ε).

证明  首先根据式(6)中v(D)的定义以及性质2可以得到v(D)⊂$\mathscr{F}$.因此对于任意A∈v(D)有A∈$\mathscr{F}$.此结论将在后面的证明中反复使用.通过性质2可以证明f₀是$\mathscr{F}$的一个t-子集.下面逐步验证v(D)满足t-子集的3个条件.

1) 显然，根据式(6)可知Ø∈v(D).

2) 第2步验证：若A∈v(D)，则χ(A)∈v(D).分为3种情形讨论：

① A⊂D, A≠D证明这是必有χ(A)⊂D.这里采用反证法证明，首先假设χ(A)⊂D是错的.由于D∈f₁，那么可以证明D是χ(A)的真子集.因此χ(A)比A多两点，矛盾.于是χ(A)⊂χ(D)，从而可以证明χ(A)∈v(D).

② A=D.此时可以证明χ(A)=χ(D).因为χ(D)∈v(D)是显然的，所以χ(A)∈v(D).

③ χ(D)⊂A.由于在性质1的基础上可证明A⊂χ(A)，所以χ(D)⊂χ(A)，从而χ(A)∈v(D).

3) 若φ是v(D)中的一个套.由式(6)中v(D)的定义可知要讨论2种情况.首先，如果φ的每一个成员都包含于D，则∪φ⊂D；如果φ中有一个成员包含χ(D)，则χ(D)⊂∪φ.又因为f₀是t-子集，∪φ∈f₀.于是按v(D)的定义，有∪φ∈v(D).至此引理1证明完毕.

引理1证明了v(D)是$\mathscr{F}$的一个t-子集.第2步将通过引理1证明f₁满足t-子集定义中的条件2).具体描述如下.

引理2如果D是集合f₁中的一个元，则χ(D)同样是f₁中的一个元.

Lemma LemmaT2 : forall (f ε : Class),

  FiniteSet f /\ f < > Empty →

  Choice_Function ε (\cup f) → (forall D,

  In D (En_f1 f ε)→ In (Fun_X D f ε)

  (En_f1 f ε)).

证明  根据式(4)和式(6)，显然可以得到v(D)⊂u(χ(D)).由引理1可知v(D)是$\mathscr{F}$的一个t-子集，又根据性质2可知f₀是最小的t-子集.因此对于每一个D∈f₁，u(χ(D))=f₀，即χ(D)∈f₁.这也就是说f₁满足t-子集条件2).

接下来第3步通过引理2证明f₀是一个套，即引理3.该引理的具体描述和Coq形式化描述如下.

引理3  如果$\mathscr{F}$为一个非空的具有有限特征的集族，ε是∪$\mathscr{F}$的选择函数，则f₀是一个套.

Lemma LemmaT3 : forall (f ε : Class),

  FiniteSet f /\ f < > Empty →

  Choice_Function ε (\cup f) →

  Nest (En_f0 f ε).

证明  根据式(5)中f₁的定义，显然f₁是f₀中的一个套.由于f₀是最小的t-子集，假如证明了f₁是一个t-子集，那么便有f₀=f₁.于是f₀便是一个套，也就完成了引理3的证明.下面根据定义5证明f₁是一个t-子集.空类属于f₁是显然的.又引理2证明了f₁满足条件2)，下面验证f₁满足条件3)：设φ为f₁中的一个套，任意A∈f₀，如果所有φ中成员都包含于A，则∪φ⊂A；如果φ中有一个成员包含A，则A∪⊂φ.因此可以证明u(∪φ)=f₀，这也就是∪φ∈f₁.综上，当$\mathscr{F}$为一个非空有限特征集族且ε是∪$\mathscr{F}$的选择函数时，f₀是一个套.

在证明了f₀是一个套之后，第4步证明存在某一元F∈$\mathscr{F}$使得χ(F)=F，具体引理描述及Coq形式化描述如下所示：

引理4  ∪f₀是$\mathscr{F}$中的一个元并且χ(∪f₀)=∪f₀.

Lemma LemmaT4: forall (f ε : Class),

  FiniteSet f /\ f < > Empty →

  Choice_Function ε (\cup f) →

  In (\cup (En_f0 f ε)) f /\

  (Fun_x (\cup (En_f0 f ε)) f ε) =

  \cup (En_f0 f ε).

证明  令F=∪f₀，根据之前证明的性质1可得F⊂χ(F).由性质2可知f₀是一个t-子集，显然f₀⊂f₀.又根据引理3，f₀是一个套.因此F是$\mathscr{F}$中的一个元.下面证明χ(F)=F，根据t-子集定义中的条件2)和3)可得F∈f₀和F∈χ(F).于是χ(F)⊂F，从而χ(F)=F，引理得证.

3.3 Tukey引理证明

最后证明的第5步通过引理4证明Tukey引理，也就是证明非空的具有有限特征的集族必有极大成员.具体证明过程如下.

证明  根据之前的假设定义，$\mathscr{F}$为一个非空的具有有限特征的集族.根据选择公理，X=∪$\mathscr{F}$有选择函数ε:${\tilde X}$→X使得对于任意A∈${\tilde X}$，ε(A)∈A.由引理4可证明存在一个元F=∪f₀使得χ(F)=${\hat F}$.因此根据式(2)中函数的定义，可证明F=${\hat F}$，从而F是集合$\mathscr{F}$的极大值，定理得证.至此，Tukey引理全部证明完毕.

4 选择公理形式化证明

第3节中将选择公理看作一条公理证明了Tukey引理.本节将选择公理作为一条定理，并通过Tukey引理证明，从而证明了选择公理与Tukey引理间的等价性.具体定理的形式化描述如下：

Theorem Tukey_Choice : forall X,

Ensemble X→exists ε, Choice_Function ε X.

在证明之前，首先构造一个特殊的集合$\mathscr{F}$.假设类μ为非空集合所成的集族，令m=∪μ，定义一个函数f:μ→m，使得对任意(E, e)∈f⊂μ×m，都有e∈E.该函数的形式化定义如下：

Definition Function_C f X : Prop :=

  Ensemble X /\ Function f /\ dom(f)=X /\

  ran(f)⊂(\cup X) /\ (forall E: Class,

  In E dom(f) → In f[E] E).

设X为非空集合，${\tilde X}$=2^X~{Ø}，令

$ {\mathscr{F}} = \left\{ {f:f是\tilde X的子集上的选择函数} \right\} $

(7)

对集合$\mathscr{F}$的形式化定义如下：

Definition En_f X : Class:=

  \{ λ f, exists A, Subclass A (pow(X)~[Ø])

  /\ Function_C f A \}.

证明  首先证明$\mathscr{F}$是非空的具有有限特征的集族.因为Ø∈$\mathscr{F}$，所以$\mathscr{F}$非空.根据有限特征集的定义，证明分为2个方面：

1) 若f∈$\mathscr{F}$且g⊂f，则易证明g∈$\mathscr{F}$；

2) 若集f的每一个有限子集都为$\mathscr{F}$的成员，则有

a) f⊂∪$\mathscr{F}$⊂${\tilde X}$×X；

b) 对每一个(E, e)∈f，e∈E；

c) 若(E, e), (E, e′)∈f，则f₀={(E, e), (E, e′)}∈$\mathscr{F}$，从而由函数的定义可得e′=e.

综上，$\mathscr{F}$是一个非空的具有有限特征的集族，对其应用Tukey引理可得$\mathscr{F}$有极大元.设f₁是$\mathscr{F}$的一个极大元，设f₁的定义域为D.若D⊊X，则有${\tilde X}$~D≠Ø.因此设E₂∈${\tilde X}$~D，取e₂∈E₂.令集合f₂=f({(E₂, e₂)})，则可以证明f₂∈$\mathscr{F}$并且f₁是f₂的真子集，这与f₁是$\mathscr{F}$极大元矛盾.故f₁的定义域D=${\tilde X}$，即对于集合X，f₁是X的选择函数，定理得证.

5 其他集合论形式化工作

公理化集合论的形式化工作方面，Werner的工作研究了公理化集合论与类型论间的关系，提出了一种ZFC集合论与Coq归纳构造演算(CIC)理论一致性的证明^[10].基于Werner的工作，Barras在Coq上形式化了CIC的元理论^[11]. Simpson完成了ZFC集合论中大部分概念的形式化，Kirst和Smolka通过Coq形式化了二阶ZF集合理论^[12].

选择公理的形式化工作方面，Schepler通过选择公理证明了Zorn引理和良序定理，但其是在Coq标准库中的朴素集合论的基础上实现的.此外，Paulson基于Isabelle证明了选择公理的相容性^[13].

笔者^[14]完成了选择公理与Hausdorff极大原则、Zermelo假定等定理的形式化证明，其中使用了Tukey引理未给出完整证明.应该指出，选择公理与Tukey引理等价性的传统数学证明散见于众多数学文献[1, 2, 15].

6 形式化证明总览

选择公理是公理化集合论中的一个重要公理，其在现代数学中有着重要应用.笔者在“公理化集合论”形式化系统的基础上，完成了选择公理与Tukey引理的形式化，并对二者间的等价性进行了完整的形式化证明.文中的所有证明都已在证明辅助工具Coq中验证.完整的Coq证明代码可见参考文献[16].

整个形式化工作大约3 800行代码，其中包括30个定义、20个引理和10个定理.全部代码都已在Coq 8.8.0中测试编译通过.表格2展示了具体每个脚本文件的形式化工作量，为了方便理解还标注了文件的对应章节.

7 结束语

选择公理和Tukey引理的形式化在数学领域中具有深远的意义，未来可以进一步研究选择公理与更多定理的等价性证明.在Tukey引理的基础上可以证明拓扑学中重要的Tychonoff定理.此外，在本文“公理化集合论”形式化系统基础上，可以快速构建近世代数理论和拓扑学理论.这对开发布尔巴基学派提出的现代数学三大母结构—序结构、代数结构、拓扑结构—的形式化具有重大意义.