论集合论的模型

李娜 何建锋

1 引言

选择公理（AC）在数学中被广泛的使用，它断定：对非空集合的任意收集，我们能从该收集的每个成员中选择一个元素。但是，AC有一些非直觉的后承，如“每个集合都能被良序”，我们难以想像所有实数的集合被良序。

1878年，康托（G.Cantor）构造了连续统假设（continuum hypothesis，CH），它断定：实数的每个无穷集，要么和N（自然数的集合）有相同的基数，要么和R（实数的集合）有相同的基数。CH的形式化为：¬∃x(ℵ0＜|x|＜2ℵ0)，其中|x|表示x的基数。CH有两个推广：一个是广义连续统假设（general continuum hypothesis GCH），∀x¬∃y(|x|＜ |y|＜ |2x|)；另一个是阿列夫假设（aleph hypothesis，AH）∀α(2ℵα= ℵα+1)。GCH蕴涵 AC、CH、AH。

1908年，集合论第一次被策梅洛（E.Zermelo）公理化，后经过斯柯伦（T.Skolem）和弗兰克尔（A.Fraenkel）的改进，形成了ZF，在ZF的基础上添加AC，就得到ZFC。公理化集合论ZFC的诞生，使得元数学成为可能，因为所有的数学都能在ZFC中被形式化。元数学即对数学自身的研究。但是根据哥德尔（K.Gödel）的不完全性定理，ZF或ZFC系统是不完全的，因此，对于我们抱有疑虑的公理AC或假设GCH，它们在形式系统ZF或ZFC中的证明或证伪就变得很有意义。

解决这些问题的努力引导了各种集合论模型的诞生。1922年，弗兰克尔给出了带原子的ZF集合论（简称ZFA）的一个置换模型（permutation model），并用它证明了AC相对于ZFA的独立性（[11]，第46页）。后来，莫斯托夫斯基（A.Mostowski）和施佩克尔（E.P.Specker）相继改进了置换模型。置换模型被用于获得AC相对于ZF0（ZF去掉基础公理）的独立性。1940年，哥德尔发表了他的可构成模型（constructible model），他使用它证明了AC相对于ZF的一致性、GCH相对于ZF+AC的一致性（[11]，第25页）。1956年，塔尔斯基（A.Tarski）提出了自然模型（natural model）的概念，将已存在的累积分层（cumulative hierarchy）视为集合论的自然模型（[25]）。1963年，科恩（P.J.Cohen）构造了集合论的力迫模型（forcing model），并使用它证明了AC相对于ZF的独立性、GCH相对于ZF+AC的独立性（[11]，第76页）。这些模型诞生的目的是为了获得一些重要的独立性结果，我们姑且将这些模型称为集合论的经典模型。

在科恩之后，斯科特（D.Scott）、索洛韦（R.M.Solovay）、福平卡（P.Vopěnka）引入了布尔值模型（boolean-valued model），这种模型可视为力迫模型的一种重构（[3]，第18页）。随后，布尔值模型被推广到了海廷代数（heyting algebra）、格（lattice）。2015年，洛维（B.Löwe）和塔拉法德（S.Tarafder）将布尔值模型推广到了三值代数（three-valued algebra），构造了广义代数值模型（generalized algebra-valued model）（[22]）。此外，1980年，富尔曼（M.P.Fourman）将拓扑斯（topos）引入到了集合论的模型研究中，展示了如何利用拓扑斯获得一些原理的独立性证明（[13]）。这些模型可算作是技术上的创新，我们姑且称它们为集合论的非经典模型。

本文分为三部分：第一部分分析集合论的经典模型的作用，并梳理其最新动态；第二部分简要介绍集合论的非经典模型，讨论其应用前景；第三部分为基于形式不一致逻辑的弗协调ZF集合论构造具有一定普遍性的广义代数值模型。

2 集合论的经典模型

本节将按照自然模型、可构成模型、置换模型、力迫模型的顺序讨论这些经典模型，并非按照时间顺序，这样安排是出于两方面的考虑：第一，作为自然模型的累积分层出现的较早，且被广泛使用，只是“自然模型”这个名字出现的较晚；第二，置换模型和可构成模型没有紧要的联系，却和力迫模型有共通之处，它们不仅都用于获得独立性结果，而且都具有对称性质（symmetry property）。1对称性质在获取AC的独立性时十分有用，在利用对称性质为ZF构造的置换模型或力迫模型中，易使AC不成立。因为本文不涉及模型的具体构造过程，所以下文不会讨论对称性质。

2.1 自然模型

1917年，米利曼诺夫（D.Mirimanoff）使用超穷归纳构造了集合Vα的一个累积分层，其中α是任意序数，如下：

(1)V0=∅；

(2)Vα+1=Vα∪℘(Vα)，其中 ℘(Vα)是 Vα的幂集；

(3)Vα=∪[Vβ|β∈α]，其中α是任意极限序数（[6]，第219页）。

从累积分层出发，可以得到任意累积集Vα，即，对任意α有Vα；也可以得到所有累积集构成的类[Vα|α∈ON]，其中ON是所有序数的类。如果我们用V表示集合全域{x|x=x}，那么，使用ZF可以证明V=∪[Vα|α∈ON]。证明过程简述为：幂集公理用于从α得到Vα。替换公理和并公理用于为一个极限序数α构造Vα。考虑一个函数，它为每个β＜α指派集合Vβ。通过替换公理，对β＜α而言，所有Vβ的收集是一个集合，所以，并公理用于这个集合产生Vα。无穷公理用于证明ω的存在，并且也证明序数的超穷序列的存在。最后，在假定其它公理的情况下，基础公理等价于陈述：对某个序数α而言，每个集合都属于某个Vα。2特殊地，冯•诺依曼（von Neumann）证明∪[Vα|α∈ON]是ZF的一个标准模型（standard-model）（[6]，第219页）。所谓标准模型是指，集合论的语言中的谓词符号∈和=分别被解释为通常意义上的隶属关系和相等关系。

