| 引用本文: | 郭达凯,冷姝锟,窦国威,陈思,郁文生.基于MK的实数公理系统相容性和范畴性的Coq形式化[J].控制理论与应用,2024,41(7):1274~1285.[点击复制] |
| GUO Da-kai,LENG Shu-kun,DOU Guo-wei,CHEN Si,YU Wen-sheng.Formalization in Coq of the consistency and categoricity of the real number axiomatic system based on Morse-Kelley set theory[J].Control Theory and Technology,2024,41(7):1274~1285.[点击复制] |
|
| 基于MK的实数公理系统相容性和范畴性的Coq形式化 |
| Formalization in Coq of the consistency and categoricity of the real number axiomatic system based on Morse-Kelley set theory |
| 摘要点击 364 全文点击 127 投稿时间：2023-10-26 修订日期：2024-06-16 |
| 查看全文 查看/发表评论 下载PDF阅读器 |
| DOI编号 DOI: 10.7641/CTA.2024.30698 |
| 2024,41(7):1274-1285 |
| 中文关键词 Morse-Kelley公理化集合论 实数公理系统 相容性 范畴性 Coq 形式化 机器证明 人工智能 |
| 英文关键词 Morse-Kelley set theory real number axiomatic system consistency categoricity Coq formalization machine-assisted theorem proving artificial intelligence |
| 基金项目 国家自然科学基金项目(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. |
|
|
|
|
|