Coq 类型论中的丘奇论题及相关公理

“丘奇论题”（$\mathsf{CT}$）作为构造逻辑中的一条公理，陈述了每个类型为 $\mathbb{N} \to \mathbb{N}$ 的全函数都是可计算的，即在某计算模型中可定义。$\mathsf{CT}$ 在经典数学和布劳威尔直觉主义中均不一致，因为它分别违背了弱柯尼希引理和扇定理。近来，$\mathsf{CT}$ 被证明对（单值）构造类型论是一致的。由于弱柯尼希引理和扇定理都既不是构造逻辑中纯逻辑公理、也不是其所假设的类选择公理的推论，似乎 $\mathsf{CT}$ 仅在与经典逻辑和选择公理的组合相矛盾。我们在 Coq 的类型论（一种具有命题宇宙、既不证明经典逻辑公理也不证明强选择公理的构造类型论）中研究 $\mathsf{CT}$ 的推论及其与若干类公理的关系。我们由此部分回答了哪些公理可能保留类型论内在的计算直觉、而哪些肯定不能的问题。本文也可作为类型论中公理的广泛综述来阅读，所有结果均在 Coq 证明辅助器中机械化。