根据反射原理（reflection principle），对每个公式φ(x1,...,xn)，ZFC证明：存在一个序数α满足：Vα反射它，即，对每个a1,...,an∈Vα有：φ(a1,...,an)在V中成立，当且仅当，φ(a1,...,an)在Vα中成立。因此，存在序数α，使得Vα是ZFC的一个模型，当然也是ZF的一个模型。ZF的形如Vα的模型被称为ZF的自然模型。关于自然模型的研究主要是确定α的取值范围。

张宏裕在讨论自然模型时，给出的定理是“若K是不可及基数，则VK是ZF的模型”（[45]，第168页）。关于ZF的自然模型Vα，这个结果没有完全地描述α的取值范围。因为蒙塔古（R.Montague）和沃特（L.R.Vaught）证明了：对任意不可及基数K，存在一个序数θ＜K并非是不可及的，且累积集Vθ是ZF的传递标准模型。为了完全地描述ZF的自然模型，2007年，布尼纳（E.I.Bunina）和扎哈罗夫（V.K.Zakharov）引入了（强）公式不可及基数（(strongly)formula-inaccessible cardinal number）的概念（[6]）。下面简要介绍这个概念。

关于公式不可及基数。首先给出一些记号说明。如果一个公式φ的所有自由变元包含于变元x1,...,xm-1,p0,...,pn-1中，那么我们把它记为φ(→x,→p)。在记号φ(→x,→p)中，变元p0,...,pn-1被视作参数（parameters）。我们用→x∈A、∀→x∈A、∃→x∈A分别表示x0∈A∧...∧xm-1∈A、∀x0∈A...∀xm-1∈A、∃x0∈A...∃xm-1∈A。然后，对任意传递集A，ZF的每个公式φ(x,y;→p)定义了一个对应，即，依赖参数→p的

[φ(x,y;→p)|A]≡{z∈A∗A|∃x,y∈A(z=〈x,y〉∧φA(x,y;→p))}⊂A∗A。其中，φA(x,y;→p)表示φ(x,y;→p)在A中成立。一个序数α被称为公式正则的（formula-regular），如果

∀→p∈Vα∀β(β∈α∧([φ(x,y;→p)|Vα]⇌(β→α)⇒∪rng[φ(x,y;→p)|Vα]∈α))，

其中，[φ(x,y;→p)|Vα]⇌ (β→α)的意思是 [φ(x,y;→p)|Vα]是一个从β到α内的函数。φ是指称ZF的任意公式的元变元（metavariable），rng表示值域。一个序数α＞ω被称为（强）公式不可及的，如果

(1)∀β(β∈α⇒|℘(β)|∈α)；

(2)α是公式正则的。

如果一个序数α满足∀β(β∈α⇒|℘(β)|∈α)，那么α是一个基数。每个公式不可及序数α是一个基数。如果α是一个公式不可及基数，那么Vα被称为公式不可及累积集（formula-inaccessible cumulative sets）。

布尼纳和扎哈罗夫证明了一个定理：在ZF中，对任意集合U，下列断定等价，

(1)对某个公式不可及基数α，有U=Vα；

(2)U是ZF的一个超传递标准模型。

据此结果，ZF的所有自然模型都可以被描述。关于超传递见[6]，第222页。

2.2 可构成模型

可构成模型被用于证明AC、GCH相对ZF的一致性。可构成（constructibility）的最初想法是：令A是非空的、两两不相交集合的一个集合。A的一个选择集C是∪A的一个子集，所以C是℘(∪A)的一个元素。所以可以设想，选择公理是从并公理和幂集公理出发可证的。但是根据分离公理，我们想证明选择集的存在，需要一个ZF公式ϕ(x)。但是我们不知道如何从一般意义上获得这样一个公式，所以，给出可定义集合（definable set）的概念。

令L是一个一阶语言，令R=〈A,...〉是L上的一个关系系统，A为它的定义域。A的一个子集S被称为在R上是可定义的（definable），当且仅当，存在L的一个公式ϕ，ϕ有一个自由变元x，使得S={a|a∈A且R⊨ϕ[a]}。令Def(R)是R的所有可定义子集的集合。

可构成模型有两种：语义的和语法的。1939年，哥德尔发表了作为语义模型的可构成模型（[11]，第25页）。这种语义模型通过定义一个超穷分层（transfinite hierarchy）Mα实现。1940年，哥德尔发表了作为语法模型的可构成模型（[11]，第25页）。这种语法模型通过定义可构成集（constructible sets）的一个分层Fα实现。这里简述作为语义模型的可构成模型，而关于语法的可构成模型请参见[45]，第175页。

作为语义模型的可构成模型如下：

令M是ZF的一个标准模型，对M中的序数α，在M中定义集合的一个分层Mα如下：

•M0=∅；

•Mα+1=Def(Mα)；

•Mλ=∪{Mα|α＜λ}，如果λ是一个极限序数。

令L=∪{Mα|α∈ONM}，其中ONM是M中所有序数的类。一个集合被称为可构成的，当且仅当，它是某个Mα的元素。因为对所有α∈ONM，Mα在M中是可定义的，可得Mα是M的子集，所以有L⊆M。可证地，〈L,∈〉是ZF的一个模型。关于此模型的详情请参见（[11]，第26页）。

可构成模型被用于证明AC相对于ZF的一致性、GCH相对于ZF的一致性、GCH相对于ZF+AC的一致性。Gödel还证明了V=L在〈L,∈〉中成立，并且V=L蕴涵AC和GCH。因此，AC和GCH在〈L,∈〉中也成立，进一步地，〈L,∈〉是ZF+AC+GCH的一个模型。

