安徽理工大学图书馆书目检索系统

Online Public Access Catalogue

题名/责任者:

公理化集合论机器证明系统/郁文生, 孙天宇, 付尧顺著

出版发行项:

北京:科学出版社,2020

ISBN及定价:

978-7-03-064039-0 精装/CNY128.00

载体形态项:

xiii, 293页:图;25cm

丛编项:

数学机械化丛书;13

个人责任者:

郁文生 著

个人责任者:

孙天宇 著

个人责任者:

付尧顺 著

学科主题:

集论公理系统-机器证明

中图法分类号:

O144

书目附注:

有书目 (第284-289页) 和索引

提要文摘附注:

本书利用交互式定理证明工具 Coq, 实现 Morse-Kelley 公理化集合论形式化系统, 包括对该体系中 8 个公理 (含选择公理)和 1 个公理图示以及全部 181 条定义或定理的Coq 描述, 其中构造了序数和基数, 定义了非负整数, 把Peano公设当作定理, 可以迅速而自然地给出一个数学基础, 摆脱了明显的悖论. 这是 Morse-Kelley公理化集合论系统的首次形式化实现. 在Morse-Kelley公理化集合论形式化系统下, 作为应用, 我们给出选择公理与它的几个著名等价命题间等价性的机器证明。

豆瓣简介：