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 ∨ ¬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.

Arboreal categories provide an axiomatic framework in which abstract notions of bisimilarity and back-and-forth games can be defined. They act on extensional categories, typically consisting of relational structures, via arboreal adjunctions. In the examples, equivalence of structures in various fragments of infinitary first-order logic can be captured by transferring bisimilarity along the adjunction. In most applications, the categories involved are locally finitely presentable and the adjunctions finitely accessible. Drawing on this insight, we identify the expressive power of this class of adjunctions. We show that the ranks of back-and-forth games in the arboreal category are definable by formulae à la Hintikka. Thus, the relation between extensional objects induced by bisimilarity is always coarser than equivalence in infinitary first-order logic. Our approach relies on Gabriel-Ulmer duality for locally finitely presentable categories, and Hodges’ word-constructions.