可构成模型不能被用于证明AC和GCH相对于ZF的独立性。科恩于1963年证明了：如果存在ZF的传递标准模型，那么存在ZF的极小模型（minimal model）。关于极小模型，如果M是ZF的一个极小模型，那么，对ZF的任意传递标准模型M′，M′包含一个同构于M的子模型（[8]）。科恩的证明带来一个后承：对任意公式ϕ，如果我们使用可构成模型M1证明ϕ相对于ZF的一致性，那么无法构造另一个可构成模型M2用于证明ϕ相对于ZF的独立性。原因是：存在ZF的极小模型M3，使得M1和M2都包含同构于M3的子模型，而这是不可能的。因此，使用可构成模型的方法，我们无法证明AC和GCH相对于ZF的独立性。

关于可构成模型的后续发展，可分为四个方面：

一、关于可构成性公理的研究。例如，1966年，斯卡尔佩里尼（B.Scarpellini）给出了可构成性公理的最一般形式，斯卡尔佩里尼称之为弱可构成性公理（weak axiom of constructibility）。该公理的形式为：∃x(∀u∀v(u∈x∧v∈u→v∈x)∧∀y∃z(z∈ON∧y∈Ftxz))，其中ON是所有序数的类，Ftxz可以理解为x上的一个可构成集。该定理说的是：存在一个集合x，使得对任意集合y，都存在一个序数z使得y是在x上可构成的。（[28]）

二、关于可构成性公理的应用的研究，一般体现为，在新构造的模型中验证可构成性公理是否成立，以此考察新模型的表达力。例如，福平卡构造了集合论的一个超幂模型（ultrapower model），在其中证明了可构成性公理是成立的（[5]）。

三、关于可构成模型的初等模型的研究。1976年，考恩（R.H.Cowen）研究了作为语义模型的可构成模型，主要研究了可构成集Mα和它的初等子模型、初等等价模型、可定义元素构成的传递坍缩（transitive collapse）之间的关系（[9]）。

四、关于可构成模型和布尔值模型的关系的研究。1967年，福平卡和哈耶克（P.Hájek）讨论了将作为语义模型的可构成模型转换为布尔值模型的可能性（[32]）。

自20世纪70年代后期起，关于可构成性公理的研究关注的是精细结构（fine structure）和核模型（thecoremodel）。精细结构是关于可构成全域L的理论，它本质上试图说明可构成分层的增长方式（[17]）。核模型是构造集合论的全域的一个可定义的内模型的方法，它需要用到精细结构和迭代超幂（iteratedultrapowers）（[10]，第xiv页）。核模型主要用于大基数（large cardinal）的研究，方法是通过判定位于某个大基数公理下的核模型来分析该大基数公理的性质（[18]）。例如，2001年，维克斯（J.Vickers）和韦尔奇（P.D.Welch）使用核模型的方法证明：Con（ZFC+存在一个传递内模型M和一个非平凡的初等嵌入M→V）不能蕴涵Con（ZFC+存在一个可测基数（measurable cardinal）），其中Con表示一致性（[31]）。

2.3 置换模型

弗兰克尔首次在1922年引入了置换模型，因为当时关于数学和元数学的区分还不十分清晰，所以弗兰克尔没能很好地处理某些概念的绝对性。这些不足被莫斯托夫斯基观察到和纠正。弗兰克尔-莫斯托夫斯基的方法不是用于普通的集合论，而是用于带原子（atoms）的集合论。弗兰克尔-莫斯托夫斯基的方法后来被施佩克尔改进，简称为FMS方法，用于允许自反集（reflexive sets）存在的集合论。

需要说明原子和自反集。原子有时也被称为基本元素（urelements），它自身不是集合，但可以作为集合的元素。一个集合x是自反的，当且仅当，x={x}，即条件∀y(y∈x↔y=x)成立。自反集具有原子的性质，并且自反集的存在矛盾于基础公理（[15]，第6页）。因此，研究允许自反集存在的集合论，不仅涵盖了对带原子的集合论的研究，而且可以研究允许非基集（unfounded sets）存在的集合论。

从ZF中去掉基础公理后，由剩余的公理构成的集合论，即为允许自反集的集合论，记为ZF°。简单来说就是：ZF=ZF°+基础公理。

说明：给定ZF，如果我们使它允许原子，但不允许自反集，那么得到的集合论记为ZFA。在ZFA中，基础公理仍然是有效的，且使用置换模型可以获得AC相对于ZFA的独立性。给定ZF，如果我们使它允许自反集，那么必须去掉基础公理。在这样的情况下使用置换模型，获得的独立性结果都是相对于ZF°的。关于前者的实例可参见[3]（第3页），关于后者的实例请参见[11]（第57–74页）。

这里不再介绍置换模型的一般构造过程，原因是：作为获得独立性结果的工具，置换模型要么不能用于纯集合构成的集合论，要么不能用于包含基础公理的集合论，相比之下，在置换模型之后出现的力迫模型，不但继承了置换模型的优点，即对称性，而且还克服了置换模型的不足，应用范围十分广泛。如果读者对置换模型的构造过程有兴趣，请参见[11]（第46–57页）。

置换模型的作用。置换模型被用来获得一些公理相对于ZF°的独立性，主要包括：基础公理相对于ZF°的独立性；AC相对于ZF°的独立性；GCH相对于AH的独立性；AC相对于库雷巴（Kurepa）的反链原理（anti-chain principle）的独立性。该反链原理是说：每个偏序集〈s,≤〉都有一个极大反链。借助于置换模型，我们还可以获得基数在ZF°中的不可定义性。定义一个集合x的基数|x|，要么借助AC，要么借助基础公理，在既没有AC也没有基础公理的情况下，我们无法定义x的基数|x|。因此，基数在ZF°中是不可定义的。莱维（A.Lévy）和甘特（R.J.Gautt）分别独立地获得了这个结果（[11]，第68页）。

2.4 力迫模型

