非直谓性 (类型论)

关于其它含义, 请参见 “非直谓性”.

非直谓性一般来说是指某种定义是自指的, 在类型论中是宇宙的性质. 大致来说, 若如下规则成立 (省略类型所在的语境):$$\frac{A:{\mathcal{U}}^{\prime }x:A⊢B:\mathcal{U}}{{\prod }_{x:A}B(x):\mathcal{U}}$$且 $\mathcal{U}$ 不包含 ${\mathcal{U}}^{\prime }$ (也就是说 ${\mathcal{U}}^{\prime }$ 比 $\mathcal{U}$ 大), 那么 $\mathcal{U}$ 是非直谓的. 一般来说, 两个类型取 $\Pi$ 类型得到的新类型, 应该存在于较大的那个宇宙, 这个性质叫做直谓性. 而能违反这件事的性质就叫做非直谓性.

由于宇宙之间的大小关系在类型论中不好统一定义, 因此非直谓性往往对于每个类型论都有自己的版本.

例 0.1. 假设某类型论中存在如下两个宇宙:

•	一族的类型宇宙 ${\mathcal{U}}_1,{\mathcal{U}}_2,{\mathcal{U}}_3,\cdots$,
•	命题宇宙 $\mathrm{Prop}$, 换言之若 $P:\mathrm{Prop}$ 那么 $P$ 会被看作命题.

规定 ${\mathcal{U}}_i:{\mathcal{U}}_{i+1}$ (对于任意 $i$) 以及 $\mathrm{Prop}:{\mathcal{U}}_1$.

我们理应将谓词 $\forall a\in A.P(a)$ 视作命题, 该谓词说的是 “对于类型 $A$ 的任意实例 $a$, 有命题 $P(a)$ 成立”. 根据 Curry–Howard 对应, 它被实现为 ${\prod }_{a:A}P(a)$, 而要让这个类型是命题, 我们需要

$$\frac{A:{\mathcal{U}}_{i}a:A⊢P(a):\mathrm{Prop}}{{\prod }_{a:A}P(a):\mathrm{Prop}}$$

若如上规则成立, 那么该命题宇宙是非直谓的, 在有非直谓的宇宙时我们也说该类型论是非直谓的.

在非类型论或者 Russell 简单类型论的讨论环境中, 非直谓一般指某种自指性.

1后果

非直谓类型宇宙在依值类型论中会破坏一致性, 参见 Berardi 悖论. 非直谓的命题宇宙则没有问题, 构造演算就是一个有直谓类型宇宙和非直谓命题宇宙的系统.

包含一个非直谓宇宙能大大提高类型论的证明论强度. 例如 Martin-Löf 类型论是直谓的, 在里面甚至不能定义 F 系统, 因为后者是非直谓的.

2相关概念

•	降级公理是定理形式的非直谓性, 和作为类型论规则的非直谓性拥有同样的证明论强度.
•	经典逻辑的公理如排中律, 选择公理蕴涵降级公理.

术语翻译

非直谓性 • 英文 impredicativity