哥德尔在（Gödel，1938）发表了选择公理（axiom of choice）和广义连续统假设（generalized continuum hypothesis）的相对一致性结果。

选择公理就是ZFC公理系统中的“C”，又记作AC。它可以表述为：任意一个由两两不交的非空集合组成的集合族都有一个选择集从其中每个集合中选出一个元素。用集合论形式语言来表达可以写作

策梅洛在（Zermelo，1904）中宣称证明了康托尔良序定理（well-ordering theorem）猜想。^[9]他在证明中本质上使用了上述选择公理，并因此而受到许多质疑，以至于他不得不在（Zermelo，1908）中以接近上述方式明确陈述了选择公理并重新证明了良序定理。值得注意的是，在这篇文章的第二部分，策梅洛花了远多于证明部分的篇幅来为选择公理和他对良序定理的证明辩护。策梅洛甚至在哥德尔的工作之前就明确意识到选择公理是“逻辑地独立于其他【公理】的”，而“即使在数学中，不可证……绝不等价于不有效”。因此，他为选择公理所做的辩护只能是非数学的。

策梅洛为选择公理所做的辩护主要基于两个方面：（1）选择公理在数学实践中业已取得的成功和不可或缺性；（2）选择公理不会造成矛盾。策梅洛列举了他那个时代已经依赖选择公理得到的数学结果，尤其是康托尔基数理论。没有选择公理，我们甚至难以证明一个集合的划分（它的一些两两不交的子集组成的集合）的基数总是小于等于原集合。不知道哥德尔在（Gödel，1964）中阐述的基于公理候选的“成功”的外在性辩护是不是受到策梅洛为选择公理辩护的影响。此外，策梅洛宣称，从选择公理通过任何已知的方法都不会得出悖论。但是，策梅洛所做的说明也仅仅能让人“希望明确地切断了任何引入ON的可能性”（Zermelo，1908，p. 192，楷体由笔者添加，原文中ON记作W^[10]）。

然而，策梅洛并未给出对选择公理的内在性辩护。现代对选择公理的主要质疑是它的非构造性。集合论公理中大多数存在性公理都是在下述意义上构造的。无论是对集公理（axiom of pairs）、并集公理（axiom of union）、分离公理（separation schema），甚至幂集公理（axiom of power）、无穷公理所断言存在的集合都是在集合论宇宙中（以已有集合为参数）可定义的，而选择公理所断言存在的选择集却外延不明。

策梅洛对选择公理辩护的这些弱点在哥德尔关于可构成集宇宙L的构造中得到了补强。哥德尔的构造不仅严格证明了选择公理相对其他集合论公理的一致性，甚至给出了一种可能：存在一个明确的方法让我们对每一个满足条件的集合族都能唯一确定地找到它的选择集。当然，这过于乐观的情况也令人怀疑，并以此作为反对V=L的理由之一。

选择公理使康托尔的基数理论得以可能。特别地，对每个基数为κ的集合X，它的幂集P（X）有一个确定的基数（记作2κ），并且κ＜2κ。^[11]康托尔猜想连续统（实数集）的基数2ℵ0就是第二个无穷基数ℵ1，这就是连续统假设（记作CH）。广义连续统假设（记作GCH）是对CH的推广：对任意无穷基数κ，2κ=κ+（κ的下一个无穷基数）。在哥德尔的可构成集宇宙L中，广义连续统假设成立。

与通过冯·诺伊曼层谱定义WF类似（见第102页），我们也是通过在序数上的递归逐层地得到越来越丰富的可构成集。

定义　3.9（可构成集）　定义序数上的映射α→Lα如下：

(1) L0=dfØ；

(2) Lβ+1=dfD(Lβ)；

（3）若α是极限序数，Lα=df∪β＜αLβ。

定义可构成集类L=∪α∈ONLα。

这里与冯·诺伊曼层谱定义唯一不同的是子句（2）中以算子D取代了冯·诺伊曼层谱中的集合幂运算P。对任意集合A，它的幂P（A）指所有A的子集组成的集合，而D（A）可以被非形式地定义为由所有在结构（A，∈）中以A中元素为参数可定义的A的子集组成的集合，也即所有在结构（A，∈，a）a∈A中可定义的A的子集组成的集合。