第一个力迫模型由科恩于1963年构造。力迫模型是一种扩张模型，即，构造力迫模型的过程就是构造某个给定模型的扩张模型。在力迫模型出现之前，当通过向ZF的模型M伴随新的集合a0,a1,...对M进行扩张时，面临的主要困难是，集合ai自身的结构会带来一些麻烦，例如，ai的内部∈结构会摧毁替换公理。力迫模型的出现克服了这个困难。在力迫模型中，使用力迫关系约束ai的性质，使之必须遵守M中形成的某些条件，通过该方式，使得ai不能带来我们不期望的麻烦。这些被伴随到M的集合ai被称为“兼纳集”（generic sets）3关于generic sets的翻译。数学词典上译为泛集，[45]译为脱殊集，[37]译为兼纳集，本文采用“兼纳集”这个译法。。如果通过力迫关系约束ai的条件为有穷条件，那么这些ai被称为在M上科恩兼纳的（Cohen-generic）。使用“科恩兼纳”这个名字是为了纪念第一个发明有穷力迫的科恩。带实线的完美闭子集的力迫被称为萨克斯（Sacks）力迫，对应的兼纳集被称为萨克斯兼纳。带博雷尔（Borel）集的力迫被称为索洛韦力迫，对应的兼纳集被称为索洛韦兼纳。（[11]）

关于力迫模型，国内逻辑学界研究的较多，这里不再赘述。关于力迫模型的一个简述请参见（[37]）。关于力迫模型的详情请参见[11]（第78–96页），关于力迫和布尔值模型的结合的介绍请参见（[45]，第229–243页），其中，该模型的名字叫脱殊模型。

下面介绍力迫模型的作用。

力迫模型被用于获得一些独立性结果。科恩证明了AC相对于ZF的独立性，即，如果ZF是一致的，那么ZF+AC是不一致的。方法是：ZF+AC⊢一个集合x是有穷的，当且仅当，它是戴德金有穷的。科恩在他构造的兼纳扩张N中，发现了一个集合既是无穷的又是戴德金有穷的，因此，ZF+AC是不一致的。因为GCH蕴涵AC，所以GCH相对于ZF也是独立的，即，如果ZF是一致的，那么ZF+GCH是不一致的。科恩还证明了，如果ZF是一致的，那么ZF+AC+¬CH是一致的。因此，CH相对于ZF+AC是不一致的，因为GCH蕴涵CH，所以GCH相对于ZF+AC也是不一致的。这就获得了GCH相对于AC的独立性。以类似的方式，科恩还证明了可构成性公理V=L相对于ZF+AC+GCH的独立性。

下面列举一些其它的独立性结果。（[11]）

BPI相对于序原理的独立性。BPI是布尔素理想定理，说的是：每个布尔代数有一个素理想。序原理OP为：每个集合x都能被全序。序扩张原理OE为：如果x是一个集合，且r是x上的一个偏序，那么存在一个线序t使得r⊆t。在力迫模型出现之前已有ZF⊢AC→BPI→OE→OP。马赛厄斯（A.R.D.Mathias）证明了：如果M是ZF+V=L的一个可数标准模型，那么M能被扩张成为ZF+OP+¬OE的一个可数标准模型N。因此，OE在ZF中独立于OP，BPI也在ZF中独立于OP。

哈尔彭（J.D.Halpern）和莱维构造了模型M的一个兼纳扩张M[a0,a1,...,A]，该扩张是ZF+BPI+¬AC的一个模型。因此，他们也证明了：如果ZF是一致的，那么AC在ZF中相对于BPI是独立的。

相关选择公理（axiom of dependent choices）是说：令R是集合x上的一个二元关系，使得(∀y∈x)(∃z∈x)(〈y,z〉∈R)，那么存在x的元素的一个可数序列y0,y1,...,yn,...(n∈ω)使得：对所有n∈ω有〈yn,yn+1〉∈R。莫斯托夫斯基在1948年构造了一个置换模型，证明了，在ZF°中，AC相对于相关选择公理的独立性。后来，马雷克（W.Marek）将莫斯托夫斯基的置换模型翻译为一个力迫模型，证明了，在ZF中，AC相对于相关选择公理的独立性。

利用力迫模型获得的更多的独立性结果请参见[43]。

3 集合论的非经典模型

拓扑斯作为一种技术的创新，能对置换模型、力迫模型、布尔值模型进行重构。因此，本节先介绍布尔值模型和布尔值模型的推广，后介绍拓扑斯。

3.1 布尔值模型

使用布尔值模型描述力迫模型的思想最早由索洛韦在1965年提出，他使用博雷尔集作为力迫条件构造模型，并声称：力迫某个陈述的条件的组合是该陈述的‘值’。福平卡独立地发现了和索洛韦相同的观点，只是福平卡最初的呈现很简洁，所以没有引起很大关注。这两条记录来自（[1]，第xv–xvi页）。（[11]，第77页）记录道：斯科特、索洛韦和福平卡发现能把力迫理解为句子的一个布尔赋值。但费尔格纳（U.Felgner）的根据是斯科特在1967年的课堂笔记，在该笔记中，斯科特证明休恩菲尔德（J.R.Shoenfield）构造力迫模型的方法是布尔值模型的方法。斯科特、索洛韦、休恩菲尔德等人都是在讨论会上讨论使用布尔值模型描述力迫模型，很多结果都没有发表，只有贝尔（J.L.Bell）整理的笔记。因此，现在通常认为是斯科特、索洛韦、福平卡三人引入了布尔值模型。

布尔值模型的作用和力迫模型的作用是一样的，正如（[1]，第xvi页）所说：“力迫和布尔值模型是相同的东西……从心理上讲，布尔值模型更加自然，但是，当面对具体的模型（和恰当模型的构造）时，常常不得不更加靠近力迫条件”。

关于布尔值模型的详细构造过程，参见[1,45]。这里只简述一下，便于介绍广义布尔值模型。布尔值模型的构造可分为三步：第一，将集合论的自然模型中的每个集合替换为它们的特征函数，这些特征函数的值域是布尔代数2；第二，用任意完全布尔代数替换布尔代数2作为特征函数的值域；第三，证明第二步中获得的特征函数的类（也被称为布尔值全域）是集合论的模型，该模型即为布尔值模型。

