类型论（二）

相反，我们应该引入一种由属性和数字组成的分支层次结构。一开始，只有一阶归纳性质，在定义中并不指性质的总体，并且将1阶数定义为满足所有一阶归纳性质的元素。接下来我们可以考虑二阶归纳性质，它可以指一阶性质的集合，以及 2 阶数，即满足 2 阶归纳性质的元素。然后我们可以类似地考虑 2 阶数3、等等。庞加莱强调这样一个事实：2 阶数更不用说 1 阶数，更一般地说，n+1 阶数更不用说 n 阶数。因此，我们有一系列越来越受限制的属性：1、2 阶的归纳属性，以及一系列越来越受限制的对象集合：1、2 阶的数字……此外，属性“成为数字” n 阶本身就是 n+1 阶的归纳性质。

如果 x,y 是 n 阶数，则似乎不可能证明 x+y 是 n 阶数。另一方面，可以证明，如果x是n+1阶数，y是n+1阶数，则x+y是n阶数。事实上，属性 P(z)“x+z 是 n 阶数”是 n+1 阶的归纳属性：P(0) 成立，因为 x+0=x 是 n+1 阶数，因此是 n 阶数，如果 P(z) 成立，即 x+z 是 n 阶数，那么 x+(z+1)=(x+z)+1 也是如此，所以 P(z) +1) 成立。由于 y 是 n+1 阶数，并且 P(z) 是 n+1 阶归纳性质，因此 P(y) 成立，因此 x+y 是 n 阶数。这个例子很好地说明了分支层次结构带来的复杂性。

如果有人像罗素和弗雷格一样，将自然数等基本对象定义为类的类，那么复杂性就会进一步放大。例如，数字 2 被定义为恰好具有两个元素的所有个体类别的类别。我们再次获得分支层次结构中不同阶的自然数。除了罗素本人之外，尽管存在所有这些复杂性，Chwistek 仍试图以一种分叉的方式发展算术，斯科勒姆强调了这种分析的兴趣。有关最新进展，请参阅 Burgess 和 Hazen 1998。

经常给出的谓语定义的另一个数学例子是有界实数类的最小上界的定义。如果我们用小于该实数的有理数集合来确定一个实数，我们就会发现这个最小上限可以定义为该类中所有元素的并集。让我们将有理数的子集识别为谓词。例如，对于有理数 q，P(q) 成立，当且仅当 q 是标识为 P 的子集的成员。现在，我们将谓词 LC（有理数的子集）定义为类 C 的最小上界，如下所示：

∀q[LC(q)↔∃P[C(P)∧P(q)]]

这是谓语：我们通过对所有谓词的存在量化来定义谓词 L。在分支层次结构中，如果 C 是一阶有理数类，则 L 将是二阶有理数类。那么我们获得的不是一个概念或实数，而是不同阶的实数 1, 2, ... 1 阶实数集合的最小上界通常至少为 2 阶。

正如我们之前看到的，谓语定义的另一个例子是莱布尼茨对等式的定义。对于莱布尼兹来说，谓词“等于 a”对于 b 来说为真，当且仅当 b 满足 a 所满足的所有谓词。

一个人应该如何处理由分支层次结构带来的复杂性？罗素在《数学原理》第二版的引言中表明，在某些情况下这些并发症是可以避免的。他甚至认为，在《数学原理》第二版的附录 B 中，为了定义关系的自反传递闭包，1,2 阶自然数的分支层次结构在 5 阶处崩溃。然而，哥德尔后来在他的论证中发现了一个问题，事实上，Myhill 1974表明，这种层次结构实际上在任何有限的层面上都不会崩溃。罗素在《数学原理》第二版引言中讨论的类似问题出现在康托定理的证明中，即从所有谓词的集合到所有对象的集合不存在任何单射函数（罗素悖论的版本在我们在引言中介绍的弗雷格系统）。这可以在分支层次结构中完成吗？罗素怀疑这是否可以在谓词的分支层次结构中完成，这一点后来确实得到了证实（参见 Chwistek 1926、Fitch 1939 和 Heck 1996）。

由于这些问题，罗素和怀特海在《数学原理》第一版中引入了以下可还原性公理：谓词的层次结构，一阶、二阶等，在第 1 层崩溃。这意味着对于任何谓词阶，有一个与其等价的一阶谓词。例如，在相等的情况下，我们假设一阶关系“a = b”，相当于“a满足b满足的所有属性”。这个公理的动机纯粹是实用主义的。没有它，所有基本的数学概念，如实数或自然数，都会分为不同的顺序。此外，尽管命令式定义具有明显的循环性，可还原性公理似乎并没有导致不一致。

