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.

翻译：在构造性逆向数学的框架下，我们分析一阶逻辑的向下Löwenheim-Skolem（DLS）定理，该定理断言每个无限模型都存在一个可数初等子模型。相较于经典基础理论中DLS定理与依赖选择公理（DC）的已知等价关系，我们的构造性方法允许更精细的逻辑分解：仅假设可数选择公理（CC）时，DLS定理等价于DC与新识别出的排中律（LEM）片段（我们称之为模糊饮酒者悖论（BDP））的合取。进一步在不假设CC的情况下，DLS定理等价于BDP与类似模糊化的DC及CC弱化形式的合取。独立于其与DLS定理的关联，我们也单独研究BDP与模糊选择公理，例如证明BDP是不包含马尔可夫原理贡献的LEM，而模糊DC是不包含CC贡献的DC。本文附有超链接至配套的Coq开发项目。