基于MK的实数公理系统相容性和范畴性的Coq形式化
Formalization in Coq of the consistency and categoricity of the real number axiomatic system based on Morse-Kelley set theory
郭达凯 1冷姝锟 1窦国威 1陈思 1郁文生1
作者信息
- 1. 北京邮电大学电子工程学院天地互联与融合北京市重点实验室,北京 100876
- 折叠
摘要
数学定理机器证明是人工智能基础理论的深刻体现.实数理论是数学分析的基础,实数公理系统是建立实数理论的重要方法.Morse-Kelley公理化集合论(MK)作为现代数学的基础,也为实数构建提供了严谨的数学框架和工具.本文使用定理证明器Coq,基于MK对实数公理系统进行了深入探索.在优化了MK形式化代码的基础上,形式化构建了完整的实数公理系统,并通过形式化Landau《分析基础》中的实数模型,证明其相对于MK相容,此外,还形式化证明了实数公理系统所有模型在同构意义下是唯一的,验证了实数公理系统的范畴性.本文全部定理无例外地给出Coq的机器证明代码,所有形式化过程己被Coq验证,并在计算机上运行通过,充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.该系统可方便地应用于拓扑学和代数学理论的形式化构建.谨以此文庆祝我国著名控制系统专家秦化淑研究员九十华诞!
Abstract
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 formal-ized 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 vivid-ly 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/形式化/机器证明/人工智能Key words
Morse-Kelley set theory/real number axiomatic system/consistency/categoricity/Coq/formalization/machine-assisted theorem proving/artificial intelligence引用本文复制引用
出版年
2024
国家科技期刊平台
NSTL
万方数据