然而，正如 Chwistek 和后来的 Ramsey 首先注意到的那样，在可还原性公理的存在下，实际上引入分支层次结构根本没有意义！从一开始就接受命令性定义要简单得多。个人、阶级、阶级的阶级……的简单“外延”层次结构就足够了。通过这种方式，我们得到了上面介绍的 Gödel 1931 或 Church 1940 中形式化的更简单的系统。

可还原性公理引起人们对谓语定义的问题状态的关注。引用 Weyl 1946 的话，可还原性公理“是一个大胆的、近乎奇妙的公理；在我们生活的现实世界中，几乎没有任何理由可以证明这一点，而我们的思想所依据的证据也根本没有任何理由”！到目前为止，使用可还原性公理还没有发现矛盾。然而，正如我们将在下面看到的，证明理论研究证实了这一原则的极端力量。

分支层次结构的思想在数理逻辑中极其重要。罗素只考虑层次结构的有限迭代：一阶、二阶等，但从一开始就考虑了无限扩展分支的可能性。 Poincaré (1909) 提到了 Koenig 在这个方向上的工作。对于上面不同阶数的例子，他还定义了一个数，如果它可归纳所有有限阶数，则该数可归纳为 ω 阶。然后他指出，如果 x 和 y 都是 ω 阶，则 x+y 是可归纳的。这说明超限阶的引入在某些情况下可以起到可约性公理的作用。哥德尔进一步分析了分支层次结构的这种超限扩展，他注意到以下关键事实：可约性公理的以下形式实际上是可证明的：当人们将自然数上的属性分支层次结构扩展到超限时，该层次结构在级别 ω1 处崩溃，最小不可数序数（Gödel 1995，and Prawitz 1970）。此外，虽然在所有级别<ω1，谓词的集合是可数的，但级别ω1的谓词集合的基数为ω1。这一事实是哥德尔可构造集合模型背后的强大动机。在此模型中，自然数集（由谓词表示）的所有子集的集合的基数为 ω1，并且类似于分支层次结构。该模型以这种方式满足了连续统假设，并给出了该公理的相对一致性证明。 （哥德尔的动机最初只是为了建立一个模型，其中自然数的所有子集的集合都是良序的。）

分支层次结构也是证明理论中许多工作的来源。 Gentzen 发现算术的一致性可以通过沿序数 ε0 的超限归纳法（在可判定谓词上）来证明，自然的问题是为分支层次结构的不同级别找到相应的序数。 Schütte (1960) 发现，对于分支层次结构的第一级，即如果我们通过仅量化一阶属性来扩展算术，我们会得到一个序数强度 εε0 的系统。对于第二级，我们得到序数强度 εεε0 等。我们记得 εα 表示第 α 个 ε 序数，ε 序数是序数 β，使得 ωβ=β，参见 Schütte (1960)。

哥德尔强调，他对连续统假设问题的方法不是建设性的，因为它需要不可数序数 ω1，并且很自然地研究沿着建设性序数的分支层次结构。在 Lorenzen 和 Wang 的初步工作之后，Schütte 分析了如果我们按照以下更具建设性的方式进行会发生什么。由于算术的序数强度为 ε0，我们首先考虑分支层次结构的迭代直至 ε0。 Schütte 计算了所得系统的序数强度并发现序数强度 u(1)>ε0。然后，我们迭代分支层次结构直至该序数 u(1)，并获得序数强度 u(2)>u(1) 的系统，依此类推。每个 u(k) 都可以根据所谓的维勃伦层次结构进行计算： u(k+1) 是 phiu(k)(0)。这个过程的极限给出了一个称为 Г0 的序数：如果我们将分支层次结构迭代到序数 Г0，我们就会得到一个序数强度 Г0 的系统。大约在同一时间，S. Feferman 独立获得了这样的序数。有人声称 Γ0 在预测系统中的作用类似于 ε0 在算术中的作用。然而，最近的证明理论工作涉及具有更大的证明理论序数的系统，这些序数可以被认为是谓语的（例如参见 Palmgren 1995）。

除了这些与分支层次结构相关的证明理论研究之外，证明理论中还致力于分析可还原性公理的一致性，或者等效地，谓语定义的一致性。继 Gentzen 对顺序微积分中的割消除性质的分析之后，Takeuti 发现了简单类型理论（无分支）的优雅的顺序公式，并做出了割消除对于该系统应该成立的大胆猜想。考虑到谓语量化的循环性，这一猜想起初似乎极其可疑，这在这种形式主义中得到了很好的体现。量化规则确实是

⊢∀X[A(X)]

⊢A[X:=T]

其中 T 是任何术语谓词，它本身可能涉及对所有谓词的量化。因此，公式 A[X:=T] 本身可能比公式 A(X) 复杂得多。

