集，选择公理，以及所有这些：一个

Zermelo-Fraenkel集合论与选择公理的不一致性及其对计算复杂性的影响

Inconsistency of the Zermelo-Fraenkel set theory with the axiom of choice and its effects on the computational complexity

本文揭示了Zermelo-Fraenkel集合论与选择公理（ZFC）的矛盾。虽然哥德尔的不完备性定理指出，一个相容的系统不能证明它的相容性，但它们并没有排除使用更强的系统或系统范围之外的方法进行证明。本文证明了无穷集的基数是不可控的和矛盾的。然后，本文指出，皮亚诺算术，或一阶算术，是不一致的，如果所有的公理和公理模式假设在ZFC系统是真的，表明ZFC是不一致的。然后，本文揭示了一些后果，是在计算复杂性理论的范围内。

2016-12-31cs.CCcs.LO

丘奇命题与柯克类型论中的相关公理

Church's thesis and related axioms in Coq's type theory

“Church's thesis”（$\mathsf{CT}$）作为构造性逻辑中的一个公理指出，每个$\mathbb{N} \to \mathbb{N}$类型的全函数都是可计算的，即在计算模型中是可定义的。$\mathsf{CT}$在经典数学和布劳威尔的直觉主义中都是不一致的，因为它分别与弱柯尼希引理和扇形定理相矛盾。最近，$\mathsf{CT}$被证明是一致的（单价）建设性类型论。由于弱柯尼希引理和扇形定理都不是构造性逻辑中假设的逻辑公理或选择类公理的结果，所以$\mathsf{CT}$似乎只与经典逻辑和选择公理的组合不一致。我们研究的后果$\mathsf{CT}$和它的关系，几类公理在Coq的类型论，建设性的类型论与宇宙的命题，既不证明经典的逻辑公理，也不强选择公理。因此，我们对以下问题提供了部分答案：哪些公理可以保留类型论固有的计算直觉，哪些公理肯定不能。该文件也可以阅读作为一个广泛的调查公理在类型论，所有结果机械化的Coq证明助手。

2020-11-03cs.LO

以最小元为兜底的集合线性序下受限选择的公理体系

Axiomatics of Restricted Choices by Linear Orders of Sets with Minimum as Fallback

University of Hagen, Germany（海德根大学）；University of Madeira（马德拉大学）；NOVA-LINCS, Portugal（NOVA-LINCS）；University of Cape Town（开普敦大学）

针对潜在选择集合受限场景下难以通过备选方案关系构建选择函数的问题，提出用带最小兜底元的集合线性序构建选择函数的方法，给出一般及并封闭场景下的公理体系，并探讨其在知识表示等领域的应用。

2025-09-04cs.AIcs.LO

模糊饮酒悖论与模糊选择公理：向下洛文海姆-斯科伦定理的构造性反反数学

Blurred Drinker Paradoxes and Blurred Choice Axioms: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem

Inria Paris, France（法国国家信息与自动化研究所巴黎分部）；Ben-Gurion University, Israel（以色列本-古里安大学）；Saarland University, Germany（德国萨尔兰大学）

本文探讨了构造性反反数学中向下洛文海姆-斯科伦定理的逻辑分解，揭示了模糊饮酒悖论与模糊选择公理在不同公理体系下的等价关系。

2026-09-24cs.LO

关系的指数与核心。应用于关系代数公理化中

The Index and Core of a Relation. With Applications to the Axiomatics of Relation Algebra

University of Nottingham（诺丁汉大学）

本文提出关系的指数与核心概念，并探讨其在关系代数公理化中的应用，证明了某些定理及『全或无』公理的可推导性。

2025-12-22cs.LO

论若干等价于选择公理的极大性与良基性原理的逻辑结构

On the logical structure of some maximality and well-foundedness principles equivalent to choice principles

本研究分析等价于选择公理的Teichmüller-Tukey引理的逻辑结构，证明其对应更新归纳向任意基数的推广，提出等价选择公理的极大性与良基性原理一般形式，并初步与Brede等提出的相关原理类做比较。

2024-05-16cs.LOmath.LO

扩展理性选择行为：具有选择对应的布尔集合论决策问题

Extending rational choice behavior: The decision problem for Boolean set theory with a choice correspondence

给定备选项集合$U$的所有非空子集的族$P$，对$U$的选择是函数$c \colon Ω\to P$，使得对于所有菜单$B \in Ω$为$Ω\subseteq P$和$c(B) \subseteq B$。如果选择$Ω= P$，则选择全部，否则选择部分。在经济学中，当一个代理人的选择行为满足适当的一致性公理时，她就被认为是理性的，一致性公理是在菜单上量化的属性。在这里，我们解决以下提升问题：给定一个部分选择满足一个或多个公理的一致性，是否有可能将其扩展到一个总的选择满足相同的公理？在刻画了经济学文献中一些著名的选择性质的提升之后，我们研究了集合论的一个基本片段的未量化公式的连通可满足性问题的可判定性，其中涉及到选择函数符号、布尔集合算子、单例、等式和包含谓词以及命题连接词.在两种情况下，我们证明了可满足性问题是NP-完全的，而在其余的情况下，我们得到NP-完全的额外的假设下，选择条款的数量是常数。

