|
题名:
|
公理化集合论机器证明系统 / 郁文生, 孙天宇, 付尧顺著 , |
|
ISBN:
|
978-7-03-064039-0 价格： CNY128.00 |
|
语种:
|
chi |
|
载体形态:
|
xiii, 293页 图 25cm |
|
出版发行:
|
出版地： 北京 出版社： 科学出版社 出版日期： 2020 |
|
内容提要:
|
本书利用交互式定理证明工具 Coq, 实现 Morse-Kelley 公理化集合论形式化系统, 包括对该体系中 8 个公理 (含选择公理)和 1 个公理图示以及全部 181 条定义或定理的Coq 描述, 其中构造了序数和基数, 定义了非负整数, 把Peano公设当作定理, 可以迅速而自然地给出一个数学基础, 摆脱了明显的悖论. 这是 Morse-Kelley公理化集合论系统的首次形式化实现. 在Morse-Kelley公理化集合论形式化系统下, 作为应用, 我们给出选择公理与它的几个著名等价命题间等价性的机器证明。 |
|
主题词:
|
集论公理系统 机器证明 |
|
中图分类法:
|
O144 版次： 5 |
|
主要责任者:
|
郁文生 著 |
|
主要责任者:
|
孙天宇 著 |
|
主要责任者:
|
付尧顺 著 |
|
索书号:
|
3 |