一个早期的结果是，Takeuti 谓语系统的割消法以有限的方式暗示了二阶算术的一致性。 （有人表明这意味着无穷大公理的适当形式的一致性，参见 Andrews 2002。）继 Schütte (1960b) 的工作之后，W. Tait 和 D. Prawitz 后来证明割消去性质确实成立（这个证明必须使用更强的证明理论原理，因为它应该根据不完备性定理。）

这里重要的是，这些研究揭示了预测量化的极端力量，或者同等地，可还原性公理的极端力量。这在某种程度上证实了庞加莱和罗素的直觉。二阶算术的证明理论强度远远高于 Schütte 考虑的所有算术的分支扩展。另一方面，尽管在 Takeuti 的微积分中，谓语定义的循环性变得如此明确，但在二阶算术中尚未发现悖论。

证明论的另一个研究方向是了解有多少必然的量化可以从直觉数学中可用的原理来解释。最强有力的此类原则是归纳定义的强形式。有了这些原理，我们就可以解释一种限定形式的谓语量化，称为 Π

1

1

-理解，仅对谓词使用一级谓语量化。有趣的是，几乎所有已知的谓式量化的用途：莱布尼茨等式、最小上界等，都可以用 Π 来完成

1

1

-理解。 Π 的减少

1

1

-理解首先由 Takeuti 以相当间接的方式实现，后来由 Buchholz 和 Schütte 使用所谓的 Ω 规则进行简化。它可以被视为对谓语定义的一些受限但重要的使用的建设性解释。

4.类型论/集合论

类型论可以用作数学的基础，事实上，罗素在他 1908 年的论文中提出了这一点，该论文与策梅洛的论文同年发表，提出集合论作为数学的基础。

直观上我们可以很清楚地解释集合论中的类型论：类型简单地解释为集合，函数类型 A→B 可以使用函数的集合论概念来解释（作为函数关系，即一组对）元素）。类型A→o对应幂集操作。

另一个方向更有趣。我们如何用类型来解释集合的概念？由于A. Miquel，它有一个优雅的解决方案，该解决方案是P. Aczel（1978）的先前作品，并且还具有解释不一定有良好基础的La Finsler的优势。一个人只是将集合解释为尖的图（图中的箭头代表成员关系）。这在类型理论中非常方便地表示，一个尖的图仅由A型和一对元素给出

答：A，R：A→A→O。

然后，我们可以在类型理论中定义两个这样的集合A，A，R和B，B，S相等的：如果A和B之间存在一个仿真t，则Tab所得到。分合是一个关系

T：A→B→O。

每当txy和rxu保持时，就会存在v，以至于tuv和syv保持，每当txy和ryv保持时，就会存在u，以便tuv和rxu保持。然后，我们可以定义会员关系：集合表示B，B，S是该集合的成员，由A，A，R IFF代表A1，因此Ra1a和A，A1，A1，R和B，B，B，S为bisimilar 。

然后可以检查一下，设置理论扩展性，功率集，联合，理解的所有常规公理对有限公式（甚至是反基础），以便在这个简单的模型中保持会员关系不需要充分的基础）。 （有界公式是一个公式，其中所有量化均为form∀x∈A…或∃x∈A…）。通过这种方式，可以证明教堂的简单类型理论与Zermelo的集合理论的有限版本相当。

5。类型理论/类别理论

类型理论与类别理论之间存在深厚的联系。我们将自己限制为将类型理论的两种应用呈现为类别理论：自由笛卡尔封闭类别和自由拓扑的构造（请参阅类别理论的条目，以解释“笛卡尔封闭”和“ topos”）。

为了构建免费的笛卡尔封闭类别，我们将简单类型的理论扩展到类型1（单位类型）和A，A型B类型的产品类型A×B类型。术语是通过添加配对操作和预测以及类型1的特殊要素来扩展的。如Lambek和Scott 1986所示，可以定义术语之间的键入转换概念，并表明这种关系是可以决定的。然后，可以显示（Lambek and Scott 1986）表明，类型为对象的类别和从a到b的形态学的类型是A→B型的封闭条款集（以平等为平等）是免费的笛卡尔封闭类别。这可以用来表明此类别中箭头之间的平等是可以决定的。

教会类型的理论也可以用来建造免费的拓扑。为此，我们将对象对a，e，e具有类型和e的部分等价关系，即封闭的项e：a→a→o，是对称和及传递的。我们以A，E和B，F之间的形态为形态r：A→B→O，其功能性，对于任何a：令人满意的EAA存在，其中一个是一个（modulo f）b的一个（modulo f）b）b这样的FBB和RAB。对于亚对象分类器，我们将对o，e与e：o→o→o定义为

