选择公理与Tukey引理等价性的机器证明

摘要：

基于计算机证明辅助工具Coq,提出一种选择公理与Tukey引理等价性的形式化证明.在公理化集合论形式化系统基础上,给出选择公理与Tukey引理的形式化描述,这是Tukey引理的首次形式化.完成了选择公理与Tukey引理等价性的证明代码,并在Coq中通过验证.体现了基于Coq的数学定理机器证明具有可读性与交互性特点,其证明过程规范、严谨、可靠,在集合论、拓扑学和代数学的形式化构建中具有重要应用.

关键词：机器证明、形式化数学、选择公理、Tukey引理

所属期刊栏目：42

分类号：TN929.53

资助基金：国家自然科学基金项目61571064, 61936008

在线出版日期：2019-12-31（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：1-7