数系的扩充始终贯穿于数学理论的发展之中。本书利用交互式定理证明工具Coq，在Morse-Kelley公理化集合论形式化系统下，给出中国科学技术大学汪芳庭教授在其《数学基础》中采用算术超滤分数构造实数的机器证明系统，包括超滤空间与算术超滤的基本概念、超滤变换以及用算术超滤构造算术模型的形式化实现，完成实数模型的形式化构建，并且给出滤子扩张原则和连续统假设蕴含非主算术超滤存在的形式化验证，在我们开发的系统中，全部定理无例外地给出Coq的机器证明代码，所有形式化过程已被Coq验证，并在计算机上运行通过，充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点，其证明过程规范、严谨、可靠。该系统可方便地推广到非标准分析理论的形式化构建。 本书可作为数学与计算机科学、信息科学相关专业的高年级本科生或研究生教学用书，也可供从事人工智能相关科研工作者学习参考。

“数学机械化丛书”前言
前言
基本符号
第1章 引言
1.1 概述
1.1.1 证明辅助工具Coq
1.1.2 形式化数学
1.1.3 Morse-Kelley公理化集合论系统
1.1.4 关于数系的扩充
1.1.5 本书结构安排
1.2 基本Coq指令清单及逻辑预备知识
第2章 Morse-Kelley公理化集合论的形式化系统实现
2.1 分类公理图式
2.2 分类公理图式（续）
2.3 类的初等代数
2.4 集的存在性
2.5 序偶：关系
2.6 函数
2.7 良序
2.8 序
2.9 非负整数
2.10 选择公理
2.11 基数
第3章 滤子构造超有理数的形式化系统实现
3.1 Peano算术的适当展开
3.1.1 加法和乘法
3.1.2 代数运算性质
3.1.3 偶数和奇数
3.2 滤子与超滤
3.3 超滤变换
3.4 算术超滤及其算术模型
3.4.1 算术超滤
3.4.2 *N上的序
3.4.3 *N上的运算
3.4.4 ω嵌入*N
3.5 *N扩张到*Z
3.5.1 等价关系与分类
3.5.2 *N×*N的一个重要分类
3.5.3 *Z上的序
3.5.4 *Z上的运算
3.5.5 *N嵌入*Z
3.6 *Z扩张到*Q
3.6.1 *Z×（*Z～{*Z0}）的一个重要分类
3.6.2 *Q上的序
3.6.3 *Q上的运算
3.6.4 *N和*Z嵌入*Q
第4章 什么是实数
4.1 *Q中的整数和有理数
4.1.1 非负整数集
4.1.2 整数集
4.1.3 有理数集
4.2 *Q中的无穷
4.2.1 Archimedes子集与无穷大
4.2.2 无穷小
4.3 实数集R
4.3.1 Q<上的一个重要分类
4.3.2 R上的序
4.3.3 R上的运算
4.4 R中的整数和有理数
4.4.1 非负整数集
4.4.2 整数集
4.4.3 有理数集
4.4.4 Archimedes性与稠密性
4.5 数列和完备性
4.5.1 ω上的数列及其延伸
4.5.2 Q上的数列及其延伸
4.5.3 R上的数列
4.5.4 实数完备性
4.6 无理数的存在性
4.6.1 数列和运算的补充性质
4.6.2 一些具体数列
4.6.3 算术平方根和无理数
4.7 实数是什么
第5章 非主算术超滤的存在性
5.1 滤子扩张原则
5.2 一些引理
5.3 连续统假设蕴含非主算术超滤存在
第6章 结论与注记
参考文献
附录一 Coq指令说明
A.1 Coq专用术语
A.2 Coq证明指令
A.3 集成策略
附录二 公理化集合论与实数公理化的结构性呈现
索引