布尔值模型的推广。该推广有两个方向：第一个方向是将布尔值模型由ZF推广到其它公理化集合论或逻辑，例如，李娜教授分别将布尔值模型推广到冯•诺依曼-贝奈斯-哥德尔集合论（vonNeumann-Bernays-Gödelaxiomaticclass-settheory，即NBG）（[35]）、聚合公理系统COG（[36]）、道义逻辑D（[39]）、含有原子的集合论（[40]）、模态命题逻辑（K、D、T、S1、S2、S3）（[38,42]）；第二个方向，是将布尔值模型推广到海廷代数、格、三值代数。关于第二个方向的推广将在下一节中说明。

3.2 从布尔值模型到广义代数值模型

格+一些限制条件=海廷代数；海廷代数+另一些限制条件=布尔代数。利用完全布尔代数构造ZFC的布尔值模型，可以证明连续统假设相对于ZFC的独立性。一种自然的想法是：用海廷代数替换布尔代数构造模型会怎么样？用格替换布尔代数构造模型会怎么样？用海廷代数H替换布尔代数B构造的VH是直觉主义集合论（intuitionistic ZF）的一个模型；用恰当的格替换布尔代数可以得到量子集合论（quantum set theory）或模糊集合论（fuzzy set theory）的模型，例如，[47]和[46]使用格构造了模糊集合论的模型4[47]和[46]将“fuzzy”译为“弗晰”，在本文中译为“模糊”。。[22]用合理蕴涵代数（reasonable implication algebras）（这是一个三值代数）替换布尔代数，得到ZF的广义代数值模型。下面按直觉主义集合论的模型、量子集合论的模型、广义代数值模型的顺序介绍此推广过程。

1973年，迈希尔（J.Myhill）构造了基于直觉主义逻辑的集合论系统IZF，即直觉主义ZF；和ZFC相比，因为直觉主义逻辑拒绝排中律，又因为选择公理和基础公理蕴涵排中律，所以IZF舍弃了选择公理和基础公理（[26]）。在使用同一语言的情况下，从形式上看，IZF和ZF有相同的外延公理、对公理、并公理、分离公理、无穷公理和幂公理；不同的是，IZF使用集合归纳公理模式（axiom schema of set induction）代替基础公理。此外，迈希尔使用收集公理模式（axiom schema of collection）代替替换公理模式，这样的行为带来的一个结果是：有两个直觉主义ZF，使用替换公理模式的IZF1和使用收集公理模式的IZF2，IZF2的表达力比IZF1强（[16]）。集合归纳公理模式（简称Ind）和收集公理模式（简称Coll）的形式如下：

(Ind)∀x[∀y∈xϕ(y)→ϕ(x)]→∀xϕ(x)；

(Coll)∀y∈x∃zϕ→∃w∀y∈x∃z∈wϕ（[16]）。

在假定排中律的情况下，Ind等价于基础公理，Coll等价于替换公理。1979年，格雷森（R.J.Grayson）使用海廷代数构造了IZF的海廷值模型（[16]）。IZF的海廷值模型的构造过程和上节中的布尔值模型的构造过程类似，只不过把完全布尔代数换成完全海廷代数，这里不再赘述。

1936年，伯克霍夫（G.Birkhoff）和冯•诺依曼引入了量子逻辑（quantum logic）（[2]）。量子逻辑与经典逻辑不同，它不同于经典逻辑的公理系统，它只是量子物理理论的一种逻辑结构，可被视为一个希尔伯特空间（Hilbert space）的所有封闭线性子空间（closed linear subspaces）的格。因为量子逻辑是格，所以，基于量子逻辑构造量子集合论（quantum set theory）的工作，实际上是使用量子逻辑构造集合的格值全域。构造格值全域的过程类似于布尔值全域的构造过程，这项工作于1981年由竹内外史（G.Takeuti）完成，详情参见（[29]），类似的工作还有（[30]）。2009年，小泽正直（M.Ozawa）为量子集合论构造了格值模型（[27]）。小泽正直的工作实际上是将竹内外史的格值全域推广到正交模格（orthomodular lattice），即，使用正交模格代替竹内外史使用的量子逻辑构造格值全域。

[22]构造ZF的广义代数值模型的基本思路是：第一，给出蕴涵代数的定义，蕴涵代数是一种否定自由代数（即不包含否定运算的代数），且讨论了蕴涵代数的两个性质，即合理性和蕴涵性，并给出蕴涵代数的一个例子PS3，PS3是合理的且演绎的；第二，介绍如何构造模型VA，其中A是蕴涵代数，如果A是合理的且演绎的，那么除基础公理外，ZF的其它公理或公理模式在VA中有效；第三，使用PS3构造模型VPS3，基础公理在VPS3中是有效的，可证地，VPS3是ZF的模型（关于该模型的详情请参见[22]）。

3.3 拓扑斯

拓扑斯在逻辑中的应用分为两个方面：一方面，拓扑斯与逻辑中的“理论”对应，拓扑斯可以在逻辑中被形式化为（带完全概括公理的）直觉主义类型论（intuitionistic type theory（with the full comprehension axiom））；另一方面，拓扑斯可以为集合论提供模型。本文不介绍拓扑斯的定义，关于拓扑斯的定义请参见（[44]）和（[1]，第175页）。下面将根据这两个方面来介绍拓扑斯在逻辑中的应用。

[12]（第1054页）引用了劳威尔（F.W.Lawvere）的一句话——“以对象范畴形式呈现的拓扑斯概括了‘高阶逻辑’的本质”。在这篇文章中，富尔曼在拓扑斯和逻辑理论之间建立了一种对应，并将这种对应形式化。和其它人所做的形式化相比，富尔曼的形式化引入了一个新的存在谓词（existence predicate），这使得我们能以通常的方式在拓扑斯中使用变元。（[19]）是关于逻辑和范畴论的关系的一篇清晰且简洁的调查。富尔曼希望自己所呈现的拓扑斯对于逻辑学家来说是可及的，他希望逻辑学家能更多地利用由格罗滕迪克（Grothendieck）和他的合作者所提供的模型，而这也正是下面将要介绍的。

