●第1章 引言
第2章 基本Coq指令清單和預備知識
第3章 Morse-Kelley公理化集合論的形式化繫統實現
3.1 分類公理圖式
3.2 分類公理圖式(續)
3.3 類的初等代數
3.4 集的存在性
3.5 序偶:關繫
3.6 函數
3.7 良序
3.8 序數
3.9 非負整數
3.10 選擇公理
3.11 基數
第4章 選擇公理及其等價命題的機器證明
4.1 基本定義
4.2 Tukey引理
4.3 Hausdor極大原則
4.4 極大原則
4.5 Zermelo假定
4.6 Zorn引理
4.7 良序定理
4.8 良序定理證明選擇公理
4.9 Zermelo假定證明選擇公理
4.10 Tukey引理證明選擇公理
第5章 結論與注記
參考文獻
索引
布爾巴基學派的序、代數、拓撲三大母結構是現代數學的基礎。利用計算機證明輔助工具,可以完整構建這三大母結構的形式化繫統。本書利用交互式定理證明工具Coq,實現Morse-Kelley公理化集合論形式化繫統,包括對該體繫中8個公理(含選擇公理)和1個公理圖示以及全部181條定義或定理的Coq描述,其中構造了序數和基數,定義了非負整數,把Peano公設當作定理,可以迅速而自然地給出一個數學基礎,擺脫了明顯的悖論。這是Morse。Kelley公理化集合論繫統的首次形式化實現。在Morse-Kelley公理化集合論形式化繫統下,作為應用,我們給出選擇公理與它的幾個有名等價命題間等價性的機器證明,這些命題包括Tukey引理、Hausdorff極大原則、極大原則、Zorn引理、良序定理及Zermelo假定等。在我們開發的繫統中,全部定理無例外地給出Coq的機器證明代碼,所有形式化過程已被Coq驗等