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