目錄
前言
基本符號
第1章 引言 1
1.1 概述 1
1.1.1 證明輔助工具 Coq 1
1.1.2 形式化數(shù)學 2
1.1.3 Morse-Kelley公理化集合論系統(tǒng) 3
1.1.4 分析基礎 5
1.1.5 本書結構安排 7
1.2 基本Coq指令清單及邏輯預備知識 8
第2章 Morse-Kelley公理化集合論的形式化系統(tǒng)實現(xiàn) 14
2.1 分類公理圖式 14
2.2 分類公理圖式 (續(xù)) 15
2.3 類的初等代數(shù) 16
2.4 集的存在性 21
2.5 序偶：關系 25
2.6 函數(shù) 29
2.7 良序 36
2.8 序 43
2.9 非負整數(shù) 51
2.10 選擇公理 54
2.11 基數(shù) 57
第3章 分析基礎的形式化系統(tǒng)實現(xiàn) 80
3.1 自然數(shù) 80
3.1.1 公理 80
3.1.2 加法 85
3.1.3 序 90
3.1.4 乘法 95
3.2 分數(shù) 98
3.2.1 定義和等價 98
3.2.2 序 100
3.2.3 加法 104
3.2.4 乘法 109
3.2.5 有理數(shù)和整數(shù) 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 實數(shù) 165
3.4.1 定義 165
3.4.2 序 170
3.4.3 加法 176
3.4.4 乘法 196
3.4.5 Dedekind基本定理 212
3.5 復數(shù).217
3.5.1 定義 217
3.5.2 加法 218
3.5.3 乘法 220
3.5.4 減法 222
3.5.5 除法 223
3.5.6 共軛復數(shù) 226
3.5.7 絕對值 227
3.5.8 和與積 229
3.5.9 冪 241
3.5.10 將實數(shù)編排在復數(shù)系統(tǒng)中 243
第4章 實數(shù)集的公理系統(tǒng)形式化 247
4.1 實數(shù)集的公理系統(tǒng)及其一般性質 247
4.1.1 實數(shù)集的定義 247
4.1.2 實數(shù)的某些一般的代數(shù)性質 250
4.1.3 完備性公理與數(shù)集的確界存在性 259
4.2 幾個重要的實數(shù)子集262
4.2.1 自然數(shù)與數(shù)學歸納法原理 262
4.2.2 有理數(shù)與無理數(shù) 267
4.2.3 Archimedes原理 280
4.3 實數(shù)的幾何解釋 286
4.4 實數(shù)模型的唯一性 291
第5章 結論與注記.321
附錄一 Coq指令說明 327
A.1 Coq專用術語327
A.2 Coq證明指令328
A.3 集成策略 331
附錄二 公理集論與實數(shù)公理化的結構性呈現(xiàn) 343
參考文獻 376
索引 387
后記 393
表格目錄
表1.1 書中涉及的常用 Coq 指令簡表9
表1.2 書中涉及的常用 Coq 術語的基本含義 12
表5.1 公理化集合論形式化系統(tǒng)代碼量統(tǒng)計 321
表5.2 分析基礎形式化系統(tǒng)代碼量統(tǒng)計 322
表5.3 實數(shù)公理化形式系統(tǒng)代碼量統(tǒng)計 322
插圖目錄
圖1.1 Kelley的《一般拓撲學》英文版和中文版封面 4
圖1.2 Landau的《分析基礎》德文、英文版和中文版封面 5
圖1.3 Zorich的《數(shù)學分析》俄文版、英文版、中文版封面 7
圖5.1 實數(shù)模型同構唯一性的證明截圖323
圖5.2 計算機軟件著作權登記證書 323
圖5.3 Lean 驗證數(shù)學定理輸出的命題和概念網絡 325