《公理化集合論機器證明系統》是2019年12月科學出版社出版的圖書，作者是郁文生、孫天宇、付堯順。
基本介紹
- 中文名：公理化集合論機器證明系統
- 作者：郁文生、孫天宇、付堯順
- 類別：數學
- 出版社：科學出版社
- 出版時間：2019年12月
- ISBN：9787030640390
圖書簡介,圖書目錄,
圖書簡介
布爾巴基學派的序、代數、拓撲三大母結構是現代數學的基礎.利用計算機證明輔助工具,可以完整構建這三大母結構的形式化系統.本書利用互動式定理證明工具Coq,實現Morse-Kelley公理化集合論形式化系統,包括對該體系中8個公理(含選擇公理)和1個公理圖示以及全部181條定義或定理的Coq描述,其中構造了序數和基數,定義了非負整數,把Peano公設當作定理,可以迅速而自然地給出一個數學基礎,擺脫了明顯的悖論.這是Morse-Kelley公理化集合論系統的首次形式化實現.在Morse-Kelley公理化集合論形式化系統下,作為套用,我們給出選擇公理與它的幾個著名等價命題間等價性的機器證明,這些命題包括Tukey引理、Hausdorff極大原則、極大原則、Zorn引理、良序定理及Zermelo假定等.在我們開發的系統中,全部定理無例外地給出Coq的機器證明代碼,所有形式化過程已被Coq驗證,並在計算機上運行通過,體現了基於Coq的數學定理機器證明具有可讀性和互動性的特點,其證明過程規範、嚴謹、可靠.該系統可方便地套用於拓撲學和代數學理論的形式化構建.
圖書目錄
- 第1章引言
- 第2章基本Coq指令清單和預備知識
- 第3章Morse－Kelley公理化集合論的形式化系統實現
- 第4章選擇公理及其等價命題的機器證明
- 第5章結論與註記
- 參考文獻
