目錄
前言
基本符號
第1章 引言 1
1.1 概述 1
1.1.1 證明輔助工具 Coq 1
1.1.2 形式化數(shù)學(xué) 2
1.1.3 Morse-Kelley公理化集合論系統(tǒng) 3
1.1.4 分析基礎(chǔ) 5
1.1.5 本書結(jié)構(gòu)安排 7
1.2 基本Coq指令清單及邏輯預(yù)備知識 8
第2章 Morse-Kelley公理化集合論的形式化系統(tǒng)實(shí)現(xiàn) 14
2.1 分類公理圖式 14
2.2 分類公理圖式 (續(xù)) 15
2.3 類的初等代數(shù) 16
2.4 集的存在性 21
2.5 序偶：關(guān)系 25
2.6 函數(shù) 29
2.7 良序 36
2.8 序 43
2.9 非負(fù)整數(shù) 51
2.10 選擇公理 54
2.11 基數(shù) 57
第3章 分析基礎(chǔ)的形式化系統(tǒng)實(shí)現(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 分?jǐn)?shù) 98
3.2.1 定義和等價(jià) 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í)數(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 復(fù)數(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 共軛復(fù)數(shù) 226
3.5.7 絕對值 227
3.5.8 和與積 229
3.5.9 冪 241
3.5.10 將實(shí)數(shù)編排在復(fù)數(shù)系統(tǒng)中 243
第4章 實(shí)數(shù)集的公理系統(tǒng)形式化 247
4.1 實(shí)數(shù)集的公理系統(tǒng)及其一般性質(zhì) 247
4.1.1 實(shí)數(shù)集的定義 247
4.1.2 實(shí)數(shù)的某些一般的代數(shù)性質(zhì) 250
4.1.3 完備性公理與數(shù)集的確界存在性 259
4.2 幾個(gè)重要的實(shí)數(shù)子集262
4.2.1 自然數(shù)與數(shù)學(xué)歸納法原理 262
4.2.2 有理數(shù)與無理數(shù) 267
4.2.3 Archimedes原理 280
4.3 實(shí)數(shù)的幾何解釋 286
4.4 實(shí)數(shù)模型的唯一性 291
第5章 結(jié)論與注記.321
附錄一 Coq指令說明 327
A.1 Coq專用術(shù)語327
A.2 Coq證明指令328
A.3 集成策略 331
附錄二 公理集論與實(shí)數(shù)公理化的結(jié)構(gòu)性呈現(xiàn) 343
參考文獻(xiàn) 376
索引 387
后記 393
表格目錄
表1.1 書中涉及的常用 Coq 指令簡表9
表1.2 書中涉及的常用 Coq 術(shù)語的基本含義 12
表5.1 公理化集合論形式化系統(tǒng)代碼量統(tǒng)計(jì) 321
表5.2 分析基礎(chǔ)形式化系統(tǒng)代碼量統(tǒng)計(jì) 322
表5.3 實(shí)數(shù)公理化形式系統(tǒng)代碼量統(tǒng)計(jì) 322
插圖目錄
圖1.1 Kelley的《一般拓?fù)鋵W(xué)》英文版和中文版封面 4
圖1.2 Landau的《分析基礎(chǔ)》德文、英文版和中文版封面 5
圖1.3 Zorich的《數(shù)學(xué)分析》俄文版、英文版、中文版封面 7
圖5.1 實(shí)數(shù)模型同構(gòu)唯一性的證明截圖323
圖5.2 計(jì)算機(jī)軟件著作權(quán)登記證書 323
圖5.3 Lean 驗(yàn)證數(shù)學(xué)定理輸出的命題和概念網(wǎng)絡(luò) 325