控制理论与应用2024，Vol.41Issue(7)：1274-1285,12.DOI:10.7641/CTA.2024.30698
基于MK的实数公理系统相容性和范畴性的Coq形式化
Formalization in Coq of the consistency and categoricity of the real number axiomatic system based on Morse-Kelley set theory
摘要
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引用本文复制引用
郭达凯,冷姝锟,窦国威,陈思,郁文生..基于MK的实数公理系统相容性和范畴性的Coq形式化[J].控制理论与应用,2024,41(7):1274-1285,12.基金项目
国家自然科学基金项目(61936008)资助.Supported by the National Natural Science Foundation of China(61936008). （61936008）
