Russell 简单类型论

关于其它含义, 请参见 “简单类型论”.

简单类型论是 Bertrand Russell 设计的一套用于数学的基础的理论, 可以看作简单类型 λ 演算加上一套表示命题的宇宙 $o$, 是分歧类型论的非直谓简化. 换言之, 数学对象被分为两类:

•	一组类型 ${\iota }_1,{\iota }_2,\cdots$, 实例就是我们关心的数学对象. 比如研究实数时, 全体实数的类型就在这一组类型里面.

•	一个类型 $o$, 实例是命题. 命题和命题之间可以有蕴含关系、进行合取、析取等操作. 这个类型可以类比现代类型论中的命题宇宙.

在这些类型上, 还要加上一些常见的构造, 比如积类型、函数类型, 比如我们需要能研究 ${\iota }_1\to {\iota }_2$ 这样的函数, 和 ${\iota }_1\times o$ 这样的二元组.

在考虑数学对象 $\iota$ 的 “子集”(注意此时没有集合的概念, 所以这里不是真正的子集, 而是在类比子集的思想) 时, 使用 $\iota \to o$ 这样的函数来 “过滤” $\iota$ 中的元素就达到了研究子集的效果.

构造演算可以不严谨地看作将简单类型论中的 $\iota$ 那一部分换成一个依值类型论 (或者说, Martin-Löf 类型论) 后得到的类型论.

简单类型论使用 $\lambda$ 符号引入变量, 如 $\boxed{\lambda x.f(x)}$, 含义类似传统数学中的 $\boxed{x\mapsto f(x)}$.

1逻辑

简单类型论中, 逻辑连接词可以定义为满足特定规则 (类似 “公理”) 的函数:

$$\begin{array}{rl}\Rightarrow & :o\to (o\to o)\\ \vee & :o\to (o\to o)\\ \wedge & :o\to (o\to o)\end{array}$$

谓词逻辑

简单类型论中, 可以定义如下函数 (注意该符号虽然用法类似谓词逻辑中的同一符号, 但在此处是新定义的符号):

$$\begin{array}{rl}\forall & :(\iota \to o)\to o\\ \exists & :(\iota \to o)\to o\end{array}$$

例 1.1. 谓词逻辑中的命题$$\forall n\in \iota ,n\ne 2$$可以翻译为简单类型论中的命题$$\forall (\lambda n.n\ne 2):o$$此处 $n\ne 2$ 是一个命题, 因此有 $n\ne 2:o$, 因此有 $\lambda n.n\ne 2:\iota \to o$, 正好适合 $\forall$ 接受的参数类型.

例 1.1 可以轻易地推广到任意谓词.

假设存在自然数类型 (有 $0$ 和 $s$ 两个生成元), 那么数学归纳法可以定义为如下公理:$$\forall (\lambda P.P(0)\wedge (\forall (\lambda n.P(n))\Rightarrow P(s(n)))))\Rightarrow \forall (\lambda n.P(n)))$$

高阶逻辑

参见: 分歧类型论

若要讨论任意阶的谓词, 将 $\forall$ 中的 $\iota$ 不断的换成 $\iota \to o$ 即可. 因此, 可以这样重新定义 $\forall$:

$$\forall :(s\to o)\to o$$

这样的话, 允许 $s\in \{\iota ,\iota \to o,(\iota \to o)\to o,\cdots \}$ 即可在简单类型论中讨论高阶逻辑.

2语义

定义 2.1. 简单类型论的 Henkin 模型给出如下信息:

•	对于每个类型 $s$, 选择一个集合 $M_s$.

•	对于函数类型 $s_1\to s_2$, 选取一个映射 $(M_{s_1}\to M_{s_2})$ 的子集 $M_{s_1\to s_2}$.

且该模型需要满足简单类型论中的所有规则.

定义 2.2. 简单类型论的标准模型是满足如下等式的 Henkin 模型: $$(M_{s_1}\to M_{s_2})=M_{s_1\to s_2}$$

3参考资料

•	Alonzo Church (1940). “A Formulation of the Simple Theory of Types”. The Journal of Symbolic Logic 5 (2), 56–68. (web)