公理化集合论机器证明系统
【作 者】郁文生，孙天宇，付尧顺著
【丛书名】数学机械化丛书
【形态项】 295
【出版项】 北京：科学出版社 , 2020.03
【ISBN号】978-7-03-064039-0
【中图法分类号】O144-39
【原书定价】128.00
【主题词】集论公理系统-机器证明
【参考文献格式】 郁文生，孙天宇，付尧顺著. 公理化集合论机器证明系统. 北京：科学出版社, 2020.03.
内容提要:
本书利用交互式定理证明工具Coq，实现Morse-Kelley公理化集合论形式化系统，包括对该体系中8个公理（含选择公理）和1个公理图示以及全部181条定义或定理的Coq描述，其中构造了序数和基数，定义了非负整数，把Peano公设当作定理，可以迅速而自然地给出一个数学基础，摆脱了明显的悖论。
下载地址
公理化集合论机器证明系统.rar