拓扑斯为集合论提供模型，并非像经典模型一样能被用于获取新的结果，而只是作为一种技术上的创新对已有的集合论模型进行重构。到目前为止，我们可将这种重构的过程分为四个阶段。第一个阶段，劳威尔提出了范畴论公理化的集合论（category-theoretic axiomatizations of set theory），[24]研究了它和传统公理化集合论在模型方面的异同。第二个阶段，拓扑斯能够统一地处理置换模型、力迫模型、布尔值模型、模型的对称性，详情参见[13]、[14]和[3]。第三个阶段，布尔值模型⇔完全拓扑斯。对允许原子的每个布尔值模型，都存在一个表示它的最小完全拓扑斯，最小完全拓扑斯是一个格罗滕迪克拓扑斯，并且，在这个布尔值模型中，该最小完全拓扑斯能被描述；反之，每个允许原子的布尔值模型都能从表示它的最小完全拓扑斯中被重构（详情参见[4]）。第四个阶段，[23]给出了直觉主义集合论的范畴模型的一个非常一般的构成。

拓扑斯概念的引入，使得我们有一种新的技术构造集合论的模型，这不仅体现在为ZF构造模型，更进一步地，我们能使用拓扑斯为基于非经典逻辑的集合论提供模型。与此同时，拓扑斯对已有模型的重构，也为我们提供了一个新的角度去考察已有的模型，从而发现它们之间的潜在联系。

4 弗协调集合论的模型

梳理经典集合论的模型只是一个出发点，我们的落脚点是为弗协调集合论构造模型。在本节，我们讨论如何构造弗协调集合论的广义代数值模型，并说明我们的模型适用于目前所有基于形式不一致逻辑的弗协调ZF集合论。

4.1 弗协调集合论

弗协调集合论是基于弗协调逻辑构造的集合论，换言之，是将公理化集合论的底层逻辑替换为弗协调逻辑。基于不同的弗协调逻辑，我们可以构造不同的弗协调集合论。目前已有的弗协调集合论基于三种弗协调逻辑：形式不一致逻辑（logics of formal inconsistency）、相干逻辑、多值逻辑。基于形式不一致逻辑的弗协调集合论包括科斯塔（N.C.A.da Costa）的ZFn系统、卡埃罗（R.da C.Caiero）和苏萨（E.G.de Souza）的ML1系统、卡尔涅利（W.Carnielli）和科尼利奥（M.E.Coniglio）的ZFCil系统，其中，ML1系统是基于蒯因（Quine）的NF集合论构造的，ZFn系统是基于丘奇（A.Church）的CHU系统构造的，ZFCil系统是基于ZF集合论构造的。关于弗协调逻辑和弗协调集合论的介绍参见（[41]）。

形式不一致逻辑的特征是，通过弱化否定使得‘{¬A,A}⊨B’不成立，其中，⊨既指语法后承也指语义后承；典型系统是科斯塔的C系统，关于C系统的详细介绍参见[48]（第1–50页）。这导致在形式不一致逻辑中通常有两种否定：一种是弱否定¬，这种弱否定是初始符号；另一种是强否定～，这种否定通常是被定义符号，从语法形式上看，强否定等价于经典逻辑中的否定。通常情况下，形式不一致逻辑包含经典逻辑，即，如果把经典逻辑的否定等同于强否定，那么经典逻辑的定理都是形式不一致逻辑的定理。在形式不一致逻辑中，任意形如(φ∧¬φ)的矛盾式都不是定理，这说明：形式不一致逻辑自身不包含矛盾，但在形式不一致逻辑中，我们可以把矛盾作为前提来研究它的后承。

从形式不一致逻辑出发构造弗协调ZF时，一个核心的问题是集合公理（关于集合的公理，下同）应该使用哪种否定。在ZF的集合公理中，使用否定的只有空集公理和基础公理。如果空集公理使用的是强否定，那么产生的空集和经典集合论中的空集相同，是真的“空”，即，没有元素隶属于该空集；如果空集公理使用的是弱否定，那么产生的空集不是真的“空”，即，可能有元素隶属于该空集。如果基础公理使用的是强否定，那么它能保证弗协调ZF中的集合都是良基的，即，没有循环集；如果基础公理使用的是弱否定，那么它不能保证弗协调ZF中的集合都是良基的，即，可能存在循环集，例如{x|x∈x}。这些情形都会影响到模型的构造。

如果一个集合x满足x∈x或者x̸=x，那么它不是一致的，其中，̸=使用的否定是弱否定。ZF中的集合都是一致的。在一个基于形式不一致逻辑的弗协调ZF中，如果集合公理使用的都是强否定，那么在该集合论中不存在不是一致的集合，这是因为：集合论中的集合要么由空集出发使用对、并、无穷、幂运算得到，要么从已有集合出发借助某个定理从分离公理或替换公理得到；使用强否定的空集是一致的，从一致集合出发使用对、并、无穷、幂运算生成的集合也是一致的；任意矛盾式都不是形式不一致逻辑的定理，这使得我们无法从一致集合出发使用矛盾式获得不是一致的集合。

科斯塔的ZFn系统的集合公理使用的是强否定，尽管科斯塔声称在ZFn系统中存在全域集，但是，全域集的存在不是弗协调逻辑的功劳，而是因为ZFn系统的集合公理是丘奇的CHU系统的集合公理，CHU自身就带有全域集；如果我们将ZFn系统的集合公理替换为标准ZF的集合公理，那么ZFn系统中的集合都是一致的。此后，当我们提及ZFn系统，指的是它的集合公理是标准ZF的集合公理。卡尔涅利和科尼利奥的ZFCil系统的集合公理使用的也是强否定，不同的是，和ZF相比，ZFCil多了一个反外延公理，该公理的形式为∀x∀y(x̸=y↔(∃z(z∈x∧z/∈y)∨∃z(z/∈x∧z∈y)))，该公理中的否定为弱否定，但是，该公理是一个双向条件式，借助它并不能生成新集合。因此，上述所有基于形式不一致逻辑的弗协调ZF的集合都是一致的。

