弗兰克尔:一代公理化集合论大师

德国犹太数学家亚伯拉罕·阿道夫·弗兰克尔,一生著述丰厚,运用公理化观念发展了p进域、环论、公理化集合论等多个数学理论,是p进域和环论的公理化实践者,是当之无愧的一代公理化集合论大师,同时又是出色的科技史家和教育家。通过对文献的考证和分析,对其生平、成就和影响进行较系统的梳理和总结。

集合论悖论若干哲学问题的思考

一、经典集合论内部的一组悖论自十九世纪七十年代康托(G.Cantor)创立集合论以后,经过康托和其他数学家二、三十年的努力,到十九世纪末,集合论已形成较完整的理论体系。与此同时,一些数学家发展了实数理论,并将实数理论的无矛盾性最终归于逻辑与集合论的无矛盾性。

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

数学定理机器证明是人工智能基础理论的深刻体现.实数理论是数学分析的基础,实数公理系统是建立实数理论的重要方法.Morse-Kelley公理化集合论(MK)作为现代数学的基础,也为实数构建提供了严谨的数学框架和工具.本文使用定理证明器Coq,基于MK对实数公理系统进行了深入探索.在优化了MK形式化代码的基础上,形式化构建了完整的实数公理系统,并通过形式化Landau《分析基础》中的实数模型,证明其相对于MK相容,此外,还形式化证明了实数公理系统所有模型在同构意义下是唯一的,验证了实数公理系统的范畴性.本文全部定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.该系统可方便地应用于拓扑学和代数学理论的形式化构建.谨以此文庆祝我国著名控制系统专家秦化淑研究员九十华诞!

论数学发展史中三次危机的实质和意义

数学的发展也和其他事物的发展一样,不可能是毕直的,它也经历了曲折的发展过程。以下谈谈在数学基础研究中出现的三次危机的历史事实和它们的实质。 1.21/2的发现和数学基础的第一次危机数学起源于数数。人们在漫长的社会实践中,从数数最初抽象出自然数的概念,数论就是在自然数概念的基础上逐渐发展起来的。到纪元前五世纪,毕达哥拉斯学派从前人所取得的数论研究成果出发,开始研究所谓的毕达哥拉斯数。

基于Coq的杨忠道定理形式化证明

实现拓扑学定理的机器证明,是吴文俊院士生前的宿愿.杨忠道定理涉及一般拓扑学中的诸多基本概念,对深刻理解拓扑空间的本质有重要意义.该定理表明,拓扑空间中每一个子集的导集为闭集当且仅当此空间中的每一个单点集的导集为闭集,是一般拓扑学中的一个重要定理.基于定理证明辅助工具Coq,从公理化集合论机器证明系统出发,对一般拓扑学中的开集、闭集、邻域、凝聚点和导集等拓扑基本概念进行形式化描述,给出这些概念基本性质的形式化验证,建立了拓扑空间的形式化框架.在此基础上,实现基于Coq的杨忠道定理形式化证明.全部引理、定理和推论均完整给出Coq的形式化描述和机器证明代码,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.杨忠道定理的形式化证明是一般拓扑学形式化内容的一个深刻体现.

悖论研究的现代哲学意义

悖论，既是一个古老的概念，又是一个年轻的课题。悖论的认识论特征是：可避免性、相对性、辩证性。悖论是思维方式的度量，它转换了人类思维的角度。悖论的发现与研究具有对人类思维的反思功能：使理论系统从它木身的结构中提出新的问题：使思维主体反思原有思维，走出思维定势的峡谷。体论的研究带来了建设功能：它可以改进理论研究系统，使之更加严谨；它可以开拓新的研究领域。任何体论问题的解决都是推动科学发展的巨大杠杆。

基于Coq的有标集族相关定理的机器证明

基于计算机证明辅助工具Coq,参考“公理化集合论”形式化系统,实现朴素集合论形式化系统,并在此基础上给出有标集族及其交和并的形式化,完成有标集族相关定理的Coq描述及机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,体现了Coq的规范、严谨、可靠.为构建完整的点集拓扑理论打下基础,在此系统下,有望实现拓扑空间相关性质的形式化系统.

数学本体论视域中的唯物辩证法——巴迪欧当代辩证法的新型本体论根基之追问

巴迪欧数学本体论视域中的唯物辩证法,是西方马克思主义经历历史辩证法和空间辩证法之后,辩证法研究推进到第三阶段颇具原创性的实验性尝试。实现此尝试的关键是承袭黑格尔辩证法与唯物主义一体化的观念,借道情境结构空间中的存在之思,为之确立新型本体论根基。新本体论根基"新"在凭借数学公理化集合论构筑情境结构空间,将存在之思置身公理化集合论结构空间;深刻处是存在之思以别样的黑格尔式绝对者为逻辑框架,此框架置身公理化集合论结构空间,在此绝对者终结处引入海德格尔式事件概念,借事件概念的开端性思考构筑一种非传统形而上学实体性的黑格尔式反身性自身观念,以凸显当代辩证法的"绝对"内涵,摆脱后现代相对主义和诡辩论的纠缠。

从恩格斯关于数学公理之定义谈起

F.恩格斯(1820-1895)于1873至1883年间写成一本世界名著《自然辩证法》,在该书中对于数学公理给出一个简洁的定义。在现代数学公理化方法研究的历史长河中,D.格高尼和M.巴许是先驱者,而G.皮亚诺和D.希尔伯特则是独立地发现者。1899年,希尔伯特的名著《几何基础》出版;1901年,著名数学家B.罗素又提出创建纯粹数学理论的新思维。从此而后,纯粹数学蓬勃发展,蒸蒸日上。

推荐五本世界公认的逻辑学著作

(1) G·Takeuti和W.M.Zaring的《公理化集合论导引》第2版(Introduction to Axiomatic Set Theory [2nd ed]),本书以Zermelo-Fraenke的理论为线索全面介绍公理化集合的Godel和Cohen相容性和独立性理论,用这种论述方式介绍,读者能较容易地掌握公理化集合论的基本理论以及其他相关结果,并进入到80年代的许多新的前沿课题。本书1971年初版,1982年第2版对初版作了全面刷新,增添了许多新内容,如Silver机、证明可构造性公理化相容性的结构设计等。本书可作为数理逻辑专业研究生一个学期集合论课程的标准教材。 (2) G·Takeuti和W.M.Zaring的《公理化集合论》(Axiomatic Set Theory)。本书是《公理化集合论导引》