参数可定义的子集

我们可以严格地定义：

注意，M=D（A）是一个以ω为参数的Δ0的集合论公式（所含量词都是有界量词）。直观上，它是否成立只涉及A，M和ω中是否含有这样或那样的集合，是一个局部性质。这样的性质，在局部含有相同的A，M集合的不同集合论宇宙间具有相同的语义。我们称这种局部的性质在上述不同集合论宇宙间是绝对的。

D运算是Lα递归定义中的核心步骤。我们宣称一个集合x=Lα，需要给出一个关于Lα的构造序列。这是一个涉及整个集合论宇宙中是否存在具有某种性质的集合（Lα的构造序列）的判断，而关于一个集合是否具有那种性质的判断是局部的，因此整个判断可以表述为一则Σ1公式（有形式∃xφ（x），其中φ（x）是Δ0的）。另一方面，我们也能通过证明所有满足条件的构造序列均指向x=Lα来证明后者。而“所有集合”都具有某种局部性质则是一则Π1公式。事实上，我们可以在ZF的一个很弱的有穷部分中证明x=Lα既等价于一个Σ1公式，也等价于一个Π1公式。我们称这种性质是（在ZF的那个有穷部分看来）Δ1的。这种Δ1性质，在满足ZF的那些有穷部分和有关封闭性的集合论宇宙间也具有相同的语义，或称绝对的。

显然，总有D（A）⊂P（A）。在ZF中也不难证明，α⊂Lα⊂Vα，因而ON⊂L⊂V。也不难验证，L是传递的，即对任意x∈L，有x⊂L。我们还可以证明ZF在L下成立，或记作ZFL。或者更准确地说，对任意σ∈ZF，ZF ⊢σL，而这本身是中可证的。我们称这些包含所有序数ON、传递且满足ZF的类为集合论的内模型（inner model）。

对任意α∈ON，Lα∈Lα+1⊂L。可以证明，在L中和V中对每个Lα的解释都是一样的，即=Lα。由此可以证明，V=L在L中成立。事实上，对任何集合论的内模型M来说，Lα都是绝对的，由此可以证明每个集合论内模型M中的那个可构成集类LM=L。因此，L包含在每个集合论内模型中，也就是最小的内模型。

根据L的定义，我们可以自然地构造一个关于整个可构成集宇宙的全局的良序。由于每个L中的元素x最初总是在某个后继层中被构造出来的，例如x∈Lα+1\ Lα，此时，我们可以把α作为x在L的一个秩，记作rankL（x）=α。由此，我们可以将可构成集做一个大致的排列：如果rankL（x）＜rankL（y），我们就认为x排在y之前。接下来，我们可以递归地定义具有相同的秩的集合之间如何排列。

假设rankLx=rankLy=α，也即x，y∈Lα+1\Lα都是在Lα中首次被定义出来的。我们可以将所有集合论公式排成一个序列{φ0，φ，...}。^[12]假设定义x，y的公式不同，那么按照上述排序，总有一个集合的（排在最前的）定义公式比另一个的（排在最前的）定义公式排得更前。不妨设φi是定义x的排在最前的公式，而φj是定义y的排在最前的公式，且i＜j。此时，我们就称x排在y之前。当然，也有可能定义x，y的排在最前的公式是一样的，只是援引了不同的参数。根据归纳，我们可以假设已有对Lα中元素的排序，从中不难得出一个对Lα中元素的有穷序列的典范排序。也即，我们可以对x，y通过排在最前的公式的定义中所使用到的参数序列排序，由此决定x，y的排序。由于在同一层用同样的公式和参数可定义的集合就是相同的集合，所以上述排序是在所有可构成集上的一个全序，并且显然是一个良序。

L上的全局良序◁L

给定关于集合论公式的枚举{φi|i＜ω}。我们对α∈ON递归定义Lα上的二元关系◁α，使得

（1）每个◁α都是Lα上的良序；