4.2 广义代数值模型的推广

到目前为止，关于弗协调集合论的模型，典型的成果是李伯特（T.Libert）为基于pac的弗协调朴素集合论构造的一种拓扑模型，详情参见（[20,21]）。这个领域的研究单薄，正如卡尔涅利和科尼利奥在2013年构造ZFCil系统时所说的那样：“关于这个问题，我们只能谈一些初步的想法，并且意识到存在大量的工作要做，在这里，我们只是触及了这个问题的表面”（[7]）。2015年，洛维和塔拉法德为ZF构造广义代数值模型时，曾设想他们的技术可以为不包含罗素集的弗协调集合论提供模型（[22]）。我们在此处的工作是为了实现他们的设想，为基于形式不一致逻辑的弗协调ZF构造广义代数值模型。

我们在4.1中花费大量的篇幅说明ZFn系统和ZFCil系统不包含不是一致的集合，这是为了契合广义代数值模型的特点。广义代数值模型是布尔值模型的推广，是使用广义代数替换布尔代数构造的模型；但它们的基本结构是一样的，即从空集出发借助超穷递归构造的一个分层结构。这个结构本身是良基的，在其中不存在循环集，这就要求弗协调集合论不应当包含满足x∈x的集合。广义代数值模型使用的广义代数对于集合是没有限制的，因为在布尔值模型和布尔值模型的推广中，布尔代数和其它的代数都只服务于逻辑联结词的解释，对于谓词的解释没有影响；因此，使用广义代数替换布尔代数并不会改变模型的基本结构。

为弗协调ZF构造广义代数值模型的关键是定义广义代数。广义代数是添加了算子的完全有界格。完全有界格形如〈A,∧,∨,0,1〉；广义代数形如〈A,∧,∨,0,1,∗〉，其中，∗表示添加的算子；关于完全有界格参见（[1]，第2页）。我们需要观察弗协调ZF使用的弗协调逻辑有几个初始逻辑联结词，初始逻辑联结词的数目就是被添加的算子的数目。ZFn系统有四个初始逻辑联结词，分别是否定¬、蕴涵→、合取∧、析取∨；ZFCil系统有五个初始逻辑联结词，分别是否定¬、蕴涵→、合取∧、析取∨、一致性◦。在经典集合论的布尔值模型中，我们将合取和析取分别解释为布尔代数中的交运算和并运算，即完全有界格〈A,∧,∨,0,1〉中的∧和∨；但是，在弗协调ZF的情形中，这不一定行得通，因为弗协调逻辑的合取和析取的真值函数不一定符合完全有界格的交运算和并运算。这就是为什么我们要根据弗协调逻辑的初始逻辑联结词的数目向广义代数中添加相等数目的算子。

在形式不一致逻辑中，对任意句子φ，它的真假和它的否定¬φ的真假是相互独立的，遵循一个句子和它的否定可以同真但不能同假的原则，可能有三种情形：φ真且¬φ假；φ真且¬φ真；φ假且¬φ真。因此，我们需要的广义代数的偏序集中至少要有三个元素，不妨记为1、i、0，分别对应于句子φ的真假的三种情形。因此，我们得到否定的真值表。

形式不一致逻辑只是弱化了否定，并没有修改其它的逻辑联结词，因此，关于蕴涵→、合取∧、析取∨，它们的真值表仍然遵循经典逻辑中的一些原则：关于蕴涵，一个蕴涵式为真，当且仅当，前件为假或者后件为真；关于合取式，一个合取式为真，当且仅当，它的两个合取肢都为真；关于析取式，一个析取式为真，当且仅当，它有一个析取肢为真。它们的真值表如下。

容易看出，当我们从这三个真值表中删除与i有关的行和列之后，剩余部分恰是经典逻辑的蕴涵、合取、析取的真值表。至此，一个可能的问题是：为什么→和∨的真值表的值中有i而∧的真值表的值中只有0和1？在形式不一致逻辑中，弱否定是一个内涵联结词，作为真值函数，它是一个内涵算子，这使得φ和¬φ的真假是相互独立的，即使我们知道φ是真的，也不能确定¬φ是真是假；因此，即使知道φ是真的，也不能确定φ的真值是1还是i。因此，关于蕴涵、合取、析取，在它们的真值表中与i有关的行和列中，我们只能确定φ是真是假，当φ为真时，我们不能确定φ的真值是1还是i，可以任意指定1和i；因为蕴涵、合取、析取都是初始联结词，所以，任意指定1和i不会在它们之间产生干扰。因此，在合取的真值表中，我们将合取式为真的情形全部指定为1。我们是故意这么做的，原因将在下文中说明。注意，本段中所说的真和假分别指的是模型有效和模型无效。

ZFCil系统中还有一个初始联结词◦，它表示一致性，即：当φ真¬φ假或者φ假¬φ真时，◦φ为真；当φ真¬φ真时，◦φ为假。因此，◦的真值表如下。

注意，本段中所说的真和假分别指的是模型有效和模型无效。至此，我们给出了ZFn系统和ZFCil系统的初始联结词的真值表。下面我们定义广义代数。

我们需要的广义代数形如〈A,∧,∨,0,1,¬A,→A,∧A,∨A,◦A〉，其中，¬A、→A、∧A、∨A、◦A是我们添加到完全有界格中的算子，它们将在赋值函数中用来解释否定、蕴涵、合取、析取、一致性。关于这个广义代数，A是一个偏序集，它是集合{0,i,1}，它的序为0≤i≤1，∧和∨分别是格上的交运算和并运算，0和1分别是它的底元素和顶元素，¬A、→A、∧A、∨A、◦A的运算规则分别对应于上面给出的否定、蕴涵、合取、析取、一致性的真值表。至此，我们完成了对广义代数的定义。有了广义代数，我们可以构造出模型的全域VL，构造方法和构造布尔值全域的方法相同，其中，L=〈A,∧,∨,0,1,¬A,→A,∧A,∨A,◦A〉。类似于布尔值全域的情形，在全域VL中，我们可以使用广义归纳法。下面定义赋值函数。

