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

定　價(jià)：￥128.00

作　者：	郁文生，孫天宇，付堯順著
出版社：	科學(xué)出版社
叢編項(xiàng)：	數(shù)學(xué)機(jī)械化叢書
標(biāo)　簽：	暫缺

購買這本書可以去

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

內(nèi)容簡介

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