Blurred Drinker Paradoxes and Blurred Choice Axioms: Constructive Reverse Mathematics of the Downward L\"owenheim-Skolem Theorem

TL;DR

This paper explores the constructive reverse mathematics of the downward L"owenheim-Skolem theorem, revealing new logical equivalences involving blurred choice axioms and the blurred drinker paradox, with formal verification in Coq.

Contribution

It introduces the blurred drinker paradox and blurred choice axioms, providing finer logical decompositions of the downward L"owenheim-Skolem theorem in constructive reverse mathematics.

Findings

DLS theorem equivalent to DC plus BDP under countable choice

BDP is LEM without Markov's principle

Blurred DC is DC without countable choice

Abstract

In the setting of constructive reverse mathematics, we analyse the downward L\"owenheim-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.