Authors: Dominik Kirst and Haoyi Zeng

The Löwenheim-Skolem (LS) theorem is a central result about first-order logic, entailing that the formalism is incapable of distinguishing different infinite cardinalities. In particular its so-called downward part (DLS), stating that every infinite model can be turned into a countably infinite model with otherwise the exact same behaviour, can be considered surprising or even paradoxical. Therefore the exact assumptions under which the downward Löwenheim-Skolem (DLS) theorem applies have been analysed thoroughly: From the perspective of (classical) reverse mathematics [?,?], the DLS theorem is equivalent to the dependent choice axiom (DC), a weak form of the axiom of choice, stating that there is a path through every total relation [?,?,?].

An even more informative answer, taking into account the computational content, can be obtained by the perspective of constructive reverse mathematics [?,?]. This programme is concerned with the analysis of logical strength over a constructive meta-theory, i.e. in particular without the law of excluded middle (LEM), stating that \(p\lor\neg p\) for all propositions \(p\), and ideally also without countable choice (CC) [?], a consequence of DC. In that setting, finer logical distinctions become visible and thus one can investigate whether (1) the DLS theorem still follows from DC alone, without any contribution of LEM, and (2) whether it still implies the full strength of DC, without any contribution of CC. We show that neither (1) nor (2) is the case by observing that the DLS theorem requires a fragment of LEM, which we call the blurred drinker paradox, and that it implies only a similarly blurred fragment of DC.