书名：自然数的紧化延伸机器证明系统
定价：288.0
ISBN：9787030775450
作者：郁文生,窦国威
版次：1
出版时间：2024-05

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



目录：
目录
“数学机械化丛书”前言
前言
基本符号
第1章 引言1
1.1 概述1
1.1.1 证明辅助工具Coq1
1.1.2 形式化数学2
1.1.3 Morse-Kelley公理化集合论系统3
1.1.4 关于数系的扩充5
1.1.5 本书结构安排8
1.2 基本Coq指令清单及逻辑预备知识9
第2章 Morse-Kelley公理化集合论的形式化系统实现15
2.1 分类公理图式15
2.2 分类公理图式(续).16
2.3 类的初等代数17
2.4 集的存在性23
2.5 序偶:关系27
2.6 函数33
2.7 良序39
2.8 序47
2.9 非负整数56
2.10 选择公理60
2.11 基数63
第3章 滤子构造超有理数的形式化系统实现88
3.1 Peano算术的适当展开88
3.1.1 加法和乘法89
3.1.2 代数运算性质95
3.1.3 偶数和奇数103
3.2 滤子与超滤109
3.3 超滤变换125
3.4 算术超滤及其算术模型134
3.4.1 算术超滤134
3.4.2 *N上的序138
3.4.3 *N上的运算143
3.4.4 ω嵌入*N165
3.5 *N扩张到*Z177
3.5.1 等价关系与分类177
3.5.2 *N×*N的一个重要分类179
3.5.3 *Z上的序184
3.5.4 *Z上的运算188
3.5.5 *N嵌入*Z208
3.6 *Z扩张到*Q221
3.6.1 *Z×(*Z～{*Z0})的一个重要分类221
3.6.2 *Q上的序226
3.6.3 *Q上的运算230
3.6.4 *N和*Z嵌入*Q255
第4章 什么是实数266
4.1 *Q中的整数和有理数266
4.1.1 非负整数集266
4.1.2 整数集274
4.1.3 有理数集283
4.2 *Q中的无穷289
4.2.1 Archimedes子集与无穷大289
4.2.2 无穷小309
4.3 实数集R317
4.3.1 Q <上的一个重要分类317
4.3.2 R上的序321
4.3.3 R上的运算325
4.4 R中的整数和有理数348
4.4.1 非负整数集348
4.4.2 整数集355
4.4.3 有理数集368
4.4.4 Archimedes性与稠密性379
4.5 数列和完备性383
4.5.1 ω上的数列及其延伸383
4.5.2 Q上的数列及其延伸388
4.5.3 R上的数列402
4.5.4 实数完备性411
4.6 无理数的存在性418
4.6.1 数列和运算的补充性质418
4.6.2 一些具体数列433
4.6.3 算术平方根和无理数446
4.7 实数是什么457
第5章 非主算术超滤的存在性461
5.1 滤子扩张原则461
5.2 一些引理467
5.3 连续统假设蕴含非主算术超滤存在497
第6章 结论与注记509
参考文献516
附录一 Coq指令说明525
A.1 Coq专用术语525
A.2 Coq证明指令526
A.3 集成策略529
附录二 公理化集合论与实数公理化的结构性呈现532
索引569
表目录
表1.1 书中涉及常用Coq指令简表10
表1.2 书中涉及常用Coq术语的基本含义13
表4.1 数系扩充符号汇集457
表6.1 公理化集合论形式化系统代码量统计509
表6.2 滤子构造超有理数形式化系统代码量统计510
表6.3 实数形式化系统代码量统计510
表6.4 非主算术超滤存在性形式化系统代码量统计510
图目录
图1.1 Kelley《一般拓扑学》的英文版和中文版封面4
图1.2 Landau《分析基础》的德文-英文版和中文版封面6
图1.3 汪芳庭《数学基础》的两个版本封面8
图3.1 滤子各概念之间的关系示意图138
图3.2 *Z=(*N×*N)/R示意图184
图3.3 *Q=(*Z×(*Z～{*Z0}))/R示意图226
图4.1 从ω扩充至*Q过程示意图458
图4.2 *Q结构与R结构之间的关系图459
图6.1 实数完备性的证明截图511
图6.2 计算机软件著作权登记证书512
图6.3 Lean验证数学定理输出的命题和概念网络513
图6.4 Lean验证多项式Freiman-Ruzsa猜想输出的Blueprint图514