命题宇宙

关于其它含义, 请参见 “构造演算”.

命题宇宙是特殊的宇宙, 它仅包含命题, 而不是所有类型, 一般记作 $\mathrm{Prop}$. 若某类型要么存在唯一实例、要么没有实例, 那么这个类型被认为是一个命题, 这个观点来源于 Curry–Howard 对应.

定义 0.1. 若对于类型 $\Gamma ⊢A$ 存在如下证明$$\prod _{a,b:A}{\mathrm{Id}}_A(a,b)$$那么 $A$ 是一个命题. 换言之, $A$ 的任意实例命题等价.

这意味着 $A$ 要么等价于空类型, 要么等价于单位类型. 这里的命题对应着$n$-类型中 $n=-1$ 的情况. 命题宇宙就是包含这样的类型的宇宙.

在 Russell 简单类型论和构造演算的传统中, 命题宇宙都满足非直谓性, 但这不是必须的.

1定义

命题宇宙有多种不同的方式定义. 有一个重要的辅助定义 $\mathrm{isProp}$, 用到了$\Pi$ 类型和相等类型:

$$\mathrm{isProp}A:=\prod _{a:A,b:A}{\mathrm{Id}}_A(a,b)$$

这个定义对应了同伦类型论中同伦层级为 $-1$ 的情况.

内部定义

使用$\Sigma$ 类型和宇宙, 可以直接定义命题的宇宙:

$$\mathrm{Prop}:=\sum _{A:\mathcal{U}}(\mathrm{isProp}A)$$

任何满足 $\mathrm{isProp}$ 的类型都可以被放进这个版本的命题宇宙中, 由于这个性质我们认为它是完备的.

严格定义

$$\Gamma ⊢\mathrm{Prop}$$

严格的命题宇宙只包含一部分预先设定好的命题, 也就是说某个类型是否是严格的命题这件事是类型论中先验的、在语法层面上就可以知道的事情, 也就是说, 严格的命题宇宙存在一些 “漏网之鱼”: 某些类型满足 $\mathrm{isProp}$ 却不属于该宇宙.

严格的宇宙如此严格, 不仅是因为它对 “哪些类型是命题” 严格, 更因为它对命题的定义严格: 任何 “证明” 都相等.

$$\frac{\Gamma ⊢A:\mathrm{Prop}\Gamma ⊢a:A\Gamma ⊢b:A}{\Gamma ⊢a=b:A}$$

该宇宙可以定义为非直谓的, 见 [Gilbert–Cockx–Sozeau–Tabareau 2019].

理想定义

融合 严格定义 和 内部定义 可以得到最强的定义, 这必须用到 Tarski 宇宙, 因为同时需要如下两个条件:

•	$\mathrm{Prop}$ 是一个独立于 $\mathcal{U}$ 的宇宙, 它等价于后者满足 $\mathrm{isProp}$ 的子集. 这是为了使得它可以被底层的规则直接操纵.
•	降级公理, 即 $\mathrm{Prop}$ 需要有足够强的构造规则, 即任何满足命题的要求的类型都存在一个等价的命题. 这里等价的定义可以任取, 只要足够类似同构即可.

于是我们在 严格定义 的基础上给出如下构造规则:

$$\frac{\Gamma ⊢Ap:\mathrm{isProp}A}{\Gamma ⊢R(A,p):\mathrm{Prop}}$$

再加上如下规则, 就满足了降级公理的需求:

$$\frac{\Gamma ⊢Ap:\mathrm{isProp}A}{\Gamma ⊢e(A,p):\mathrm{el}(R(A,p))\simeq A}$$

弱定义

理想定义 过于理想, 因为它隐含了一种从 $\mathrm{isProp}$ 中的命题相等到类型论内部的相等的转换, 这会使得类型论的性质过强, 接近外延类型论. 因此, 可以将 理想定义 中 严格定义 的部分换成如下规则:

$$\frac{\Gamma ⊢A:\mathrm{Prop}}{\Gamma ⊢\mathrm{inProp}(A):\mathrm{isProp}A}$$

这样就消除了命题相等到相等的转化.

2性质

外延性

参见: 泛等公理

我们希望互相蕴涵的命题相等, 但这并不总是成立 (至少在 Martin-Löf 类型论中不能证明).

定义 2.1 (命题外延性). 对于命题 $A,B$, 如下命题叫做命题外延性: $$(A\to B)\times (B\to A)\to \mathrm{Id}(A,B)$$

泛等公理蕴涵命题的外延性.

一致性

为了确保一致性, 类似 严格定义 中的命题不能被 “转换” 为一般的类型. 换言之, 考虑 $A:\mathrm{Prop},B:\mathcal{U}$, 函数类型$$A\to B$$的实例只能是常数函数, 不能对参数进行类似模式匹配的消去.

例 2.2 (反例). 考虑如下类型:

•	$2:\mathcal{U}$ 为有两个不同实例 $y,n$ 的类型 (显然 $y\ne n$),
•	$2_p:\mathrm{Prop}$ 为有两个不同证明 $y_p,n_p$ 的命题 (根据命题的性质, 有 $y_p=n_p$).

考虑对参数进行消去的模式匹配函数: $$\begin{array}{rl}f& :2_p\to 2\\ f& (y_p)=y\\ f& (n_p)=n\end{array}$$将 $y_p=n_p$ 的证明通过以上函数映射到一个 $y=n$ 的证明, 矛盾.

选择公理在一定程度上解除了该限制.

3范畴语义

依值类型论中性质合适的命题宇宙对应它范畴语义中的子对象分类子. 令 $\Omega$ 为 $\mathrm{Prop}$, 再考虑等价于单位类型的类型 ${\Sigma }_{A:\mathrm{Prop}}A$, 子对象分类子的交换图可以重新诠释:

$$\Gamma ,A{\Sigma }_{A:\mathrm{Prop}}A\Gamma \mathrm{Prop}证明\mathrm{isProp}A{\pi }_A取第一项R(A,p)$$

该交换图指出若存在某类型 $\Gamma ⊢A$ 使得该图表存在右上部分, 然后左边的 ${\pi }_A$ 又是类型本身的定义一定能给出的, 那么就一定存在唯一的 $R(A,p):\mathrm{Prop}$ 对应之. 也就是说, 若我们能证明 $\mathrm{isProp}A$, 那么存在唯一的命题等价于 $A$.

4参考资料

•	Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau (2019). “Definitional Proof-Irrelevance without K”. Proc. ACM Program. Lang. 3 (POPL). (doi) (web)

术语翻译

命题宇宙 • 英文 universe of propositions

命题外延性 • 英文 propositional extensionality