（2）若α＜β，则◁β是◁α的尾节扩张，即◁α⊂◁β且对任意x∈Lα，b∈Lβ\Lα有x ◁βb。

给定α∈ON，

（1）若α是极限序数，令◁α=∪γ＜α◁γ；

（2）若α=β+1，由归纳假设，已有◁β是Lβ的良序，

（a）对x，y∈Lβ，令x ◁αy当且仅当x ◁βy，

（b）对x∈Lβ，y∈Lβ+1\Lβ，令x ◁αy，

（c）对x，y∈Lβ+1\Lβ，令i，j＜ω是最小的分别使得存在，让

而

的自然数。

i.如果i＜j，则令x ◁αy；

ii.而如果i=j，则考虑在由◁β生成的上的典范良序下最小的分别使得（3.3），（3.4）成立的并定义x◁αy当且仅当

最后，定义◁L=∪α∈ON◁α。即，对任意x，y∈L，x ◁Ly，当且仅当存在α∈ON使得x ◁αy。容易验证，◁L是L上的良序，并且是一个Σ1可定义的关系。

因此，对任意x∈L，◁L∩x×x就是x上的一个良序，选择公理在L中成立。

为了在L中证明广义连续统假设成立，首先注意，对每个无穷的序数α，Lα的基数就是α的基数。其次，我们需要使用斯寇伦发明的一种模型论方法来证明每个Lα的可构成子集都是在Lα+^[13]之前被构造出来的。假设X⊂Lα是可构成集，那么它总是在某一步，例如Lδ中被定义出来的。δ可能很大，甚至远远大于α+。根据归纳假设，我们可以假定定义X所使用的那有穷个参数都在某个Lβ（α＜β＜α+）之前就被构造出来了。利用上面提到的那种模型论方法，我们可以找到一个Lγ（β＜γ＜α+），使得X在Lγ中就可以用同样的公式和参数定义出来。由此，Lα的所有可构成子集P（Lα）∩L⊂。因此，在L中，基数card Lα=card α＜2cardα=card P（Lα）≤card Lα+=α+，广义连续统假设成立。

至此，我们证明了AC和GCH在L中成立。这些证明是在ZF中完成的，也即我们有ZF ⊢ACL和ZF ⊢GCHL，而后者又可以看作是中可证的算术命题。结合ZFL的证明，对任意集合论公式φ，我们有

特别地，取σ为v1/=v1，即

以上，我们简述了基于哥德尔可构成集概念的有穷主义的相对一致性证明。关于L更详细的讨论，读者可以参考（郝兆宽、杨跃，2014）、（Kunen，2013）和（Jech，2002）。接下来，笔者试图进一步挖掘L的构造及其发现过程中所涉及的哲学内涵。

哥德尔在发表其一致性结果的报告（Gödel，1938）中就写道：

“可构成”集被定义为那些由罗素的分支类型谱系推广到超穷阶所能得到的集合。

哥德尔在哥廷根演讲（Gödel，1939）中也提到可构成集的定义“在其观念上依赖于所谓的分支类型论（ramified type theory）”，并肯定了可化归公理（axiom of reducibility）的重要作用。在其为数不多的哲学论文《罗素篇》（Russell’s Mathematical Logic，Gödel，1944）中，哥德尔将罗素分支类型论与可构成集的联系作为主要证据，以试图论证实在论立场相对构造主义的优势。

在哥德尔看来，罗素曾经是“言之凿凿的实在论”者，但其实在论“态度随着时间推移而衰减，并且始终是理论上强，实际中弱”。哥德尔的评论主要针对的正是罗素在其分支类型论中体现出来的构造主义思想。

罗素的类型论是对数学基础问题的一种基于逻辑主义的解决方案，也即试图将数学还原为被称作类型论的逻辑理论。特别地，类型论将数学对象区分为诸类型是为了避免悖论。罗素等人认为悖论产生的根本原因在于出现了所谓恶性循环。回顾罗素悖论的构造（见第104页）。首先，要“构造”所谓罗素集R={x|x /∈x}，即“所有集合”中不包含自身的集合组成的集合，然后问是否有R /∈R。罗素认为，这里的问题出在罗素集的构造援引了“所有集合”这个概念。而对后者的理解依赖于所有集合，包括罗素集。因此，罗素集的定义是一种循环定义。为此，罗素在他与怀特海合著的《数学原理》（Whitehead and Russell，1913）中，为他们的数学基础方案设定了所谓的恶性循环原则。

