论文标题
教会的论文和相关公理在Coq的类型理论中
Church's thesis and related axioms in Coq's type theory
论文作者
论文摘要
“教堂的论文”（$ \ mathsf {ct} $）作为建设性逻辑中的公理，即类型$ \ mathbb {n} \ to \ mathbb {n} $的每个总函数都是可计算的，即在计算模型中可定义。 $ \ mathsf {Ct} $在古典数学和Brouwer的直觉主义中都是不一致的，因为它分别与弱König的引理和粉丝定理相矛盾。最近，事实证明，（单价）建设性类型理论被证明是一致的。 由于弱König的引理和风扇定理都不是仅仅是逻辑公理的结果，也不是在建设性逻辑中假定的类似选择的公理，因此$ \ Mathsf {ct} $似乎仅与经典逻辑和选择公理的组合不一致。我们研究$ \ Mathsf {CT} $的后果及其与Coq类型理论中的几类公理的关系，Coq的类型理论是一种具有构想宇宙的建设性类型理论，该理论既不证明经典的逻辑公理也不是强大的选择公理。 因此，我们对哪个公理可以保留类型理论固有的计算直觉的问题提供了部分答案，而哪些公理直觉肯定不是。该论文也可以读取为类型理论中公理的广泛调查，其中所有结果在COQ证明助手中进行了机械化。
"Church's thesis" ($\mathsf{CT}$) as an axiom in constructive logic states that every total function of type $\mathbb{N} \to \mathbb{N}$ is computable, i.e. definable in a model of computation. $\mathsf{CT}$ is inconsistent in both classical mathematics and in Brouwer's intuitionism since it contradicts Weak König's Lemma and the fan theorem, respectively. Recently, $\mathsf{CT}$ was proved consistent for (univalent) constructive type theory. Since neither Weak König's Lemma nor the fan theorem are a consequence of just logical axioms or just choice-like axioms assumed in constructive logic, it seems likely that $\mathsf{CT}$ is inconsistent only with a combination of classical logic and choice axioms. We study consequences of $\mathsf{CT}$ and its relation to several classes of axioms in Coq's type theory, a constructive type theory with a universe of propositions which does neither prove classical logical axioms nor strong choice axioms. We thereby provide a partial answer to the question which axioms may preserve computational intuitions inherent to type theory, and which certainly do not. The paper can also be read as a broad survey of axioms in type theory, with all results mechanised in the Coq proof assistant.
