一句话：在构造性反推数学中精细分解向下Löwenheim-Skolem定理，提出模糊饮酒者悖论BDP并刻画其与选择公理的关系。
本文在构造性反推数学下重新审视一阶逻辑的向下Löwenheim-Skolem（DLS）定理：每个无限模型都有可数初等子模型。经典基底下该定理等价于依赖选择公理（DC）；作者通过构造性分析给出更细的逻辑分解：在可数选择（CC）下，DLS等价于DC与新识别的排中律片段——模糊饮酒者悖论（BDP）——的合取；不假设CC时，DLS等价于BDP与DC、CC的模糊弱化形式的合取。作者还独立研究BDP与模糊选择公理，表明BDP是不依赖Markov原理的LEM、模糊DC是不依赖CC的DC。结果伴随Coq机器化开发。
In the setting of constructive reverse mathematics, we analyse the downward Löwenheim-Skolem (DLS) theorem of first-order logic, stating that every infinite model has a countable elementary submodel. Refining the well-known equivalence of the DLS theorem to the axiom of dependent choice (DC) over classical base theories, our constructive approach allows for several finer logical decompositions: Just assuming countable choice (CC), the DLS theorem is equivalent to the conjunction of DC with a newly identified fragment of the excluded middle (LEM) that we call the blurred drinker paradox (BDP). Further without CC, the DLS theorem is equivalent to the conjunction of BDP with similarly blurred weakenings of DC and CC. Independently of their connection with the DLS theorem, we also study BDP and the blurred choice axioms on their own, for instance by showing that BDP is LEM without a contribution of Markov's principle and that blurred DC is DC without a contribution of CC. The paper is hyperlinked with an accompanying Coq development.
DOI 原文 ·
@inproceedings{paperbot8659,
title = {The Blurred Drinker Paradox: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem},
author = {Dominik Kirst and Haoyi Zeng},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00073}
}