恶性循环原则（vicious circle principle）最清晰也即哥德尔主要针对的形式可以表述为：不存在一种只有通过某个包含它的总体（totality）才能被定义的实体（entity）。^[14]违反了这种形式的恶性循环原则的定义被认为是非直谓定义。直谓主义正是源自罗素恶性循环原则的一种构造主义的哲学立场。它只承认那些可以通过直谓定义被构造出来的数学对象。正如哥德尔所说的，如果站在与构造主义相对立的实在论的立场，那么援引“总体”的非直谓定义就没什么不妥了。

在数学实践中，人们常常会使用所谓非直谓定义来定义数学对象。例如，在集合论中，自然数集ω被定义为所有满足“包含0且在+1下封闭”这个性质的集合中最小的那个。ω的定义似乎必须要诉诸“所有满足‘包含0且在+1下封闭’这个性质的集合”这个总体，而后者显然又要包含ω。又如在分析中人们常用到的“最小上界”概念：r是某个有界性质的最小上界，当且仅当它是所有上界中最小的那个。显然，这个最小上界的定义依赖于包含它的“所有上界”这个总体。同许多其他的构造主义者一样，直谓主义者试图通过各种技巧在避免使用非直谓定义的前提下保留足够多的数学。^[15]在这个意义上，罗素的分支类型论也是一种构造主义的数学基础方案。接下来，笔者将具体展示分支类型论构造中所体现的直谓主义思想及其困难。

直谓主义与自然数集

正如我们所看到的，集合论中对自然数集的定义是非直谓的。然而，直谓主义者往往接受自然数集的存在。这使他们区别于更严格的构造主义者。例如，外尔（Weyl，Hermann）宣称：“对迭代的直观向我们保证了‘自然数’概念是外延上确定的。”（Weyl，1987，p. 110）但是，我们所理解的对迭代的直观可以被表述为皮亚诺算术中的几则关于后继的公理。而运用简单的模型论方法（例如紧致性定理）很容易构造出满足这些公理的非标准模型，甚至完备的算术理论也存在可数的非标准模型。在这个意义上我们说，“自下而上”的构造方法无法确定自然数集的外延，后者必须诉诸“总体”才能定义，即所有算术模型中最小的那个。

另外，以哈姆肯斯（Hamkins，Joel David）为代表的集合论多宇宙观（set-theoretic multiverse view）的立场来看，即使预设了某个集合论宇宙M，在这个宇宙中定义的标准的自然数集也有可能在更大更真实的宇宙N中看来是非标准的：

关于集合论多宇宙观更多的讨论可参考（Hamkins，2012）和（杨睿之，2015）。(www.daowen.com)

一般将罗素的类型论区分为简单类型论（simple type theory）和分支类型论两个版本。无论是在简单类型论或是分支类型论中，一个性质（或一个命题函项）的论域（或自由变元的取值范围）都只能是一个特定的类型（type）。所有个体组成了第一个类型，或称作类型0。在简单类型论中，关于类型n中事物的所有性质组成了类型（n+1）。一个关于简单类型论的结构如图3.1所示。

图3.1　简单类型层谱

简单类型论的复杂版本

如果考虑区分含有不止一个变元的命题函项（或k元关系）的话，有可能出现更多的类型。例如，一个命题函项φ（x，Y）含有一个以所有个体为取值范围的自由变元x和一个以所有个体的性质为取值范围的自由变元Y，人们或许希望将它与ψ（X）（仅含有一个以所有个体变元的性质为取值范围的自由变元X）区别开来。为此，我们可以这么定义类型层谱：

令个体组成类型0。如果命题函项含有k个自由变元且它们的取值范围分别是类型t1，...，tk（或者称它是关于类型t1，...，tk中对象的k元关系），那么就称该命题函项（或关系）是类型〈t1，...，tk〉的，即用递归生成的有穷序列而不是自然数来索引诸类型。