我们使用符号〚·〛表示赋值函数，其中，·是一个占位符，没有意义；因此，对任意句子φ，〚φ〛是它的真值。关于原子公式，除了形如x∈y和x=y的原子公式之外，ZFCil系统还引入了两个新的谓词，零元谓词⊥和一元谓词C，C(x)表示集合x是一致的。我们使用x、y、u、v表示全域VL中的任意元素，使用φ和ψ表示任意公式，给出公式的赋值函数如下：

说明：我们这里给出的赋值函数和ZF情形中的赋值函数有两点不同：第一，关于 〚x∈y〛，在 ZF 的情形中，〚x∈y〛=(∨u∈dom(y)(y(u)∧〚u=x〛))，而在这里，我们使用算子∧A对(∨u∈dom(y)(y(u)∧〚u=x〛))施加了一次自反运算；第二，关于〚φ∧ψ〛和〚φ∨ψ〛，在ZF在情形中，∧和∨分别被解释为广义代数中的交运算∧和并运算∨，而在这里，我们将它们分别解释为算子∧A和∨A。至此，我们给出了模型中的赋值函数。下面定义模型有效性。

关于模型有效性，我们只需要给出真值的指定集就可以了。根据广义代数值模型的构造规则，真值的指定集必须是偏序集A的一个滤子。我们给出的真值的指定集是{i,1}，它是偏序集A的滤子；因此，对任意公式φ，φ是模型有效的，当且仅当，〚φ〛∈{i,1}。

至此，我们定义了广义代数L，定义了全域VL，定义了赋值函数，定义了模型有效性。使用我们给出的这些材料，遵循洛维和塔拉法德为ZF构造广义代数值模型的步骤顺序，弗协调ZF的广义代数值模型能够被构造出来。

4.3 一些说明

为弗协调集合论构造模型时，相等关系=是比较难处理的，在弗协调一阶逻辑中，一般要求相等关系=满足自反性（即x=x）和代入自由（也叫莱布尼兹公理，即(x=y)→(φ(x)↔φ(y)))。在经典逻辑的情形中，这些要求很容易被满足，因为经典逻辑的联结词都是外延的；然而，在形式不一致逻辑中，逻辑联结词否定¬是内涵的，这使得在否定¬的辖域中不能进行等值替换，因而不能满足代入自由。但是，我们发现，当〚x=y〛=1时，满足代入自由，当〚x=y〛=i时，不满足代入自由，因此，这就迫使我们的广义代数值模型必须满足：对全域VL中的任意元素x都有〚x=x〛=1。为了满足这个要求，我们令初始逻辑联结词∧的真值表中不包含i，只包含0和1；同时，我们定义的原子公式x∈y的赋值函数也与经典逻辑的情形不同，借助了算子∧A。经过这样的修改，原子公式x∈y的真值〚x∈y〛只能是0或1；进而，因为〚x=y〛是借助∈而定义的，所以，〚x=y〛也只能是0或1；在这种情形下，相等关系=的自反性和代入自由就被满足了。

在洛维和塔拉法德为ZF构造的广义代数值模型中，他们使用的广义代数满足合理性和演绎性，这两个性质极大地方便了ZF的公理的模型有效性证明；然而，在我们为弗协调ZF构造的广义代数值模型中，我们定义的广义代数不满足合理性，这增加了公理的模型有效性证明的复杂程度，一种比较原始的方法是：像使用真值表证明逻辑定理的有效性一样，依次验证弗协调ZF的每个公理是模型有效的。

我们的方法还可适用于将来可能出现的弗协调ZF集合论，要求是：这些集合论不能承诺那些不是一致的集合的存在，即不能包含像{x|x∈x}或{x|x̸=x}这样的集合；这个要求也恰恰体现了广义代数值模型的局限性，即，它不能为弗协调朴素集合论提供模型。对于弗协调ZF集合论，不管它们的底层逻辑是何种形式的形式不一致逻辑，通过调整蕴涵、合取、析取的真值表中与i有关的行和列中的值，我们都可以构造出适应这些集合论的模型。

5 结语

我们梳理了近百年以来人们为经典集合论构造的各种重要模型，目的是为了寻找合适的模型构造技术为基于哲学逻辑的集合论构造模型；特殊地，为弗协调集合论构造模型。我们根据洛维和塔拉法德为ZF构造的广义代数值模型的思路，为基于形式不一致逻辑的弗协调ZF构造了广义代数值模型，并指出我们的广义代数值模型具有一定的普遍性。

经典集合论的模型大多被用于研究某些公设（例如AC和GCH）相对于经典集合论的一致性或独立性；相比之下，弗协调集合论的情形则不同，弗协调集合论的模型主要用于证明弗协调集合论的非平凡性，即，在弗协调集合论的语言中，存在某个句子φ使得φ是模型无效的。AC和GCH的独立性和一致性在弗协调集合论的情形中不一定是个问题，例如，从2010年到2012年，韦伯（Z.Weber）构造了一个弗协调朴素集合论，并证明了：AC是该集合论的一条定理，GCH在该集合论中是不成立的（即，可证伪的）（[33,34]）。但是，韦伯的弗协调朴素集合论缺乏模型。

广义代数值模型有它的局限性，它不能为承诺了不一致集合的弗协调集合论提供模型，例如弗协调朴素集合论。2003年到2005年，李伯特使用拓扑为基于pac的弗协调朴素集合论构造了模型，他的模型包含不是一致的集合。在未来的工作中，我们将致力于借助拓扑斯为弗协调集合论、模态集合论、弗协调模态集合论构造模型。