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

Formalization in Coq of the consistency and categoricity of the real number axiomatic system based on Morse-Kelley set theory

作　　者：郭达凯 冷姝锟 窦国威 陈思 郁文生 GUO Da-kai;LENG Shu-kun;DOU Guo-wei;CHEN Si;YU Wen-sheng(Beijing Key Laboratory of Space-Ground Interconnection and Convergence,School of Electronic Engineering,Beijing University of Posts and Telecommunications,Beijing 100876,China)

机构地区：[1]北京邮电大学电子工程学院天地互联与融合北京市重点实验室,北京100876

出　　处：《控制理论与应用》2024年第7期1274-1285,共12页Control Theory & Applications

基　　金：国家自然科学基金项目(61936008)资助。

摘　　要：数学定理机器证明是人工智能基础理论的深刻体现.实数理论是数学分析的基础,实数公理系统是建立实数理论的重要方法.Morse-Kelley公理化集合论(MK)作为现代数学的基础,也为实数构建提供了严谨的数学框架和工具.本文使用定理证明器Coq,基于MK对实数公理系统进行了深入探索.在优化了MK形式化代码的基础上,形式化构建了完整的实数公理系统,并通过形式化Landau《分析基础》中的实数模型,证明其相对于MK相容,此外,还形式化证明了实数公理系统所有模型在同构意义下是唯一的,验证了实数公理系统的范畴性.本文全部定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.该系统可方便地应用于拓扑学和代数学理论的形式化构建.谨以此文庆祝我国著名控制系统专家秦化淑研究员九十华诞!Machine-assisted theorem proving represents a profound foundational theory within the field of artificial intelligence.The theory of real numbers serves as the bedrock of mathematical analysis,and the real number axiomatic system constitutes an essential methodology for establishing this theory.The Morse-Kelley axiomatic set theory(MK),functioning as the foundation of contemporary mathematics,furnishes a rigorous mathematical scaffolding and toolkit for the conceptualization of real numbers.In the present study,we employ the theorem prover Coq to undertake an exhaustive investigation into the real number axiomatic system,predicated on the MK framework.Upon the refinement of formalized MK code,we have systematically constructed the real number axiomatic system.This construction is substantiated through the formalization of the real number model presented in Landau's Foundations of Analysis,and we establish its consistency relative to MK.Furthermore,we provide formalized proofs demonstrating that all models of the real number axiomatic system are unique in the sense of isomorphism,thereby corroborating the categorical nature of the real number axiomatic system.For all theorems presented herein,we furnish machine-verified Coq code without exception.The entire formalization procedure has been corroborated by Coq and successfully executed on a computational platform.This vividly illustrates the readability,interactivity,and intelligence intrinsic to mathematical theorem proving based on Coq.Our formalized system manifests itself as a paradigm of rigor,precision,and reliability,and can be conveniently deployed in the formal construction of theories in topology and algebra.This paper is respectfully proffered in honor of the nonagenarian milestone achieved by professor Qin Huashu,an outstanding scientist in the field of control systems.

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

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]