000    nam 
001 __ CAL 012020017402
005 __ 20200407111109.6
010 __ ■a978-7-03-064039-0■b精装■dCNY128.00
099 __ ■aCAL 012020017402
100 __ ■a20200407d2020    em y0chiy50      ea
101 0_ ■achi
102 __ ■aCN■b110000
105 __ ■aak  a   001yy
106 __ ■ar
200 1_ ■a公理化集合论机器证明系统■Agong li hua ji he lun ji qi zheng ming xi tong■f郁文生, 孙天宇, 付尧顺著
210 __ ■a北京■c科学出版社■d2020
215 __ ■axiii, 293页■c图■d25cm
225 2_ ■a数学机械化丛书■Ashu xue ji xie hua cong shu■v13
320 __ ■a有书目 (第284-289页) 和索引
330 __ ■a本书利用交互式定理证明工具 Coq, 实现 Morse-Kelley 公理化集合论形式化系统, 包括对该体系中 8 个公理 (含选择公理)和 1 个公理图示以及全部 181 条定义或定理的Coq 描述, 其中构造了序数和基数, 定义了非负整数, 把Peano公设当作定理, 可以迅速而自然地给出一个数学基础, 摆脱了明显的悖论. 这是 Morse-Kelley公理化集合论系统的首次形式化实现. 在Morse-Kelley公理化集合论形式化系统下, 作为应用, 我们给出选择公理与它的几个著名等价命题间等价性的机器证明。
410 _0 ■12001 ■a数学机械化丛书■v13
606 0_ ■a集论公理系统■Aji lun gong li xi tong■x机器证明
690 __ ■aO144■v5
701 _0 ■a郁文生■Ayu wen sheng■4著
701 _0 ■a孙天宇■Asun tian yu■4著
701 _0 ■a付尧顺■Afu yao shun■4著
801 _0 ■aCN■bNMU■c20200407
905 __ ■bH00264161■aTSG■dO144■e0006■f1
906 __ ■d128.00
920 __ ■a215010■z1