《反基础公理的逻辑研究》概要
（注：李娜，南开大学教授，博士生导师。）
一、研究的目的、意义及方法
在经典的公理集合论系统ZFC中，由于基础公理FA（也称良基公理或者正则公理）的存在，所以，这样的集合论，也称为良基集合论，它所描述的集合也称为良基集合。在ZFC中，由于基础公理FA是独立于ZFC-（=ZFC-FA）的其他公理的，所以，如果用反基础公理（或称非良基公理）代替基础公理FA，那么ZFC-中所有不依赖于FA的结果在非良基集合论中都成立。而这样的集合论，也称为非良基集合论，它的论域中既包含良基集合，又包含被基础公理排除掉的具有无穷∈递降链或循环性质的非良基集合。而具有循环性质的非良基集合（也称超集或奇异集合）的最大特点是具有性质Ω∈Ω，即包含其自身作元素，如Ω={Ω}。
然而，由于在哲学、逻辑学、数学、计算机科学、语言学、情境语义学、人工智能领域和认知科学中，存在着许许多多各种各样的循环现象和问题，而非良基集合恰恰可以以一种明显的方式来刻画循环的现象和问题，因此，在集合论的发展中，用反基础公理替换基础公理也成为必然。反基础公理最早是由福蒂（M.Forti）和洪塞尔（F.Honsel）在他们1983年的一篇论文中给出的。现在这条公理被阿克采尔（P.Aczel）称作AFA，并且阿克采尔还给出了一套建立各种各样循环现象模型的方法。
20世纪70年代前后，互模拟（也称双仿）的概念几乎同时并且独立地在集合论、模态逻辑和计算机科学等领域中提出。在此之前，两个结构之间的关系只能用同态或者同构来衡量。然而，两个同态的结构其中一个一定能嵌入到另一个之中，因此，它们形式上一个包含另一个，本质上是相同的。同构的结构不论是形式上还是本质上都被认为是相同的。于是人们希望有一个比同态或同构弱的概念。而互模拟不仅是一个比同态或同构弱的概念，同时还能保证两个结构之间相互模仿对方。特别地，“互模拟也是非良基集合论的核心概念。当人们把集合论的论域由良基集合扩充到非良基集合时，经典的外延公理在判断非良基集合之间的相等时无能为力。运用基于互模拟概念的强外延公理可以很好地解决这一问题”（注：李娜、姚从军：《互模拟的一些基本性质》，《云南师范大学学报》（哲学社会科学版），2010年第5期，第69页。）。今天，互模拟理论因为各种各样的目的被广泛地用在并发系统、函数语言、对象定位语言、类型论、数据类型、域论、数据库、编辑最优化、程序分析、证明工具等中。
然而，为公理集合论的ZFC系统建立模型，一直是公理集合论研究中的一个重要问题。20世纪90年代以后，为集合论的含有各种反基础公理的公理系统建立模型，是公理集合论研究中的一个热点问题。因此，反基础公理的逻辑研究从理论上丰富了数理逻辑的重要分支——公理集合论刻画集合论模型的理论；丰富了巴威斯（J.Barwise）等人关于用方程组研究反基础公理的理论，为现代逻辑的研究提供了证明论的工具，促进了逻辑学的发展。同时，用非良基集合重新刻画模态逻辑，建立模态系统之间的互模拟关系，必将进一步促进数理逻辑与逻辑、哲学之间的相互渗透、相互融合。因此，这些工作都可能在基础理论的层面上促进数学、逻辑学和哲学的发展。与此同时，这些工作对于我国这样一个对逻辑研究还比较薄弱的状况来说，无疑具有十分积极的意义。
本成果所采用的主要方法是数理逻辑中构建模型的方法和代数的方法。
二、成果的主要内容
本成果分为三编。第Ⅰ编，它是笔者承担的2008年度国家社会科学基金项目“超集、双仿以及在模态逻辑、计算机科学中的作用研究”（项目批准号：08BZX049）的最终研究成果的部分内容；第Ⅱ编，它是笔者承担的2011年度天津市社会科学基金项目“基于方程组的反基础公理AFA以及应用研究”（项目批准号：TX11-007）的最终研究成果的部分内容；第Ⅲ编即附录，它也是笔者承担的2008年度国家社会科学基金项目“超集、双仿以及在模态逻辑、计算机科学中的作用研究”的最终研究成果的部分内容。
第Ⅰ编：为用图刻画的各种反基础公理系统（ZFC-+AFA（或者SAFA、FAFA以及反基础公理家族AFA~））建立不同的集论模型，从而证明各种反基础公理与ZFC-的相对协调性。
第Ⅱ编：修正、完善并丰富了巴威斯等人用代数方法（方程组）刻画的反基础公理——解引理的理论。
第Ⅲ编：包括两个附录。附录1——给出了结构之间的互模拟理论。附录2——给出了项目研究期间发表的四篇论文。
第Ⅰ编的主要内容如下：
为集合论的公理系统建立模型是公理集合论研究的一个重要问题。由于人们已经为经典的公理集合论系统ZFC建立了自然模型、可构成模型、布尔值模型以及含有原子的模型，因此，本成果在第Ⅰ编中为用图的方法刻画的反基础公理AFA（或者SAFA、FAFA以及反基础公理家族AFA~）所构成的非良基集合论系统ZFC-+AFA（或者SAFA、FAFA以及反基础公理家族AFA~）建立了以下三种模型：
（1）以ZFC的布尔值模型VB（B是一个完全的布尔代数）为基础，采用阿克采尔的方法，构建了阿克采尔的非良基集合论公理系统ZFC-+AFA的一种模型。在此基础上，构建了由反基础公理家族AFA~所构成非良基集合论公理系统ZFC-+AFA~的模型，并由此构建了斯科特（D.Scott）的非良基集合论公理系统ZFC-+SAFA和费斯勒（P.Finsler）的非良基集合论公理系统ZFC-+FAFA的模型。
（2）在可构成公理V=L的假设下，利用ZFC的可构成模型L，采用阿克采尔的方法，构建了阿克采尔的非良基集合论公理系统ZFC-+AFA的一种模型。在此基础上，构建了由反基础公理家族AFA~所构成非良基集合论公理系统ZFC-+AFA~的模型，并由此构建了斯科特的非良基集合论公理系统V=L+ZFC-+SAFA和费斯勒的非良基集合论公理系统V=L+ZFC-+FAFA的模型。
（3）利用ZFC+A（A断言：存在原子的集合）含有原子的集合A的模型V（A），采用阿克采尔的方法，构建了阿克采尔的非良基集合论公理系统ZFC-+A+AFA的一种模型。在此基础上，构建了由反基础公理家族AFA~所构成非良基集合论公理系统ZFC-+A+AFA~的模型，并由此构建了斯科特的非良基集合论公理系统ZFC-+A+SAFA和费斯勒的非良基集合论公理系统ZFC-+A+FAFA的模型。
第Ⅱ编的主要内容如下：
巴威斯等人用代数方法（方程组）所刻画的反基础公理——解引理AFA断言：平坦方程组有唯一解。然而，当平坦方程组是x={x}时，Ω={{{{…{{∅}}…}}}}（这里省略号表示有无穷多层括号）和Ω'={{{{…{{∅，{∅}}}…}}}}（这里省略号表示有无穷多层括号）都满足Ω={Ω}并且Ω'={Ω'}。也就是说，Ω和Ω'都是集合方程组x={x}的解，但是，Ω≠Ω'。这与巴威斯的假设平坦方程组有唯一解不一致。
为了使巴威斯等人的解引理AFA更符合直观，本成果基于线性方程组及解结构的思想，将巴威斯等人的平坦方程组划分为齐次平坦方程组和（巴威斯型的）平坦方程组，并假设齐次平坦方程组有解，假设（巴威斯型的）平坦方程组有唯一解。这样一来，x={x}是齐次平坦方程组，根据假设，x={x}有解而不是唯一解。因此，本篇利用齐次线性方程组和方程组之间的关系以及它们解之间的关系，完成了下面的工作：
（1）定义了齐次平坦方程组并给出了它的解引理LAFA：每个齐次平坦方程组都有一个解。然后，在齐次平坦方程组的基础上，定义了（巴威斯型的）平坦方程组，并给出了它的解引理AFA：A（原子的集合）上的每个（巴威斯型的）平坦方程组都有一个唯一解。最后，给出平坦方程组的一种推广形式——一种广义的平坦方程组。
（2）定义了两个齐次平坦方程组之间的互模拟；给出并证明如果两个或两个以上的齐次平坦方程组有相同解，那么这两个或两个以上的齐次平坦方程组是互模拟的；在此基础上证明了（巴威斯型的）平坦方程组有相同解的充分必要条件；给出并证明了以A为相同原子集的两个广义方程组之间互模拟的一些基本性质；利用方程组之间互模拟的这些基本性质（不用解引理）证明了广义平坦方程组上的极大互模拟是一个等价关系。
（3）定义了一种广义的齐次方程组；在此基础上，定义了广义的方程组并给出了相应的解引理；最后证明了：在ZFC-中，AFA等价于每个广义方程组有一个唯一的解。
（4）证明了基于方程组的反基础公理——解引理AFA与ZFC-的相对协调性。
（5）证明了每个图有一个装饰等价于每个齐次平坦方程组有一个解。
（6）证明了（巴威斯型的）平坦方程组有唯一的解等价于A上的每个图有唯一的装饰。
（7）定义费斯勒齐次平坦方程组；同时给出了费斯勒齐次平坦方程组的解引理LFAFA；证明了费斯勒齐次平坦方程组的解引理与费斯勒图的反基础公理的等价性。
（8）证明了费斯勒平坦方程组的解引理与A上的每个费斯勒图的反基础公理的等价性。
（9）定义一种不依赖于代入规则的齐次崎岖方程组以及崎岖方程组，给出了它们的解引理，并表明：不用代入，用集合的累积层也能使我们处理一些较复杂的方程组。
第Ⅲ编的主要内容如下：
本成果在附录1中完成了下面的工作：
（1）在两个框架之间，给出一种比同态弱的概念——满模拟，并在这种定义下证明了两个结构之间的一些保持性。
（2）在两个框架之间，给出一种比同构弱的概念——互模拟，并在这种定义下证明了两个结构之间的一些不变性。
在附录2中给出四篇已发表的论文，其中：
（1）论文《集合论的反基础公理》（《哲学动态》，2009年第1期）和《论基础公理与反基础公理》（《逻辑学研究》，2013年第2期）主要讨论了基础公理与反基础公理。
（2）论文《互模拟的一些基本性质》（《云南师范大学学报》（哲学社会科学版），2010年第5期）给出了能够刻画计算机科学、模态逻辑和集合论中互模拟概念的一个统一定义，并在这种定义下证明了互模拟的一些基本性质。
（3）论文《解悖方法研究近况》（《哲学动态》，2011年第11期）主要介绍了用解引理AFA解悖的方法。
三、成果的学术创新和应用价值
1.学术创新
第Ⅰ编的学术创新如下：
本编为阿克采尔用图的方法刻画的反基础公理AFA（或者SAFA、FAFA以及反基础公理家族AFA~）所构成的非良基集合论系统ZFC-+AFA（或者SAFA、FAFA以及反基础公理家族AFA~）建立了以下三种模型：
首先，基于ZFC的布尔值模型VB构建了阿克采尔的非良基集合论公理系统ZFC-+AFA的一种模型。在此基础上，构建了由反基础公理家族AFA~所构成的非良基集合论公理系统ZFC-+AFA~的模型，并由此构建了斯科特的非良基集合论公理系统ZFC-+SAFA和费斯勒的非良基集合论公理系统ZFC-+FAFA的模型。
其次，假设可构成公理V=L成立，利用ZFC的可构成模型L，构建了阿克采尔的非良基集合论公理系统ZFC-+AFA的一种模型。在此基础上，构建了由反基础公理家族AFA~所构成的非良基集合论公理系统ZFC-+AFA~的模型，并由此构建了斯科特的非良基集合论公理系统V=L+ZFC-+SAFA和费斯勒的非良基集合论公理系统V=L+ZFC-+FAFA的模型。
最后，利用ZFC+A（A断言：存在原子的集合）含有原子的集合A的模型V（A），构建了阿克采尔的非良基集合论公理系统ZFC-+A+AFA的一种模型。在此基础上，构建了由反基础公理家族AFA~所构成的非良基集合论公理系统ZFC-+A+AFA~的模型，并由此构建了斯科特的非良基集合论公理系统ZFC-+A+SAFA和费斯勒的非良基集合论公理系统ZFC-+A+FAFA的模型。
第Ⅱ编的学术创新如下：
为了使巴威斯等人用代数的方法（方程组）所刻画的解引理AFA更符合直观，本编基于线性方程组及解结构的思想和方法，将巴威斯等人的平坦方程组划分为齐次平坦方程组和（巴威斯型的）平坦方程组。在此基础上，完成了下面的工作：
首先，定义了齐次平坦方程组并给出了它的解引理LAFA：每个齐次平坦方程组都有一个解。然后，在齐次平坦方程组的基础上，定义了（巴威斯型的）平坦方程组，并给出了它的解引理AFA：A（原子的集合）上的每个（巴威斯型的）平坦方程组都有一个唯一解。最后，给出平坦方程组的一种推广形式——一种广义的平坦方程组。
第二，定义了两个齐次平坦方程组之间的互模拟；提出并证明了如果两个或两个以上的齐次平坦方程组有相同解，那么这两个或两个以上的齐次平坦方程组是互模拟的；在此基础上证明了（巴威斯型的）平坦方程组有相同解的充分必要条件；提出并证明了以A为相同原子集的两个广义方程组之间互模拟的一些基本性质；利用方程组之间互模拟的这些基本性质（不用解引理）证明了以A为原子的广义平坦方程组上的极大互模拟是一个等价关系。
第三，定义了一种广义的齐次方程组；在此基础上，定义了广义的方程组并给出了相应的解引理；最后证明了在ZFC-中，AFA等价于每个广义方程组有一个唯一的解。此外，还证明了基于方程组的反基础公理——解引理AFA与ZFC-的相对协调性。
第四，证明了每个图有一个装饰等价于每个齐次平坦方程组有一个解以及证明了（巴威斯型的）平坦方程组有唯一的解等价于A上的每个图有唯一的装饰。
第五，定义费斯勒齐次平坦方程组；同时给出了费斯勒齐次平坦方程组的解引理LFAFA；证明了费斯勒齐次平坦方程组的解引理与费斯勒图的反基础公理的等价性。此外，还证明了费斯勒平坦方程组的解引理与A上的每个费斯勒图的反基础公理的等价性。
最后，定义一种不依赖于代入规则的齐次崎岖方程组以及崎岖方程组，给出了它们的解引理，并表明：不用代入，用集合的累积层也能使我们处理一些较复杂的方程组。
第Ⅲ编的学术创新如下：
首先，在两个框架之间，给出了一种比同态弱的概念——满模拟，并在这种定义下证明了两个结构之间的一些保持性。
第二，在两个框架之间，给出了一种比同构弱的概念——互模拟，并在这种定义下证明了两个结构之间的一些不变性。
第三，给出能够刻画计算机科学、模态逻辑和集合论中互模拟概念的一个统一定义，并在这种定义下证明了互模拟的一些基本性质。
最后，基于“循环并不可恶”的思想，指出了基础公理的局限性；分析反基础公理导致集合论域在V=WF上不断扩张的方法，并指出这种扩张的方法与数系扩张的方法相同；同时得出结论：良基集合理论（ZFC）与非良基集合理论（ZFC-+AFA（或者ZFC和ZFC-+FAFA或者ZFC和ZFC-+SAFA））之间的关系类似于欧几里得几何学与非欧几何学之间的关系。
2.应用价值
（1）进一步完善和丰富了逻辑学理论。
集合论是一种为带结构的对象构造模型的最灵活的工具。20世纪初，罗素用康托尔集合论中的基本概念“∈”构造了类T={x|x∉x}，而T中的元素具有自己不属于自身的性质，由此导致了矛盾，这个矛盾被称为罗素悖论。罗素悖论的出现引起了许多数学家的震惊，也由此引起了数学的第三次危机。为了排除悖论，集合论学者们用公理化的方法对康托尔的集合论进行了修正，建立了许多严谨的集合论系统，在整个20世纪中应用最广泛的就是ZFC公理集合论。由于ZFC公理集合论中存在基础公理（或称正则公理或称良基公理），基础公理断言，ZFC公理集合论中的集合都是良基的（即非循环的和非无穷递降的），由此直接排除了循环的类，也排除了所有非良基集合。而非良基集合论是在ZFC的基础上，去掉基础公理，引入反基础公理得到的。它的方法是扩大ZFC公理集合论的论域，将Ω={Ω}等视为集合，即将那些具有循环性质和具有无穷∈递降链的对象也作为集合，从而为循环的理论建立了集合论模型。1988年阿克采尔利用图来刻画非良基集合并研究了反基础公理AFA。1989年巴威斯等人利用方程组来刻画非良基集合并研究了反基础公理AFA。本成果的工作无疑丰富和完善了非良基集合理论。
（2）促进了集合论与模态逻辑、计算机科学理论之间的相互渗透和相互融合。
20世纪70年代，互模拟的概念几乎同时出现在集合论、模态逻辑和计算机科学中。本成果给出一种能够刻画集合论、模态逻辑和计算机科学中互模拟概念的统一定义，并在这种定义下证明了互模拟的一些基本性质。另外，借助代数结构的思想，在两个框架之间，给出一种比同态弱的概念——满模拟，并在这种定义下证明了两个结构之间的一些保持性；在两个框架之间，给出一种比同构弱的概念——互模拟，并在这种定义下证明了两个结构之间的一些不变性。这些工作不仅促进了逻辑学各分支理论相互渗透和相互融合，并可能是在最基础的层面上，促进逻辑学、数学、哲学以及计算机科学的发展。
（3）为哲学、人工智能理论、计算机科学、认知科学、语言学和哲学等领域的研究提供工具。
近30年来，循环现象已经引起了哲学、人工智能理论、计算机科学、认知科学、语言学和哲学等领域中研究者的广泛重视。在这些领域中，非良基集合的模型可以很方便地为循环现象建立模型。如，应用平坦方程组的解引理AFA消解悖论；应用用图刻画的反基础公理建立了程序语言语义的一种数学方法，即计算程序进程的终结共代数语义。因此，本成果的研究为人工智能理论、计算机科学、认知科学、语言学和哲学等领域的研究提供了更方便、更简捷的工具。