类型论（一）
1. 悖论和罗素的类型理论
2. 简单类型理论和 λ 演算
3. 分支层次结构和命令式原则
4.类型论/集合论
5.类型理论/类别理论
6. 类型系统的扩展、多态性、悖论
7. 单一基础
参考书目
学术工具
其他互联网资源
相关条目
1. 悖论和罗素的类型理论
类型论是罗素为了解决他在集合论的描述中发现的一些矛盾而提出的，并在1903年罗素的“附录B：类型学说”中引入。这个矛盾是通过分析康托定理得到的没有映射
F:X→Pow(X)
（其中 Pow(X) 是类 X 的子类的类）可以是满射的；也就是说，对于 X 的某个元素 a，F 不能使得 Pow(X) 的每个成员 b 都等于 F(a)。这可以“直观地”表述为 X 的子集比 X 的元素多的事实X. 这个事实的证明是如此简单和基本，所以值得在这里给出。考虑 X 的以下子集：
A={x∈X∣x∉F(x)}。
这个子集不能在F的范围内。对于如果A=F(a)，对于某个a，那么
a ∈ F(a) 当且仅当 a ∈ A
当且仅当 a∉F(a)
这是一个矛盾。
有些评论是有顺序的。首先，该证明没有使用排中律，因此直观上是有效的。其次，所使用的方法，称为对角化，已经存在于 du Bois-Reymond 的工作中，用于构建比给定函数序列中的任何函数增长得更快的实际函数。
罗素分析了如果我们将这个定理应用到A是所有类中的类的情况，会发生什么，并承认存在这样一个类。然后他被引导去考虑不属于他们自己的特殊类别
R={w∣w∉w}。
然后我们有
R∈R 当且仅当 R∉R。
看来康托确实已经意识到这样一个事实：所有集合的类不能被认为是一个集合。
罗素将这个问题传达给弗雷格，他的信以及弗雷格的回答出现在 van Heijenoort 1967 中。重要的是要认识到公式 (*) 并不适用于弗雷格的系统。正如弗雷格本人在给罗素的答复中所写的那样，“谓词是谓词本身”这一表述并不准确。弗雷格对谓词（概念）和宾语进行了区分。 （一阶）谓词适用于对象，但不能将谓词作为参数。弗雷格系统中悖论的精确表述使用了谓词 P 的外延概念，我们将其指定为 εP。谓词的外延本身就是一个对象。重要的公理 V 是：
εP=εQ=∀x[P(x)=Q(x)]
该公理断言，当且仅当 P 和 Q 实质上等价时，P 的外延与 Q 的外延相同。然后我们可以通过定义谓词将罗素悖论（*）翻译成弗雷格系统
R(x) 当且仅当 ∃P[x=εP∧ØP(x)]
然后可以使用 Axiom V 以一种关键的方式进行检查，
R(εR)≠R(εR)
我们也有矛盾。 （请注意，为了定义谓词 R，我们对谓词使用了谓词存在量化。可以证明弗雷格系统的谓词版本是一致的（参见 Heck 1996 和 Ferreira 2002 的进一步细化）。
从这个叙述中可以清楚地看出，弗雷格的著作中已经存在了类型的概念：在那里我们发现了对象、谓词（或概念）、谓词的谓词等之间的区别。（这一点在 Quine 1940 中得到了强调。）这种层次结构被罗素称为“外延层次结构”（1959），罗素认为其必要性是其悖论的结果。
2. 简单类型理论和 λ 演算
正如我们在上面看到的，宾语、谓词、谓词的谓词等区别似乎足以阻止罗素悖论（Chwistek 和 Ramsey 认识到了这一点）。我们首先在《原理》中描述类型结构，然后在本节中，我们将介绍 Church 1940 基于 λ 演算的优雅公式。类型可以定义为
i 是个体的类型
() 是命题类型
如果 A1,…,An 是类型，则 (A1,…,An) 是各个类型 A1,…,An 的对象上的 n 元关系的类型
例如，个体上的二元关系类型为(i,i)，二元联结词的类型为((),())，个体上的量词类型为((i))。
为了形成命题，我们使用这种类型结构：因此，如果 R 是 (A1,…,An) 类型并且 ai 是 Ai 类型（i=1,…,n），则 R(a1,…,an) 是一个命题。这一限制使得不可能形成 P(P) 形式的命题：P 的类型应为 (A) 形式，并且 P 只能应用于 A 类型的参数，因此不能应用于自身，因为A 与 (A) 不同。
然而，简单的类型理论不是预测性的：我们可以通过以下方式定义类型为 (i,i) 的对象 Q(x,y)
∀P[P(x)⊃P(y)]
假设我们有两个个体 a 和 b，使得 Q(a,b) 成立。我们可以将 P(x) 定义为 Q(x,a)。显然 P(a) 成立，因为它是 Q(a,a)。因此 P(b) 也成立。我们已经以必然的方式证明了 Q(a,b) 蕴涵 Q(b,a)。
哥德尔和塔斯基提出了另一种更简单的公式，仅保留类、类的类等概念。实际上，哥德尔在他 1931 年关于形式上不可判定命题的论文中使用了这个更简单的版本。不可判定命题的发现可能是由一种启发式论证所激发的，即人们不太可能将一阶逻辑的完备性定理扩展到类型论（参见哥德尔文集第三卷中他 1930 年在柯尼斯堡的演讲的结尾） ，Awodey 和 Carus 2001 以及 Goldfarb 2005）。 Tarski 有一个用类型论表达的可定义定理的版本（参见 Hodges 2008）。参见 Schiemer 和 Reck 2013。
我们有类型 0 的对象，对于个体，类型 1 的对象，对于个体的类，类型 2 的对象，对于个体的类的类，等等。两个或多个参数的函数（如关系）不需要包含在原始对象中，因为可以将关系定义为有序对的类，并将有序对定义为类的类。例如，个体 a、b 的有序对可以定义为 {{a},{a,b}}，其中 {x,y} 表示唯一元素为 x 和 y 的类。 （Wiener 1914 建议对类关系进行类似的简化。）在这个系统中，所有命题都具有 a(b) 形式，其中 a 是 n+1 类型的符号，b 是 n 类型的符号。因此，该系统建立在给定域的对象的任意类或子集的概念以及给定域的所有子集的集合可以形成下一类型的新域的事实之上。从给定的个体领域开始，然后迭代这个过程。正如 Scott 1993 所强调的那样，在集合论中，形成子集的过程被迭代到超限中。
在这些版本的类型论中，就像在集合论中一样，函数不是原始对象，而是被表示为函数关系。例如，加法函数由 (i,i,i) 类型的对象表示为三元关系。 Church 在 1940 年给出了简单类型理论的优雅表述，通过引入函数作为原始对象来扩展它。它使用 λ 演算符号（Barendregt 1997）。由于这样的表述在计算机科学中很重要，对于与范畴论和 Martin-Löf 类型理论的联系，我们对其进行了一些详细的描述。在这个公式中，谓词被视为一种特殊的函数（命题函数），这个想法可以追溯到弗雷格（例如参见 Quine 1940）。此外，函数的概念被认为比谓词和关系的概念更原始，并且函数不再被定义为一种特殊的关系。 （Oppenheimer 和 Zalta 2011 提出了一些反对这种原始函数表示的论点。）该系统的类型归纳定义如下
有两种基本类型 i（个体类型）和 o（命题类型）
如果 A,B 是类型，则 A→B，即从 A 到 B 的函数类型，是类型
我们可以用这种方式形成类型：
i→o（谓词类型）
(i→o)→o（谓词的谓词类型）
对应于类型 (i) 和 ((i))，但也对应于新类型
i→i（函数类型）
(i→i)→i（泛函类型）
写起来很方便
A1,…,An→B
为了
A1→(A2→…→(An→B))
这样
A1,…,An→o
对应于类型(A1,…,An)。
一阶逻辑仅考虑形式的类型
i,…,i→i（函数符号类型），以及
i,…,i→o（谓词类型，关系符号）
请注意
A→B→C
代表
A→(B→C)
（右侧的关联）。
对于这种逻辑的术语，我们不会遵循丘奇的解释，而是对其进行轻微的改变，这是由于库里（在丘奇的论文出现之前他有类似的想法）造成的，并且在 R. Hindley 的关于类型理论的书中详细介绍了这一点。与 Church 一样，我们使用 λ 演算，它提供了函数的一般表示法
M::=x∣MM∣λx.M
这里我们使用了所谓的BNF表示法，在计算科学中非常方便。这给出了 λ 项的语法规范，展开后意味着：
每个变量都是一个函数符号；
两个功能符号的每个并置都是一个功能符号；
每个 λx.M 是一个函数符号；
没有其他功能符号。
函数应用 MN 的符号与数学符号 M(N) 略有不同。一般来说，
M1M2M3
代表
(M1M2)M3
（左侧的关联）。项 λx.M 表示将 M[x:=N] 与 N 相关联的函数。这种表示法是如此方便，以至于人们想知道为什么它没有在数学中广泛使用。 λ-演算的主要方程是（β-转换）
(λx.M)N=M[x:=N]
将 λx.M 表达为函数的含义。我们使用 M[x:=N] 作为当 N 替换矩阵 M 中的变量 x 时所产生的表达式值的符号。人们通常将此方程视为重写规则（β-约简）
(λx.M)N→M[x:=N]
在无类型 lambda 演算中，这种重写可能不会终止。典型的例子由术语 Δ=λx.xx 给出，并且应用
ΔΔ→ΔΔ
（注意与罗素悖论的相似性。）Curry 的想法是将类型视为 lambda 项上的谓词，编写 M:A 来表示 M 满足谓词/类型 A。
N：A→B
那么就是
∀M，如果 M:A 则 NM:B
这证明了以下规则的合理性
N:A→BM:A
近品名称：B
中:B[x:A]
λx.M:A→B
一般来说，人们的判断形式如下
x1:A1,...,xn:An⊢M:A
其中 x1,...,xn 是不同的变量，M 是具有 x1,...,xn 中所有自由变量的项。为了能够得到丘奇系统，我们需要添加一些常数来形成命题。通常
不是：o→o
暗示：o→o→o
并且：o→o→o
对于所有人： (A→o)→o
期限
λx.Ø(xx)
表示不适用于自身的谓词的谓词。然而，该项没有类型，也就是说，不可能找到 A 使得
λx.←(xx):(A→o)→o
这是罗素悖论无法表达这一事实的正式表达。莱布尼茨等式
问：i→i→o
将被定义为
Q=λx.λy.∀(λP.imply(Px)(Py))
通常写为 ∀x[M] 而不是 ∀(λx.M)，然后 Q 的定义可以重写为
Q=λx.λy.∀P[暗示(Px)(Py)]
这个例子再次说明我们可以在简单类型理论中制定谓语定义。
使用 λ 项和 β 约简最方便地表示简单类型理论中所需的复杂替换规则。例如，如果我们想用谓词 λx.Qax 代替命题中的 P
暗示(Pa)(Pb)
我们得到
暗示((λx.Qax)a)((λx.Qax)b)
并且，使用 β-约简，
暗示(Qaa)(Qab)
总之，简单类型理论禁止自我应用，但不禁止命令式定义中存在的循环性。
λ-演算形式主义还可以更清晰地分析罗素悖论。我们可以将其视为谓词的定义
Rx=Ø(xx)
如果我们将 β-约简视为展开定义的过程，我们就会发现理解 R R 的定义已经存在问题
RR→Ø(RR)→Ø(Ø(RR))→…
从某种意义上说，我们有一个没有充分根据的定义，它与矛盾（一个命题相当于其否定）一样有问题。一个重要的定理，即归一化定理，表明这种情况不会发生在简单类型上：如果我们有 M:A，那么 M 可以强方式归一化（从 M 开始的任何归约序列都会终止）。
有关此主题的更多信息，我们参考 Church 的简单类型理论条目。
3. 分支层次结构和命令式原则
罗素引入了另一种层次结构，它的动机不是正式系统中表达的任何正式悖论，而是出于对“循环性”的恐惧和类似于说谎者悖论的非正式悖论。如果一个人说“我在撒谎”，那么我们就会遇到一种让人想起罗素悖论的情况：一个命题等于它自己的否定。如果我们将一个整数定义为“无法用少于 100 个单词定义的最小整数”，则会出现另一种非正式的这种矛盾情况。为了避免这种非正式的悖论，罗素认为有必要引入另一种等级制度，即所谓的“分支等级制度”。 Russell 1903 的附录 B 暗示了对这种层次结构的需要。有趣的是，这与等价命题的同一性和一类命题的逻辑乘积的问题有关。彻底的讨论可以在 Russell 1959 的第 10 章中找到。由于这种分支层次结构的概念在逻辑尤其是证明理论中具有极大的影响力，因此我们对其进行一些详细描述。
为了进一步激发这种层次结构，这里有一个罗素的例子。如果我们说
拿破仑是科西嘉人。
我们在这句话中并不是指任何属性的组合。据说“成为科西嘉人”这个属性是谓语。如果我们从另一方面说
拿破仑具备伟大将军的所有品质
我们指的是品质的整体。据说“具备伟大将军的一切品质”这一属性是必然的。
另一个同样来自拉塞尔的例子表明，预测性属性可能会导致类似说谎者悖论的问题。假设我们建议定义
一个典型的英国人拥有大多数英国人所拥有的所有财产。
显然，大多数英国人并不拥有大多数英国人所拥有的所有财产。因此，根据这个定义，一个典型的英国人应该是不典型的。拉塞尔认为，问题在于“典型”一词是通过引用所有属性来定义的，并且本身被视为一种属性。 （值得注意的是，在定义随机数的概念时，也出现了类似的问题，参见 Martin-Löf“构造性数学笔记”（1970）。）罗素引入了分支层次结构，以处理此类命令性定义的明显循环性。人们应该区分一阶属性，例如科西嘉岛，它不指属性的总体，并认为二阶属性仅指一阶属性的总体。然后我们可以引入三阶属性，它可以指代二阶属性的整体，等等。这显然消除了与命令性定义相关的所有循环。
大约在同一时间，庞加莱进行了类似的分析。他强调了“谓词”分类的重要性，以及不使用对此类进行量化来定义类元素的重要性（Poincaré 1909）。庞加莱使用了以下例子。假设我们有一个包含元素 0、1 和一个操作 + 的集合，满足
x+0 =0
x+(y+1) =(x+y)+1
假设一个性质是归纳性的，如果它满足 0，并且如果它满足 x+1，则它也成立。
一个强制性且潜在“危险”的定义是，如果一个元素满足所有归纳属性，则将其定义为数字。那么很容易证明“是一个数”这个属性本身就是归纳性的。事实上，0 是一个数字，因为它满足所有归纳性质，如果 x 满足所有归纳性质，那么 x+1 也满足。类似地，如果 x,y 是数字，则很容易证明 x+y 是数字。事实上，x+z 是一个数的属性 Q(z) 是归纳的：Q(0) 成立，因为 x+0=x 并且如果 x+z 是一个数，那么 x+(z+1)=(x+z )+1。然而，这整个论证是循环的，因为“成为数字”这个属性不是谓语，应该以怀疑的态度对待。