例如，上面的φ（x，Y）是类型〈0，〈0〉〉的，而ψ（X）是类型〈〈0〉〉的。这样的类型层谱会非常复杂。这样精细的区分或许在计算机语言设计中有意义，但在具体数学实践中往往是不必要的。假设我们的语言可以谈论合适的类型元素间的属于关系，那么以较低类型为取值范围的变元在一定意义上总可以被以较高类型为取值范围的变元取代。例如，φ（x，Y）可以被替换为

θ(X,Y)=∃!x(x∈X)∧∀x[x∈X→φ(x,Y)]。

显然，θ中只含有以个体的性质为取值范围的自由变元。并且，个体a和性质P实现φ，当且仅当性质{a}和P实现θ。另外，在预设了基本数学理论的前提下，有穷多个变元总可以被编码为一个变元。因此，区分自由变元个数也是没必要的。

拉姆齐（Ramsey，Frank Plumpton）等学者很早便指出，简单类型论已经足以避免罗素悖论（Ramsey，1925）：当一个罗素集的论域被限制在某个类型i上时，Ri={x∈Ti|x /∈x}，它成了一个类型（i+1）的对象，而它的元素都是类型i的对象，因而，它当然不会属于它自身。因此，有人认为，罗素的分支类型论是为了解决集合悖论以外的语义悖论，例如“最小的十六个字内不可定义的自然数”等。我们将看到，分支类型论实际上是罗素对恶性循环原则或直谓主义的贯彻，并希望由此从根本上排除一切悖论。^[16]

简单类型论并没有特别的设定来避免非直谓现象。例如，我们假设类型0的个体就是所有自然数（这是直谓主义者往往接受的出发点），即类型0=ω。我们也可以假设自然数的所有性质（或命题函项）或实数P（ω）能排成一个良序，尽管我们可能并不真正知道如何来排序。这样，在这个序下最小的关于自然数的性质或实数就是存在的了，又或者具有某种属性的最小的实数。这些看起来都是非直谓的定义，它诉诸总体及其排序，并且我们或许并不知道它们具体是怎么被构造出来的。这看起来是选择公理或良序引理的问题。事实上，P（ω）上的良序引理的前提是P（ω）存在。而接下来介绍的分支类型层谱中，每一阶上都有自然的排序。如果再假设罗素的可化归公理，那么直谓主义所接受的P（ω）上就有一个自然的排序了。这也是罗素认为可化归公理蕴涵乘积公理（multiplicative axiom）^[17]的直观。

在具体定义分支类型层谱前值得一提的是：罗素在分支类型论中不预设任何“类”“性质”或“概念”的存在，而只是把它们处理成façon de parler（说话方式），也即命题函项。命题函项中可能含有自由变元和约束变元。含有一个自由变元的就是性质或类，含有两个的就是二元关系，依此类推。不含有自由变元的命题函项就是命题。例如，x=y是命题函项，而∀x∃y（x=y）是命题。这与一阶逻辑中关于公式和句子的界定是一致的。给定一个关于常元符号和量词的解释，一个命题就有了外延，非真即假。而一个命题函项就是一个函数，当我们输入关于自由变元的赋值时，它便成了命题，从而有了真假。

首先，在分支类型论中罗素假设了无穷公理，即个体是无穷的。我们不妨假设所有个体组成的类型0就是自然数集ω。如果个体的总数是有穷的话，那么分支类型层谱和简单类型层谱就没什么区别了。有穷集合的所有子集都是直谓的。

但假设有个体无穷后，罗素不直接承认所有ω上的性质都是类型1的。在有了类型0以后，接下来能得到的是ω上的直谓的命题函项，这些函项的变元全都是以ω为取值范围的。我们称这些命题函项是类型0上的1阶性质。这显然不包括关于ω中对象的所有性质。事实上，如果可以使用以所有这些1阶性质为取值范围的“2阶变元”，我们就能够利用对角线法定义出一个不同于任何一个1阶性质的关于ω中对象的性质。这个性质仍然是关于类型0的对象的，即它所对应的命题函项只含有以类型0中对象为取值范围的自由变元。但它还含有以所有1阶性质为取值范围的约束变元，所以我们称之为类型0上的2阶性质。更严格地，我们可以做如下定义：

