选择公理 (类型论)

在类型论中可以定义选择公理, 是集合论中定义的翻译.

1定义

定义 1.1. 考虑如下数据: $$\Gamma ⊢A:\mathcal{U}\Gamma ⊢B:A\to \mathcal{U}$$满足 $A$ 是集合 (类型论), 并且对于每个 $a:A$, $B(a)$ 也是集合. 在语境 $\Gamma$ 下, 选择公理是说如下命题: $$\prod _{a:A}|B(a)|\to \left|\prod _{a:A}B(a)\right|$$

这个定义出自同伦类型论, 但由于它只用到了$\Sigma$ 类型、集合、相等类型和逻辑截断类型, 而恰好逻辑截断类型有一个巧妙的 $\lambda$ 编码、集合可以用 K 公理表述, 因此也适用于大部分支持命题宇宙的依值类型论.

2解读

经典的选择公理最常见的表述为 “任何有元素的集合的 Descartes 积仍然有元素”. 这里, “$X$ 有元素” 即对应命题 $|X|$. 这样看, 定义 1.1 就是显然的类型论翻译. 下面给出一个更容易理解的定义解读.

我们一步步解读经典的选择公理:

考虑集合 $X$, 且 $\forall x\in X$, 都有 $x\ne \varnothing$. 集合 $\cup X$ 表示 $X$ 的所有元素的并.

这个定义本质上是要求存在一组集合, 且有一个集合 $X$ 包含这些集合, 且这些集合可以取并. 这样看的话, 若使用$\Sigma$ 类型的思想, 就可以绕开集合 $X$, 直接讨论一组集合和它们的并了. 我们使用类型的思路和集合 (类型论) 翻译它:

考虑集合 $X$ 和 $A:X\to \mathcal{U}$, 满足 $\forall x:X$, 都有 $A(x)$ 为非空集合. 类型 ${\sum }_{x:X}A(x)$ 表示这些集合的并.

在类型论中, “存在” 的概念由逻辑截断给出, 因此上述条件可以描述为:$$\begin{array}{rl}X& :\mathcal{U}\\ A& :X\to \mathcal{U}\\ p& :\prod _{x:X}\left|A(x)\right|\end{array}$$

经典的选择公理在如上条件下给出一个选择函数, 即:

存在 $f:X\to \cup X$ 使得$$\forall x\in X,f(x)\in x$$

在类型论中, 按照前面的思路, 可以直接改写为

存在 $f:X\to {\sum }_{x:X}A(x)$ 使得$$\prod _{x:X}f(x)给出一个A(x)的实例$$

由于我们前面使用了 $\Sigma$ 类型编码 $\cup X$, 选择函数需要满足的性质是恒成立的, 因为 $f(x).2:A(x)$ 恒成立. 这就大大简化了叙述, 我们只需要要求该函数存在即可! 因此, 选择公理就可以叙述为:

$$\{\begin{array}{l}X:\mathcal{U},s_X:\mathrm{isSet}X\\ A:X\to \mathcal{U},s_A:{\prod }_{x:X}\mathrm{isSet}(A(x))\\ p:{\prod }_{x:X}\left|A(x)\right|\end{array}⟹\left|\prod _{x:X}A(x)\right|$$

这样的选择公理在同伦类型论可以加入同伦类型论中. 若去掉关于集合的条件, 那么这样的选择公理可以证伪.

3性质

•	选择公理与同伦类型论、立方类型论都是相容的, 尽管无法证明这条公理, 也无法证伪.

计算

选择公理在运气好的情况下可以计算, 这是一般的公理难以做到的. 由于逻辑截断类型中的一个构造规则只是包裹了它里面的类型, 假设我们能在这种情况下 (违规地) 把它里面的元素取出, 选择公理就变成了如下形式:

$$\prod _{a:A}B(a)\to \prod _{a:A}B(a)$$

这个函数的计算规则很显然: 直接返回参数即可. 但实际上逻辑截断类型并不只是简单地包裹了里面的类型, 它还有另一个构造器, 这个构造器就不能取出一个对应的元素, 这些情况下选择公理也就没法计算了.

排中律

选择公理蕴含类型论形式的排中律:

$$\prod _{P:\mathrm{Prop}}P+\neg P$$

(...)

4推广

选择公理可以看作一种将某个操作 $F:\mathcal{U}\to \mathcal{U}$ 从 $\Pi$ 类型的 “里面推到外面” 的过程:

$$\prod _{a:A}F(B(a))\to F\left(\prod _{a:A}B(a)\right)$$

将 $F$ 换成其它的操作, 比如双重否定 (类型论), 可以得到很多其它的公理.