公理化集合論機器證明系統(tǒng)

　　利用計算機證明輔助工具，可以完整構(gòu)建這三大母結(jié)構(gòu)的形式化系統(tǒng)。本書利用交互式定理證明工具Coq，實現(xiàn)Morse-Kelley公理化集合論形式化系統(tǒng)，包括對該體系中8個公理（含選擇公理）和1個公理圖示以及全部181條定義或定理的Coq描述，其中構(gòu)造了序數(shù)和基數(shù)，定義了非負(fù)整數(shù)，把Peano公設(shè)當(dāng)作定理，可以迅速而自然地給出一個數(shù)學(xué)基礎(chǔ)，擺脫了明顯的悖論。這是Morse-Kelley公理化集合論系統(tǒng)的首次形式化實現(xiàn)。

暫缺《公理化集合論機器證明系統(tǒng)》作者簡介