定义　3.10（分支类型层谱）　给定一个无穷的个体集I以及I上的若干初始性质/关系/函数。读者也可以设想I=ω，而初始关系/函数包括自然数上标准的序和算术运算。给定谓词逻辑语言，其中含有无穷多类型的变元符号（我们称是第i个n级变元符号）以及对应那些初始性质/关系/函数的谓词/函数符号。

（1）定义类型0为I。

（2）类型（n+1）由所有下述命题函项组成：其中所含有的最高级变元是n级变元。直观上，这些命题函项所含的变元在语义解释中至高是以类型n为取值范围的。

（3）我们称一个命题函项是类型n上的性质，当且仅当其中所含有的最高级的自由变元是n级的。

（4）我们称一个类型n上的性质是k+1阶的，当且仅当对应的命题函项所含有的最高级的变元是（n+k）级的。我们称类型n上的性质是直谓的，当且仅当它是1阶的性质。

在上述定义中，我们忽略了单个自由变元与多个自由变元（或性质与关系）之间的区别，也只考虑命题函项所含的最高级的变元。根据对简单类型论复杂版本的讨论（见本书第114页），这样的简化并不会造成什么损失。根据上述定义，分支类型的层谱可以表示为图3.2。

图3.2　分支类型层谱

在定义3.10中，每个类型上都有任意高阶的性质，而只有1阶性质被称作直谓的（predicative）。在分支类型的层谱中，判断一个命题函项的类型只需要看其中所含变元的最高级别就行了。例如，属于类型3的命题函项，其中最高级的变元是以类型2中对象为取值范围的。因此，在分支类型层谱中的所有对象（性质），在其定义中都只援引了已先行被构造出来的对象。在可以被直谓主义（predicativism）所接受的意义上，分支类型的层谱中的所有对象都是符合恶性循环原则的，因而都是“直谓的”。显然，这与定义3.10中的“直谓”不是一个概念。

“直谓”的这两种涵义或许正暗示了罗素为分支类型论引入的声名狼藉的可化归公理。罗素将可化归公理表述为：“每个命题函项，就它的值来说，都等价于一个直谓函项。”（Russell，1908）这是在说，如果我们只考虑命题函项所定义的外延，那么一个类型上的所有性质早已在第一阶的构造中就出现了。可化归公理可以说是罗素为了使他过于复杂的分支类型论得以实际运作而不得不假设的。

分支类型论中的自然数

我们可以不假设类型0中的个体是自然数，而是无穷多个任意的对象。在分支类型论中，我们仍然可以效仿弗雷格的方法定义出每个自然数。用于计数个体的自然数可以看作是个体的性质的性质。例如，2是由所有外延中有且仅有两个元素的个体性质组成的。但根据分支类型论的构造，我们不能直接说“所有……个体性质”，而只能说“所有……个体的1阶性质”。这样，我们就会有不同类型的2。例如，类型（k+2）的2k是由所有外延中有且仅有两个元素的个体k+1阶性质组成的。显然，一个含有三个个体的1阶的类与一个含有两个个体的2阶的类的合取至多含有五个个体。不同类型的自然数之间理应是可以放在一起运算的。但在分支类型论中却变得非常复杂。可化归公理的引入使得人们只需要考虑一阶性质的数，即类型2中的对象。因为一阶性质在外延上已经齐全了。

类似地，在分支类型论中得到一般的归纳原理也需要可化归公理。假设我们已经有了所有的自然数（或者直接作为个体给出，或者构造出来的某一给定阶的自然数），那么自然数集这个概念N（x）可以写作

由此，自然可以得到归纳原理：

但是，“∀φ”并不是一个符合直谓主义的表达。根据直谓主义的要求，我们只能说：

但这样就会导致不同阶的自然数概念Nk（x）。以及针对每个自然数概念的归纳原理：

这样，归纳原理至少无法得到统一的辩护。