emn = and（暗示）（暗示）

然后，人们可以证明此类别形成了TOPOS，实际上是免费的Topos。

应当指出的是，兰贝克和斯科特1986年的类型理论使用了亨金（Henkin）和P. Andrews（2002）提出的类型理论的变体，该理论是具有伸展等于的唯一逻辑连接，即多态常数

等式：A→A→O。

并从该结缔组织和常数t，f：o定义所有逻辑连接器。例如，一个人定义

∀P= dfeq（λx.t）p

O类型的平等性是逻辑等效性。

强度公式的一个优点是，它允许基于λ-calculus直接表示证明（Martin-Löf1971和Coququand 1986）。

6。类型系统的扩展，多态性，悖论

我们已经在类型上看到操作A→A→O与集合的PowerSet操作之间的类比。在集合理论中，可以沿累积层次结构转移Powerset操作。这样很自然地寻找类型理论的类似的跨限定版本。

教堂简单类型理论的这种扩展是通过添加宇宙获得的（Martin-Löf1970）。添加宇宙是一个反射过程：我们添加了一个类型U，其对象是到目前为止所考虑的类型。对于教会的简单类型理论，我们将拥有

o：u，i：u和a→b：u如果a：u，b：u

此外，如果A：u，则A是一种类型。然后，我们可以考虑诸如

（A：U）→A→A。

和诸如

id =λa.λx.x：（a：u）→a→a

该函数ID作为参数作为“小”类型A：U和类型A的元素X，并输出A类型A的元素。如果t（a）是假设A：U，则可以形成一个类型。因类型

（a：u）→t（a）

该m是这种类型的，意味着每当a：u时MA：t（a）。我们以这种方式扩展类型理论，其强度与Zermelo的集合理论相似（Miquel 2001）。在（Palmgren 1998）中考虑了更强大的宇宙形式。 Miquel（2003）介绍了一种类型的强度理论，相当于Zermelo-Fraenkel之一。

通过添加公理u：u获得一种非常强大的宇宙形式。 P. Martin-Löf在1970年提出了这一点。吉拉德（Girard）表明，所产生的类型理论是逻辑系统不一致的（Girard 1972）。尽管起初似乎可以使用一组所有集合可以直接重现罗素的悖论，但由于集合和类型之间的差异，实际上无法直接悖论。确实，在这种系统中矛盾的派生是微妙的，并且是间接的（尽管如Miquel 2001所述，现在可以通过将集合表示为尖的图来将其简化为Russell的悖论）。 J.Y.吉拉德（Girard）首先获得了较弱的系统的悖论。稍后将这种悖论完善（Coquand 1994和Hurkens 1995）。 （Barendregt 1992中引入的纯型系统的概念很方便获得这些悖论的尖锐表述。）而不是Axiom u：U仅假设

（a：u）→t（a）：u

如果t（a）：u [a：u]。请注意圆形性，实际上与被分配的层次结构拒绝的循环相同：我们通过量化U的所有元素来定义u类型的元素

（A：U）→A→A：U

将是多态认同函数的类型。尽管有这种循环，J.Y。吉拉德（Girard）能够显示出具有这种形式多态性系统的类型系统的归一化。但是，教会简单类型理论用多态性的扩展是逻辑系统不一致的，即所有命题（O型）都是可证明的。

J.Y.吉拉德（Girard）考虑具有多态性类型系统的动机是将戈德尔的辩证神（Gödel1958）解释扩展到二阶算术。他证明了使用可还原性方法（1967年）引入的同时分析戈德尔（Gödel）1958年引入的归一化。 （然后使用吉拉德的论点来表明，切割终止在上面介绍的takeuti的序列微积分中终止。）J。Reynolds（1974）独立引入了类似的系统，同时分析了计算机科学中多态性的概念。

马丁·洛夫（Martin-Löf）介绍了一种类型的所有类型，源于库里（Curry）和霍华德（Howard）的工作所建议的命题和类型的概念。值得回忆起他的三个激励点：

罗素对类型的定义是命题功能的重要性范围

一个人需要对所有命题进行量化（简单类型理论的不可思议）这一事实这一事实这一事实

识别命题和类型

给定（1）和（2），我们应该具有一种类型的命题（如简单类型的理论），并且（3）这也应该是所有类型的类型。吉拉德（Girard）的悖论表明，一个人不能同时拥有（1），（2）和（3）。马丁·洛夫（Martin-Löf）的选择是剥夺（2），将类型理论限制为谓词（实际上，宇宙的概念在类型理论中首先是所有类型类型的谓语版本）。 1986年，Coquand讨论了取走（3）的另一种选择（3）。