內容簡介
布爾巴基學派的序、代數、拓撲三大母結構是現代數學的基礎。利用計算機證明輔助工具，可以完整構建這三大母結構的形式化繫統。本書利用交互式定理證明工具Coq，實現Morse-Kelley公理化集合論形式化繫統，包括對該體繫中8個公理(含選擇公理)和1個公理圖示以及全部181條定義或定理的Coq描述，其中構造了序數和基數，定義了非負整數，把Peano公設當作定理，可以迅速而自然地給出一個數學基礎，擺脫了明顯的悖論。這是Morse。Kelley公理化集合論繫統的搶先發售形式化實現。在Morse-Kelley公理化集合論形式化繫統下，作為應用，我們給出選擇公理與它的幾個有名等價命題間等價性的機器證明，這些命題包括Tukey引理、Hausdorff極大原則、極大原則、Zorn引理、良序定理及Zermelo假定等。在我們開發的繫統中，全部定理無例外地給出Coq的機器證明代碼，所有形式化過程已被Co......