但如果假设可化归公理成立，那么“合法”的（3.8）就获得了实际上和（3.6）同样的涵义。

显然，可化归公理本身不是一个在直谓主义立场上的合法命题，因为它涉及对“每个命题函项”的断言。因而，可化归公理必须被看作是一个分支类型论的元公理。对可化归公理的批评非常多，有的认为可化归公理使分支类型论退化成简单类型论。^[18]更多人认为，可化归公理只在个体有穷的情况下成立，而在罗素所假设的个体无穷的情况下是错误的。在接下来具体介绍分支类型层谱与可构成集层谱的对应时，我们将很容易看到这点。

为说明分支类型论与可构成集类之间的对应关系，不妨先回顾一下定义3.9（第108页）中对可构成集层谱的构造。由于罗素假设有无穷多个个体，可以假设类型0就是ω=L0（ω），而初始的谓词就是ω上的序关系，也即集合属于关系，那么类型0上的1阶性质，即类型1就是L1（ω）=D（L0（ω）），也就是在结构（ω，∈）中的所有一阶谓词公式参数可定义的ω的子集。^[19]那些一阶公式只含有一种量词，并且在结构（ω，∈）的语义解释中以ω为取值范围。

而类型2就是L2（ω）=D（L1（ω））。显然，L2（ω）是所有在结构（L1（ω），∈）中由一阶谓词公式及L1（ω）中参数所定义的L1（ω）的子集。这里的一阶公式在结构（L1（ω），∈）解释下的取值范围就是L1（ω），也即类型1。因此，L2（ω）中的对象都是类型1上的1阶性质。

另一方面，由于L0（ω）=ω∈L1（ω），我们可以使用以L0（ω）为参数的公式，例如∀y∈L0（ω）φ（x，y）来定义L2（ω）中的集合。这里，∀y∈L0就可以被看作是一个以类型0为取值范围的量词。因此，类似类型论的说法，我们在定义类型1的1阶性质时，可以使用分别以类型0和类型1为取值范围的两种量词。

又由于，显然ω⊂L1（ω），L2（ω）中会出现一些ω的子集，而这些子集是通过可以使用以类型1为取值范围的量词来构造的，因此是类型0上的2阶性质。所以，L2（ω）包含且仅包含1上的1阶性质和0上的2阶性质，因而它本身也就是类型2了。^[20]

不难看出，如果我们只考虑类型论中那些性质或命题函项的外延，并且自然地允许类型的划分向下兼容，即类型n⊂类型（n+1）（这也完全符合直谓主义关于恶性循环原则的要求），那么在有穷阶下，分支类型论谱系与可构成集的谱系可以形成一一对应，即类型n=Ln（ω）。只不过，分支类型论的构造仅限于有穷阶，即每个Ln（ω），而不承认Lω（ω）本身。参考分支类型论对性质的阶的分层，我们可以定义可构成集的分层如下：

定义　3.11

（1）集合A⊂Lα（ω）是Lα（ω）的β+1阶可构成子集，当且仅当A∈Lα+β+1（ω）\Lα+β（ω）；

（2）可构成集A是β+1阶可构成的，当且仅当存在最小的序数α使得A⊂Lα（ω），且A是Lα（ω）的β+1阶可构成子集。

在上述对应下，一个集合A可以被表示为类型n的k+1阶性质，当且仅当它是Ln（ω）的k+1阶可构成子集。由此，我们就可以在可构成集语境下将可化归公理表述为：

以及一个更强的版本：

可是，无论（3.9）还是（3.10）在ZFC下都被证明是错的。例如，在L中，ω的可构成子集的基数是不可数的，即Lcard P（ω）＞ℵ0，而其1阶可构成的子集L1（ω）受限于公式的基数，是可数的。或者更具体地，我们可以利用对角线法的构造，在每个Ln+1（ω）中找到一个与所有Ln（ω）中的所有ω子集都不同的ω子集。

根据哥德尔的说法，可构成集层谱无非是对分支类型层谱在任意阶上的推广。可构成集类包含Lω（ω），乃至任意Lα（ω）（α∈ON）。在允许任意超穷阶的前提下，我们可以陈述一则弱版本的可化归公理。这时，我们不要求每个可构成集在下一个序数阶就被构造出来，而只要求它在下一个基数阶前被构造出来，即：

