分歧类型论

分歧类型论是 Russell 简单类型论的原型, 它可以看作一种过度直谓的 “不简单的类型论”.

在分歧类型论中, 最底层的 “性质” 不能用其它上的谓词定义, 比如:

我是数学家.

中的 “是数学家” 就是一个底层的性质, 这样的性质是直谓的. 如果使用了谓词, 比如:

我拥有所有数学家拥有的精神品质.

这个性质就涉及到了 “所有数学家”, 所以是非直谓的, 这样的性质就比前面的性质高一层.

令 $n<m$, 分歧类型论仅允许通过第 $n$ 层的性质来定义 $m$ 层的性质. 这种限制大大降低了分歧类型论作为数学的基础的强度, 因为有过多的数学概念的定义本身就会提升层级, 比如序列在定义的时候需要用到元素上的大小关系, 这就导致序列这个概念本身需要有一个层级, 比如使用第 $k$ 层的性质定义的序列就处于第 $k+1$ 层, 而该序列的性质则在 $k+2$ 层, 等等.

因为上述原因, 在 [Whitehead–Russell 1927] 中出现了如下公理:

定义 0.1 (规约公理). 对于任何第 $k$ 层的性质, 都存在一个逻辑上等价的第 $1$ 层的性质.

这个公理使得分歧类型论的性质分层没有任何意义, 于是便诞生了不分层的 Russell 简单类型论.

1相关概念

在同伦类型论中有一个类似的公理——降级公理.

2参考资料

•	Alfred North Whitehead, Bertrand Russell (1927). Principia mathematica; 2nd ed.. Cambridge Univ. Press. ()

术语翻译

分歧类型论 • 英文 ramified type theory