书名：机器证明：公理集论及分析基础的形式化
定价：198.0
ISBN：9787030832443
作者：郁文生等
版次：1
出版时间：2025-09

内容提要：
布尔巴基学派的序、代数、拓扑三大母结构是现代数学的基础。利用计算机证明辅助工具，可以完整构建这三大母结构的形式化系统。本书利用交互式定理证明工具Coq，实现Morse-Kelley公理化集合论形式化系统，可以迅速而自然地给出一个数学基础，摆脱了明显的悖论。在我们开发的系统中，全部定理无例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点，其证明过程规范、严谨、可靠。该系统可方便地应用于拓扑学和代数学理论的形式化构建。为方便应用，在Morse-Kelley公理化集合论形式化系统下，分别给出Landau的经典著作《分析基础》的形式化系统以及Zorich的著名著作《数学分析》中实数公理化的形式系统实现，从而迅速且自然地给出数学分析的坚实基础。



目录：
目录
前言
基本符号
第1章 引言 1
1.1 概述 1
1.1.1 证明辅助工具 Coq 1
1.1.2 形式化数学 2
1.1.3 Morse-Kelley公理化集合论系统 3
1.1.4 分析基础 5
1.1.5 本书结构安排 7
1.2 基本Coq指令清单及逻辑预备知识 8
第2章 Morse-Kelley公理化集合论的形式化系统实现 14
2.1 分类公理图式 14
2.2 分类公理图式 (续) 15
2.3 类的初等代数 16
2.4 集的存在性 21
2.5 序偶：关系 25
2.6 函数 29
2.7 良序 36
2.8 序 43
2.9 非负整数 51
2.10 选择公理 54
2.11 基数 57
第3章 分析基础的形式化系统实现 80
3.1 自然数 80
3.1.1 公理 80
3.1.2 加法 85
3.1.3 序 90
3.1.4 乘法 95
3.2 分数 98
3.2.1 定义和等价 98
3.2.2 序 100
3.2.3 加法 104
3.2.4 乘法 109
3.2.5 有理数和整数 113
3.3 分割.133
3.3.1 定义 133
3.3.2 序 136
3.3.3 加法 138
3.3.4 乘法 145
3.3.5 有理分割和整分割 153
3.4 实数 165
3.4.1 定义 165
3.4.2 序 170
3.4.3 加法 176
3.4.4 乘法 196
3.4.5 Dedekind基本定理 212
3.5 复数.217
3.5.1 定义 217
3.5.2 加法 218
3.5.3 乘法 220
3.5.4 减法 222
3.5.5 除法 223
3.5.6 共轭复数 226
3.5.7 绝对值 227
3.5.8 和与积 229
3.5.9 幂 241
3.5.10 将实数编排在复数系统中 243
第4章 实数集的公理系统形式化 247
4.1 实数集的公理系统及其一般性质 247
4.1.1 实数集的定义 247
4.1.2 实数的某些一般的代数性质 250
4.1.3 完备性公理与数集的确界存在性 259
4.2 几个重要的实数子集262
4.2.1 自然数与数学归纳法原理 262
4.2.2 有理数与无理数 267
4.2.3 Archimedes原理 280
4.3 实数的几何解释 286
4.4 实数模型的唯一性 291
第5章 结论与注记.321
附录一 Coq指令说明 327
A.1 Coq专用术语327
A.2 Coq证明指令328
A.3 集成策略 331
附录二 公理集论与实数公理化的结构性呈现 343
参考文献 376
索引 387
后记 393
表格目录
表1.1 书中涉及的常用 Coq 指令简表9
表1.2 书中涉及的常用 Coq 术语的基本含义 12
表5.1 公理化集合论形式化系统代码量统计 321
表5.2 分析基础形式化系统代码量统计 322
表5.3 实数公理化形式系统代码量统计 322
插图目录
图1.1 Kelley的《一般拓扑学》英文版和中文版封面 4
图1.2 Landau的《分析基础》德文、英文版和中文版封面 5
图1.3 Zorich的《数学分析》俄文版、英文版、中文版封面 7
图5.1 实数模型同构唯一性的证明截图323
图5.2 计算机软件著作权登记证书 323
图5.3 Lean 验证数学定理输出的命题和概念网络 325