引理　3.12　假设V=L。如果X⊂Lα（ω），那么X∈Lα+（ω）。

其中，α+是比α大的下一个基数。引理3.12是ZF可证的。对比第111页的说明，不难看出，3.12正是证明广义连续统假设在L中成立的关键引理。正是在这个意义上，哥德尔写下了下面这段关于分支类型论的论断：

如果只是从纯数学的立场来看，而无关乎非直谓定义是否被允许的哲学问题，这种阶理论会显示出更丰富的成果。以这种角度来看，即将它视为通常的数学框架之内建立起来的理论，其中允许非直谓定义，就不会反对将它扩张到任意高的超穷阶。即使一个人反对非直谓定义，我认为也没理由反对把它扩张到在有穷阶框架中可构造的超穷序数上。该理论似乎本身有这种扩张的需要，因为它自动就会导致考虑那些在其定义中指涉所有有穷阶函项的函项，而这些会是ω阶的函项。允许超穷阶的话，一种可化归公理可以被证明。然而，这对这个理论的本来目的毫无帮助，因为那个序数α——使得每个命题函项都外延地等价于一个α阶的函项——过于大，以至于它预设了那些非直谓的全体。尽管如此，这种做法却有丰厚的收获，以至于所有非直谓性都可以归约为特殊的一种，即某些大序数（或良序集）的存在以及它们之上的递归推理的有效性。特别地，一个序型为ω1的良序集的存在对实数理论已经足够了。此外，这条超穷版的可化归定理可以证明选择公理、康托尔连续统假设甚至广义连续统假设（说的是在任何集合的势和它的所有子集组成的集合的势之间不存在另一个基数）相对于集合论公理，同样也相对于《数学原理》公理的一致性。（Gödel，1944）

哥德尔在（Gödel，1944）中把分支类型论与他的可构成集理论的上述对应看作是对其实在论立场具有优势的佐证。将分支类型层谱推广到任意序数阶的定义是简单直接的，即对极限序数α定义Lα（ω）=∪ξ＜αLξ（ω）。然而，超穷极限序数以及不可数基数的存在却不符合直谓主义的要求。因此，哥德尔认为，直谓主义帮助罗素发现了分支类型层谱的精妙构造，而这种构造主义的哲学立场却又使他们注定无法发现推广这种构造所能获得的“更丰富的成果”。而对于实在论者来说，理解直谓主义的构造并将其推广至任意序数阶都是毫无障碍的。这里，哥德尔巧妙地将其数学工作和哲学论证融为一体。

最后，关于基于可构成集类的相对一致性证明值得一提的是：它是一种基于内模型方法的相对一致性证明，而所有完全基于内模型方法的相对一致性证明都可以被直接看作是通过构造一种理论间的翻译来得到相对一致性结果的。^[21]在本例中所构造的是从（ZFC+GCH）到ZF中的翻译，即每则（ZFC+GCH）的定理σ被翻译为σL并被证明是ZF的定理。

“在解释力上不弱于”往往蕴涵相对一致性。即：如果存在从T2到T1的翻译，使得π[T2]是T1的子理论，那么Con（T1）→Con（T2）。因此，构造理论间的翻译是证明相对一致性的基本手段之一。

哥德尔在（Gödel，1933）中构造了“哥德尔否定性翻译”，将经典算术翻译到直觉主义算术中并由此证明了经典算术相对直觉主义算术一致；在（Gödel，1958）中构造了一种基于“自然数上的有限类型的可计算函数”（computable function of finite type over the natural numbers）的T系统，并通过“《辩证法》翻译”将直觉主义算术HA翻译到T中，由此证明了皮亚诺算术和直觉主义算术相对T的一致性。由此得到结论：直觉主义算术作为数学基础相比经典算术并没有什么优势或更安全。感兴趣的读者可以参考论文（杨睿之，2014）。

但是下一节中介绍的基于力迫法的相对一致性证明却不能被解释成构造了一种经典谓词逻辑理论间的翻译。