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

定　價：￥128.00

作　者：	郁文生，孫天宇，付堯順著
出版社：	科學出版社
叢編項：	數(shù)學機械化叢書
標　簽：	暫缺

購買這本書可以去

ISBN：	9787030640390	出版時間：	2020-03-01	包裝：	平裝
開本：	32開	頁數(shù)：	316	字數(shù)：

內(nèi)容簡介

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