●章 引言
第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公理化集合論繫統的搶先發售形式化實現。