基于MK的实数公理系统相容性和范畴性的Coq形式化

• 全文链接
• 请求原文

作   者：

郭达凯;  冷姝锟;  窦国威;  陈思;  郁文生; 

作者机构：

北京邮电大学电子工程学院天地互联与融合北京市重点实验室; 

关键词：

Morse-Kelley公理化集合论;  实数公理系统;  Coq;  形式化;  人工智能;  机器证明;  相容性;  范畴性; 

期刊名称：

控制理论与应用

i s s n：

1000-8152

年卷期：

2024 年 007 期

页   码：

1274-1285

摘   要：

数学定理机器证明是人工智能基础理论的深刻体现.实数理论是数学分析的基础,实数公理系统是建立实数理论的重要方法. Morse-Kelley公理化集合论(MK)作为现代数学的基础,也为实数构建提供了严谨的数学框架和工具.本文使用定理证明器Coq,基于MK对实数公理系统进行了深入探索.在优化了MK形式化代码的基础上,形式化构建了完整的实数公理系统,并通过形式化Landau《分析基础》中的实数模型,证明其相对于MK相容,此外,还形式化证明了实数公理系统所有模型在同构意义下是唯一的,验证了实数公理系统的范畴性.本文全部定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.该系统可方便地应用于拓扑学和代数学理论的形式化构建.