2022-12-02cs.LO

参数化丘奇论文：没有选择的综合可计算性

Parametric Church's Thesis: Synthetic Computability without Choice

在Richman、Bridges和Bauer开创的综合可计算性中，人们在没有明确计算模型的情况下发展了可计算性理论。这是通过假设一个公理等价于假定一个函数$ϕ$对于空间$\mathbb{N}\to\mathbb{N}$是泛在的（$\mathsf{CT}_ϕ$，构造主义公理$\mathsf{CT}$的一个推论），马尔可夫原理，以及至少可数选择公理。假设$\mathsf{CT}$和可数选择使排中律失效，从而也使可计算性教科书中流行的经典直觉失效。另一方面，像赖斯定理这样的结果在没有选择的情况下是不可证明的。与现有的工作相比，我们的调查建设性的类型论与一个单独的，不可预测的宇宙的命题可数的选择不成立，因此先验$\mathsf{CT}_ϕ$和法律的排中律似乎是一致的。我们引入各种参数的加强$\mathsf{CT}_ϕ$，这相当于假设$\mathsf{CT}_ϕ$和$S^m_n$运营商的$ϕ$一样，在$S^m_n$定理。加强公理允许发展合成可计算性理论没有选择，如赖斯定理的优雅的合成证明所示。此外，它们似乎与经典直觉并不冲突，因为它们是$\mathsf{CT}$的传统分析形式的结果。除了解释新的公理和赖斯定理的证明，我们贡献的Coq证明助手的所有结果的机器检查证明。

2021-12-22cs.LOmath.LO

神经证明嵌入中选择公理的几何测量

Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

Rodrigo Mendoza-Smith（罗德里戈·门多萨-史密斯）

通过Lean 4内核级公理依赖追踪，发现选择公理在证明空间中具有可测量的几何关联，服从单参数混合律，并影响神经定理证明器性能。

2026-06-26cs.AIcs.LGcs.LO

关系上的 Thins 序

The Thins Ordering on Relations

本文在关系上定义了一种称为 thins 序的偏序，证明所提出的受限选择公理等价于核关系为该序的极小元，并刻画了其极大元，从而为关系上的无点推理提供了新的理论支持。

2024-07-01cs.LO

具有选择对应的布尔集合论的可满足性问题

The Satisfiability Problem for Boolean Set Theory with a Choice Correspondence

给定一个备选集U，U上的选择（对应）是定义在U的非空子集族Ω上的压缩映射c。在语义上，选项c将Ω中的每个菜单A关联到A的非空子集c（A），该子集包括A的被认为可由代理选择的所有元素。一个关于U的选择是全的，如果它的定义域是U的幂集减去空集，否则是部分的。根据显示偏好理论，如果一个选择可以从U上的二元关系中通过获取每个菜单的所有最大元素来检索，则该选择是可合理化的。众所周知，合理化选择的特点是满足适当的一致性公理，这编纂了菜单中选择的逻辑规则。例如，WARP（弱显示偏好公理）通过传递关系来表征可合理化的选择。在这里，我们研究了集合论的一个基本片段的未量化公式的可满足性问题，涉及选择函数符号c，布尔集运算符和单例，等式和包含谓词，以及命题连接词。特别是，我们考虑的情况下，其中的解释c满足任何组合的两个特定公理的一致性，其结合是等价于WARP。在两种情况下，我们证明了相关的可满足性问题是NP-完全的，而在其余的情况下，我们得到NP-完全的额外的假设下，选择条款的数量是常数。

2017-09-07cs.LO

经典可实现性中的Bar递归：依赖选择与连续统假设

Bar recursion in classical realisability : dependent choice and continuum hypothesis

本文在经典可实现性的背景下讨论了棒递归算子。在Berardi，Bezem & Coquand [1]，T. Streicher在[10]中利用他们的棒递归算子证明了由$λ$ -演算（Scott域，相干空间，. . .),满足依赖选择公理。我们给出了这个结果的证明，使用经典的可实现性的工具。此外，我们还证明了这些可实现性模型满足$\mathbb{R}$的良序性和连续性假设。因此，这些公式是由封闭的$λ_c$ -项实现的。这允许获得程序证明算术公式使用所有这些公理。

2016-05-16cs.LOmath.LO

依赖选择作为终止原则

Dependent choice as a termination principle

我们引入了一个新的配方的公理依赖的选择，可以被看作是一个抽象的终止原则，概括的递归路径排序用于建立终止重写系统。我们认为我们的终止原理的几个变种，并将它们与文献中的一般终止定理。

2019-02-25cs.LOmath.LO