# A formalization of the downward Löwenheim-Skolem theorem in Coq

Timothée Huneau

<figure><img src="image_1.png" /></figure>

## To cite this version:

Timothée Huneau. A formalization of the downward Löwenheim-Skolem theorem in Coq. Mathematics [math]. 2025. hal-05467238

HAL Id: hal-05467238

https://inria.hal.science/hal-05467238v1

Submitted on 21 Jan 2026

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
A formalization of the downward
Löwenheim–Skolem theorem in Coq

Timothée Huneau

Under the supervision of Yannick Forster and Dominik Kirst
Inria Paris

April 2025 – July 2025

2nd year internship thesis for the Mathématiques Avancées master
Université Claude Bernard Lyon I

Abstract

This internship is about a core theorem of model theory: the downward Löwenheim–Skolem (DLS) theorem, stating that one cannot force, using first-order formulas only, a mathematical structure to have a specified infinite cardinal. Its usual proofs rely on the axiom of choice (AC) and the law of excluded middle (LEM), two related principle said to be non-constructive.

Espíndola [9] and Karagila [14] studied the dependence of the DLS on AC. Kirst and Zeng [15] studied the dependence of a weak form of the DLS on LEM and AC. We have in mind the future goal of extending both of these results to the dependence between the DLS and both LEM and AC.

We provide a constructive formalization in Rocq, up to some non-
constructive prerequisites, of a proof of the DLS theorem. The strategy
we use is similar to that of Button and Walsh [4] and Skolem's original
one [19].
# Contents

<table><tr><td>I</td><td>Introduction</td><td>3</td></tr><tr><td></td><td>I.1 Overview</td><td>3</td></tr><tr><td></td><td>I.2 Outline</td><td>5</td></tr><tr><td>II</td><td>Definitions and formalism of type theory</td><td>6</td></tr><tr><td></td><td>II.1 Types, propositions, functions, implications</td><td>6</td></tr><tr><td></td><td>II.2 Existential statements and proof irrelevance</td><td>7</td></tr><tr><td></td><td>II.3 The axiom of choice</td><td>8</td></tr><tr><td></td><td>II.4 Sets and subsets</td><td>8</td></tr><tr><td></td><td>II.5 Functional extensionality</td><td>9</td></tr><tr><td>III</td><td>Model theory</td><td>9</td></tr><tr><td></td><td>III.1 Syntax</td><td>9</td></tr><tr><td></td><td>III.2 Semantics</td><td>11</td></tr><tr><td></td><td>III.3 Elementary equivalences, embeddings and submodels</td><td>12</td></tr><tr><td>IV</td><td>Sizes and infinity</td><td>14</td></tr><tr><td></td><td>IV.1 Less-than relations</td><td>14</td></tr><tr><td></td><td>IV.2 Infinity</td><td>16</td></tr><tr><td></td><td>IV.3 Application to model theory</td><td>17</td></tr><tr><td>V</td><td>The DLS theorem</td><td>17</td></tr><tr><td></td><td>V.1 Skolem and Tarski-Vaught functions</td><td>17</td></tr><tr><td></td><td>V.2 Function and Tarski-Vaught-closed sets</td><td>19</td></tr><tr><td></td><td>V.3 Step operators</td><td>20</td></tr><tr><td></td><td>V.4 Elementary submodel</td><td>22</td></tr><tr><td></td><td>V.5 Size boundedness</td><td>23</td></tr><tr><td>VI</td><td>Related work</td><td>24</td></tr><tr><td></td><td>VI.1 The classical DLS theorem in ZF</td><td>24</td></tr><tr><td></td><td>VI.2 In Rocq</td><td>25</td></tr><tr><td></td><td>VI.3 In other proof assistants</td><td>26</td></tr><tr><td>A</td><td>Variants of the DLS theorem</td><td>28</td></tr></table>
# I Introduction

## I.1 Overview

The Löwenheim-Skolem (LS) theorem is a theorem about a phenomenon of first-order logic: theories within this logic cannot distinguish between models of different infinite cardinalities. We will here be interested in the downward part of the Löwenheim-Skolem theorem (DLS), stating that for any signature $Σ$, any infinite model of this signature admits an elementary submodel of size at most $|Σ| + |N|$: a theory cannot force all of its models to be of a precise cardinality. Our goal is to provide a formalization of a proof of that theorem in Rocq, given some assumptions hold. We will dedicate this introduction to explaining these first sentences, that may not be clear to the reader as of now. The strategy we chose is akin to the one found in a book by Button and Walsh [4] with a key element, Skolem functions, coming from Skolem's original proof [19].

A consequence of the DLS theorem is Skolem's paradox [25, p. 290]. Set theory is expressable within first-order logics, with a single symbol ($∈$) and a few axioms. The theory of sets proves that, in any of its models, there exists a set $ω$ of natural numbers as well as a set $P(ω)$ of all subsets of $ω$. Within this same theory, it is also provable that $P(ω)$ is not in bijection with $ω$ and that all elements of $P(ω)$ are sets. Set theory has an infinite model, so by using the DLS theorem, set theory has a model $V$ of countable size, within which $ω$ and $P(ω)$ must be definable, but not in bijection. The solution to this apparent paradox it to remark that one definition of countable is meant as the existence of a bijection between the natural numbers and $V$ outside of $V$, while the other is the existence of a bijection between $ω$ and $P(ω)$ within $V$. It is indeed possible that $V$ contains no bijection between $ω$ and $P(ω)$, while the objects used to model them are in external bijection.

The usual framework for doing mathematics, including model theory and hence, proving the DLS theorem, is Zermelo-Fraenkel set theory with the axiom of choice (ZFC). The axiom of choice (AC) is a rather ubiquitous axiom, that we will not state clearly yet, having many equivalent forms: Zorn's lemma, Zermelo's well-ordering theorem, ... and many weaker variants: dependent choice (DC), choice up to a cardinal $κ$ ($κ$-AC), unique choice, ... One can look into the book of Howard and Rubin [12] for a wide survey of principles and theorems related to AC; the work of Herrlich [11] also provides a range of unexpected consequences of both the presence and absence of AC.

The field of reverse mathematics, in which this thesis falls, can be defined as looking for the optimal hypotheses of some proposition: understanding the requirements for a theorem to hold, as well as, assuming a theorem holds, finding out what it entails. The best result is achieved when an equivalence is proved. One of the first questions of this kind to be answered is about the relation between AC and Zermelo's well-ordering theorem. Indeed, Zermelo's proofs [28, 27] led to a controversy [10] over the use of AC; it was later proved that, when using only Zermelo-Fraenkel axioms for set theory (ZF) without AC, AC and Zermelo's well-ordering theorem are equivalent.
Reverse mathematics was already carried out for the full DLS theorem as well as some of its variants [9, 14].<fnref n="1" /> The Löwenheim theorem<fnref n="2" /> is such a weaker variant, stating that any infinite model admits an elementarily equivalent model of size $|\Sigma|+\aleph_0$. It was pointed out by Skolem in 1920 that, within ZF, AC implies the DLS theorem [19] [25, pp. 252-263] and then again Skolem proved in 1922 without using AC that the Löwenheim's theorem holds [25, pp. 290-301]. It was later remarked<fnref n="3" /> that the DLS theorem is equivalent to AC [14]. These questions of dependence between some principles leads to a need for weak base settings, in which these principles can be analyzed, where one can study the dependence of a theorem on AC or its weaker forms.

It is possible to work in an even weaker setting than ZF: constructive mathematics. Classically, to prove a proposition $P$, one can simply deduce a contradiction from assuming $\neg P$ and apply the principle of double negation elimination (DNE), stating $\neg\neg P \rightarrow P$. Another related principle is that if $P \rightarrow Q$ and $\neg P \rightarrow Q$ both hold, then $Q$ holds. These principles stem from what is called the law of excluded middle (LEM), stating that for any proposition $P$, $P \lor \neg P$ holds. We call any logic assuming LEM classical.

Constructive mathematics is obtained by removing LEM from the classical logic rules. Many domains of mathematics can be made constructive, by working without LEM. For instance, one can do constructive reverse mathematics. In this new, constructive, setting, LEM and DNE are equivalent. Notably, any result true in constructive mathematics is also true in classical mathematics.

Constructive logic has a great advantage: one actually *constructs* objects. Indeed, to show an existential statement, one has to provide a witness, the mere proof that the absence of such an object would be absurd is not sufficient; to show a disjunction, one has to effectively provide a proof of one of the cases. An example of that is the usual proof that there exists two irrational numbers $a$ and $b$ so that $a^b$ is rational, using LEM. We know $\sqrt{2}$ is irrational. Then, either $\sqrt{2}^{\sqrt{2}}$ is rational and we put $a = b := \sqrt{2}$, or it is not and we put $b := \sqrt{2}$ and $a := \sqrt{2}^{\sqrt{2}}$. Remarkably, the proof does not tell which value of $a$ works; nonetheless, there are other proofs of that fact, some yielding a more constructive result.

Kirst and Zeng have already partly analyzed DLS from a constructive reverse mathematical point of view. Namely, they have shown that for any countable signature $\Sigma$, the DLS theorem for models of signature $\Sigma$ is equivalent to the conjunction of four logical principles weaker than LEM and AC; see their work [15, Theorem 8.1] for the detailed statement.

Working out reverse mathematics is difficult when using only pen and paper. It requires to keep track of every lemma and assumption used. In constructive reverse mathematics, some classically equivalent definitions can even

<footnote n="1">¹Naming of said variants throughout the literature is inconsistent, as some authors refer to different, non-equivalent, theorems by the same name.</footnote>

<footnote n="2">²Sometimes confusingly also called DLS theorem [6].</footnote>

<footnote n="3">³It is difficult to establish who first proved that result, some attribute it to Vaught [26], although he does not seem to prove the same result.</footnote>
become constructively distinct, for instance, there are many constructively non-
equivalent definitions of “finite” [20], all becoming equivalent within a classical
setting. A useful tool for carrying out reverse mathematics, and especially con-
structive reverse mathematics, is a proof assistant: a software that checks the
validity of a proof. The ability to change only a piece of a proof and then having
the software automatically rechecking the whole proof is of great help. We use
Rocq [24] as our proof assistant. This means that we have in mind the calculus
of inductive constructions as the underlying framework [7].

The aim of this internship was then to work toward the general case of reverse
mathematics of the DLS, to extend the recent result of Kirst and Zeng [15]. Since
their proof method cannot scale to arbitrary signatures, a subgoal was to give
a general statement of the DLS theorem, another was to give a proof of it on
paper and then in Rocq.

I.2 Outline

Section I, this introduction, is dedicated to explaining the context of this work
and its broad outline.

In Section II, we will recall some definitions of type theory.

In Section III, we explain the framework used for doing model theory inside
type theory. Section IV is about specifications for comparing sizes of types
through a cardinal-like ordering, as well as a definition of infiniteness.

The heart of this work is Section V: it contains the exact statement of the
DLS as well as the proof of our main result, step by step.

Finally, Section VI is about related works, from a historical point of view as
well as current work around it.

Appendix A gives a quick overview of the variety of statements called DLS theorem by different authors.
## II Definitions and formalism of type theory

Although it can be transposed in any constructive setting, we will provide a concrete instance of our work in constructive type theory, of which a model is the calculus of inductive constructions (CIC). In this setting, terms t inhabit types T, denoted by “t : T”.

We consider Prop the type of propositions, such that Prop is a type. Any proposition P : Prop is a special kind of type and is inhabited by its proofs.

### II.1 Types, propositions, functions, implications

We quickly recall the core of type theory: functions. Given X, Y : Type, the type of functions from X to Y is denoted by $X \to Y$. Its inhabitants are of the form$^4$ $x \mapsto y$, where $y : Y$ can depend on the input $x$. Given $Y : X \to Type$, we can build the type of dependent functions $\forall x : X. Y(x)$. Its inhabitants are also of the form $x \mapsto y$, but with the type of $y$ also depending on $x$. Note that this means that $X \to Y$ is an abbreviation of $\forall x : X. Y$ for $X, Y : Type$.

An example of a type is $\mathbb{N}$, the type of natural numbers. Given a type $X$ and a number $n$, one can build the type $V_n(X)$ of vectors of length $n$ of elements of $X$. An inhabitant of $Type \to \mathbb{N} \to Type$ is, for instance, $X \mapsto (n \mapsto V_n(X))$. An inhabitant of $X \to (\forall n, V_n(X))$ is $x_0 \mapsto (n \mapsto (x_0; \dots; x_0))$, with $n$ occurrences of $x_0$ in the output.

Given $n : \mathbb{N}$ and $X, Y : Type$, we can consider the function map : ($X \to Y) \to V_n(X) \to V_n(Y)$. It takes a function $f : X \to Y$ as input and is so that (map $f$) takes a vector $v$ of $X$ and outputs the vector where $f$ has been applied to all components of $v$.

A function can be defined on Type. For instance, the binary sum $X + Y$ of two types $X$ and $Y$ is well-defined. This makes + a function of type $Type \to Type \to Type$. Note that an inhabitant of $X + Y$ is either from the left type or the right one.

An important piece of our setting is the Curry-Howard correspondence: given $P, Q : Prop$, we can consider the proposition $P \to Q$, read as “P implies Q”. The same symbol is used for implications and functions, because inhabitants of an implication $P \to Q$ can be thought of as ways to transform a proof of $P$ into a proof of $Q$. In that sense, they are functions. Note that a proof $f$ of some proposition $P \to Q$ does not need $P$ to have a proof, it just says that if $p$ is a proof of $P$, then $f(p)$ is a proof of $Q$.

A useful property of Prop is its impredicativity: a proposition can quantify over all propositions, including itself.

**Example 1.** *The proposition*

$$ \perp := \forall P : \mathbf{Prop}. P $$

is a well-defined proposition. A proof of $\perp$ would be a function, taking as input any proposition $P$ and outputting a proof of $P$. In other words, $\perp$ states that

<footnote>$^4$In theoretical computer science, one often uses the notation $\lambda x. y$.</footnote>
any proposition is provable. Nonetheless, $\perp$ has no proof,<fnref n="5" /> so it can be used as the False proposition.

Likewise, the proposition

$$ \top := \forall P : \mathbf{Prop}. \perp \to P $$

is well-defined. This time, it is provable. Indeed, given $P : \mathbf{Prop}$, we need to exhibit a term of type $\perp \to P$. We consider the function taking any $f : \perp$ as input and outputting $f(P)$; indeed we can apply $f$ to $P$, yielding a term of $P$.

Propositions being first-class objects just like types, we can also have functions from a type to a proposition.

## II.2 Existential statements and proof irrelevance

There is a main difference between **Prop** and **Type**: how one can eliminate their terms to create new terms. By eliminating, we mean extracting the data used to build a term and using it to create a new term. For $X : \mathbf{Type}$ and $x : X$, $x$ can be eliminated into a term of a type or a proof of a proposition. On the other hand, for $P : \mathbf{Prop}$ and $p : P$, $p$ can only be eliminated into a proof of a proposition. $\Sigma$-types and existential propositions, as well as being prominently used in this work, provide a good example of the previous fact.

**Definition 1.** Given $X : \mathbf{Type}$ and a function $P : X \to \mathbf{Type}$, we build the $\Sigma$-type $\sum_{x:X} P(x) : \mathbf{Type}$. A term of such a type is a dependent pair $(x; p_x)$, where $x : X$ and $p_x : P(x)$.

When $P$ is a predicate, we may call that $\Sigma$-type construction a subtype. Existential propositions are built similarly.

**Definition 2.** Given $X : \mathbf{Type}$ and a predicate $P : X \to \mathbf{Prop}$, we build the existentially quantified proposition $\exists x : X. P(x) : \mathbf{Prop}$. A proof of such an existential statement is made out of $x : X$ and $p_x : P(x)$, we shall denote it by $\langle x; p_x \rangle$.

Given $X : \mathbf{Type}$ and $P : X \to \mathbf{Prop}$ a predicate on that type, given $x, x' : X$ so and $p : P(x)$ and $p' : P(x')$, we have $\langle x; p \rangle, \langle x'; p' \rangle : \sum_{y:X} P(y)$ and $\langle x; p \rangle, \langle x'; p' \rangle : \exists y. P(y)$. Saying that terms of a type can be eliminated into a proof means that the function $\langle x_0; p_0 \rangle \mapsto \langle x_0; p_0 \rangle : \sum_{y:X} P(y) \to \exists y. P(y)$ is well defined whereas the fact that a proof cannot be eliminated into a non-proof term means that $\langle x_0; p_0 \rangle \mapsto \langle x_0; p_0 \rangle : \exists y. P(y) \to \sum_{y:X} P(y)$ is ill-defined.

Proof irrelevance (PI) states that all proofs of a given proposition are identical. Formally, it is the following proposition:

$$ \forall P : \mathbf{Prop}. \forall p_1, p_2 : P. p_1 = p_2 $$

The seemingly limiting rule on elimination allows to assume PI as an axiom. For a given type $X$ with $x, x' : X$ and $x \neq x'$ and a predicate $P : X \to \mathbf{Prop}$

<footnote n="5">⁵This allows our setting to remain consistent.</footnote>
holding on $x$ and $x'$ thanks to proofs $p : P(x)$ and $p' : P(x')$, the function $\pi := \langle\langle y; q \rangle\rangle \mapsto y$ of type $\exists y : X. P(y) \to X$ was cannot be well-defined, since we would have $\langle\langle x; p \rangle\rangle = \langle\langle x'; p' \rangle\rangle$ due to PI but $\pi(\langle\langle x; p \rangle\rangle) = x \neq x' = \pi(\langle\langle x'; p' \rangle\rangle)$.

## II.3 The axiom of choice

We now define AC.

**Principle 1.** AC is stated as follows:

$$ \forall J, X : \text{Type.} $$

$$ \forall R : J \to X \to \text{Prop.} $$

$$ (\forall j : J. \exists x : X. R(j)(x)) \to (\exists f : J \to X. \forall j : J. R(j)(f(j))) $$

This formulation of AC states that if one has a family indexed by a type $J$ of non-empty sets of a type $X$, then it is possible to choose an element of each of them at once, yet without providing a function to do so.

Importantly, we do not assume it as an axiom but rather consider it as a regular proposition, that could hold or not, as well as be a premise or a conclusion of some bigger proposition.

## II.4 Sets and subsets

One can define sets within a type. A function from a type to **Prop** is called a predicate. For the purpose of this section, we fix a type $X$.

**Definition 3.** A set of $X$ is a $\sum$-type of the form $\sum_{x:X} P(x)$ where $P : X \to \text{Prop}$ is a predicate on $X$.

Given $A$ and $B$ two sets of $X$ with predicates $P$ and $Q$, one can consider their binary union $A \cup B := \sum_{x:X}(P(x) \lor Q(x))$ and their binary intersection $A \cap B := \sum_{x:X}(P(x) \land Q(x))$. The proposition $A \subseteq B$ is defined as $\forall x. P(x) \to Q(x)$. The equality between sets is up to equivalence of their predicate, we denote$^6$ $A = B$, even though $A$ and $B$ are not strictly equal, whenever $\forall x. P(x) \leftrightarrow Q(x)$.

If $A$ is a subset of $B$, then we have a proof $f : \forall x. P(x) \to Q(x)$, hence we can define the function $\iota : A \to B$ by $\langle x; p_x \rangle \mapsto \langle x; f(x)(p_x) \rangle$, called the inclusion map. By abuse of notation, we sometimes make $\iota$ implicit to keep things readable. For any $x : X$, we write $x \in A$ to denote the fact that $P(x)$ holds.

There is always a full set, defined as $\sum_{x:X} \top$ and an empty set, defined by $\sum_{x:X} \bot$. We sometimes denote the full set of $X$ by $X$, although they are not the same objects.

As there is a correspondence between sets and predicates, we denote $P(X) := X \to \text{Prop}$ the type of sets of $X$. A family of sets of $X$ indexed by a type $J$ is a function of type $J \to P(X)$. We consider the union and intersection of such families.

<footnote>$^6$Hence, we overload the $=$ notation.</footnote>
**Definition 4.** The union of a family $A: J \to \mathcal{P}(X)$ of sets of $X$, denoted by $\bigcup_{j:J} A(j)$ is the set defined by the predicate:

$$x \mapsto (\exists j : J. A(j)(x))$$

The intersection of the same family is denoted by $\bigcap_{j:J} A(j)$ and defined by

$$x \mapsto (\forall j : J. A(j)(x))$$

## II.5 Functional extensionality

We now wish to add an additional axiom that is independent of those discussed earlier.

Functional extensionality (FE) states that a function is entirely defined by its values. Formally, it is stated by the following proposition:

$$\forall X, Y : \text{Type}. \forall f, g : X \to Y. (\forall x. f(x) = g(x)) \to f = g$$

FE follows from the axioms of set theory, but it is not always assumed in type theory.<fnref n="7" />

In this work, we assume and use it without always saying so.

# III Model theory

As explained by Tarski [22], model theory aims to separate the syntax from semantics. We first define what is a formula with inductively and then, the question of whether it can be true in some setting is raised.

## III.1 Syntax

The goal of a signature is to define the abstract symbols one can use in a given setting.

**Definition 5.** A signature is given by two types $\Sigma_f$ and $\Sigma_P$ together with an arity function $\text{ar} : \Sigma_f + \Sigma_P \to \mathbb{N}$ (and we denote also by $\text{ar}$ the associated functions $\Sigma_f \to \mathbb{N}$ and $\Sigma_P \to \mathbb{N}$); terms $f : \Sigma_f$ are called function symbols and have an arity $\text{ar}(f)$ and terms $P : \Sigma_P$ are called predicate symbols and have an arity $\text{ar}(P)$.

Although a signature bears no intrinsic meaning outside of a further defined context, some are commonly named.

**Example 2.** A possible signature is given by the following four function symbols: $0, s, +, \times$, with $\text{ar}(0) = 0$, $\text{ar}(s) = 1$ and $\text{ar}(+) = \text{ar}(\times) = 2$ and one predicate symbol = of arity 2. We call this signature $\Sigma_{PA}$ the signature of Peano arithmetic.

<footnote n="7">⁷One can be interested in function intentionality.</footnote>
We extend the previously defined function $\nu$ to formulas, so that for all $j \ge \nu(\varphi)$, $x_j$ does not appear as a free variable in $\varphi$. A formula $\varphi$ is then closed if $\nu(\varphi) = 0$ Note that there is, like for terms, also always an injection $\psi$ from $\mathbb{N}$ to $\mathbb{F}$, for instance sending $0 \mapsto \bot$ and $\psi(n+1) := \dot{\forall}\psi(n)$.

**Example 4.** Continuing Example 3, $(s[x_0] = 0) \stackrel{\cdot}{\rightarrow} \bot$ is an open formula, as well as $\dot{\forall}(s[x_0] = s[x_1] \rightarrow x_0 = x_1)$, $s[x_0] = x_0$, ... The formulas $\dot{\forall}\dot{\forall}(x_0 + s[x_1] = s[x_0 + x_1])$, $\dot{\forall}((\exists(x_1 = s[x_0])) \rightarrow ((x_1 = 0) \rightarrow \bot))$, ... are closed formulas.

### III.2 Semantics

The syntactic part being now set up, we can define the semantics, starting with the core of model theory: models.

**Definition 8.** A model $\mathcal{M}$ is a type $M$ (the domain) alongside interpretations of symbols: for all $f : \Sigma_f$, we have $f^\mathcal{M} : V_{\text{ar}(f)}(M) \to M$; for all $P : \Sigma_P$, we have $P^\mathcal{M} : V_{\text{ar}(P)}(M) \to \text{Prop}$.

**Example 5.** Continuing Example 4, we can endow the type $\mathbb{N}$ with a model in $\Sigma_{PA}$, call it $\mathcal{N}$. We interpret $0^\mathcal{N}$ by the element $0 : \mathbb{N}$. We give the symbol $+$ : $\Sigma_f$ its usual meaning of addition, and $\times$ its meaning of multiplication. We interpret $s^\mathcal{N} := n \mapsto n + 1$. Finally, we interpret $=$ as the equality in $\mathbb{N}$. This gives rise to what is called the standard model of Peano arithmetic.

Note that we gave one interpretation of the signature, but many other are possible. We could, with the same signature $\Sigma_{PA}$, have a model $\mathcal{Z}$ of domain $\mathbb{Z}$, with $0, +, \times, s$ and $=$ interpreted as zero, addition, multiplication, successor and equality. Understanding how $\mathcal{N}$ and $\mathcal{Z}$ differ can be done by understanding which formulas are true in which model.

An environment on $X$ is a map $\rho : \mathbb{N} \to X$ and we use the notational short-hand $\text{env}(X) := \mathbb{N} \to X$. For $x : X$ and $\rho : \text{env}(X)$, we build the environment $(x :: \rho) : \text{env}(X)$ as follows: $(x :: \rho)(0) := x$ and $(x :: \rho)(n + 1) := \rho n$. This is shifting all values of $\rho$ up and putting $x$ as its new first element.

Given $\rho : \text{env}(M)$, we define the term evaluation mapping $\hat{\rho} : \mathbb{T} \to M$ recursively, mapping $x_n \mapsto \rho n$ and $f[v] \mapsto f^\mathcal{M}((\text{map } \hat{\rho})(v))$. It can be understood as replacing the placeholder variables by values and then computing with these.

We can finally define formula satisfaction by recursion on the formulas. The satisfaction function $\mathcal{M} \models_\rho \mathbb{T} \to \text{Prop}$, with $\rho : \text{env}(M)$, is defined as follows:

* $\mathcal{M} \models_\rho P[v]$ is $P^\mathcal{M}((\text{map } \hat{\rho})(v))$;

* $\mathcal{M} \models_\rho \varphi \dot{\wedge} \psi$ is $\mathcal{M} \models_\rho \varphi \wedge \mathcal{M} \models_\rho \psi$;

* $\mathcal{M} \models_\rho \varphi \dot{\wedge} \psi$ is $\mathcal{M} \models_\rho \varphi \vee \mathcal{M} \models_\rho \psi$;

* $\mathcal{M} \models_\rho \varphi \rightarrow \psi$ is $\mathcal{M} \models_\rho \varphi \rightarrow \mathcal{M} \models_\rho \psi$;

* $\mathcal{M} \models_\rho \dot{\forall} \varphi$ is $\forall m. \mathcal{M} \models_{m::\rho} \varphi$;

* $\mathcal{M} \models_\rho \exists \varphi$ is $\exists m. \mathcal{M} \models_{m::\rho} \varphi$;
• $\mathcal{M} \models_{\rho} \dot{\perp}$ is $\perp$;

Since a formula can only have a finite amount of variables, the last elements of an environment do not matter for formula satisfaction.

**Definition 9.** Two environments $\rho$ and $\rho'$ are said to be up-to-$n$-equivalent, denoted by $\approx_n$, if:

$$ \rho \approx_n \rho' := \forall j. j \le n \rightarrow \rho(j) = \rho'(j) $$

The $\approx_n$-equivalence classes of env($X$) are in bijection with $\mathcal{V}_n(X)$: for any $n$, the function taking as input an environment and outputting the vector of its first $n$ values is $\approx_n$-invariant.

**Lemma 1.** For any $t: \mathbb{T}$ and and $\rho, \pi: \text{env}(M)$, we have:

$$ \rho \approx_{\nu(t)} \pi \rightarrow \hat{\rho}(t) = \hat{\pi}(t) $$

For any $\varphi: \mathbb{F}$ and $\rho, \pi: \text{env}(M)$, we have:

$$ \rho \approx_{\nu(\varphi)} \pi \rightarrow (\mathcal{M} \models_{\rho} \varphi \leftrightarrow \mathcal{M} \models_{\pi} \varphi) $$

*Proof.* The proof is a straightforward induction, first on terms and then on formulas. $\square$

When the formula $\varphi$ is closed, $\mathcal{M} \models_{\rho} \varphi$ does not depend on $\rho$: there is only one equivalence class for $\approx_0$. In that case, we write $\mathcal{M} \models \varphi$. It follows from Lemma 1.

### III.3 Elementary equivalences, embeddings and submodels

Given two models of our given signature, we can study how they relate to each other. We define three relations on models. Take $\mathcal{M}$ and $\mathcal{N}$ two models of domains $M$ and $N$ of our given signature.

**Definition 10.** We say they are elementarily equivalent if for any closed formula $\varphi$, $\mathcal{M} \models \varphi$ is equivalent to $\mathcal{N} \models \varphi$.

**Definition 11.** We say $\mathcal{N}$ elementarily embeds into $\mathcal{M}$ if there exists a function $h: N \rightarrow M$, called an elementary embedding, such that for any environment $\rho$ and any (not necessarily closed) formula $\varphi$, $\mathcal{N}$ satisfies $\varphi$ in $\rho$ if and only if $\mathcal{M}$ does in $h \circ \rho$; in symbols:

$$ \exists h: N \rightarrow M. \forall \rho: \text{env}(N). \forall \varphi: \mathbb{F}. \mathcal{N} \models_{\rho} \varphi \leftrightarrow \mathcal{M} \models_{h \circ \rho} \varphi $$

**Definition 12.** We say $\mathcal{N}$ is an elementary submodel of $\mathcal{M}$ if $N$ is a set of $M$ and the inclusion map is an elementary embedding.
Nonetheless, if $r$ and $s$ are two mutually transcendental real numbers, $\mathbb{Q}[r]$ and $\mathbb{Q}[s]$ are mutually not embeddable in one another. For any polynomial $P$ with integer coefficients, we can find $x : \mathbb{Q}$ so that $r < x < P(s)$ or $r > x > P(s)$. Hence, if $h$ is a function from $\mathbb{Q}[r]$ to $\mathbb{Q}[s]$, it has to map $\mathbb{Q}$ on $\mathbb{Q}$ identically to be an elementary embedding. Then, $r$ would have to be mapped to $P(s)$ for a non-constant $P$ an polynomial with integer coefficients. Given $x := \frac{p}{q}$ separating $r$ and $P(s)$, we have that the formula $\psi := x_0 \times q < p$ is such that, for the environment $\rho$ constant at $r$, $\mathbb{Q}[r] \models_{\rho} \psi$ holds if and only if $\mathbb{Q}[s] \models_{h \circ \rho} \psi$ does not hold, so $h$ cannot be an elementary embedding. The same reasoning applies for an embedding in the opposite direction. This example comes from [21] □

# IV Sizes and infinity

The usual formulation of the DLS theorem deals with infinite cardinalities. Expressing a notion of cardinals for types in CIC is not easily doable. The closely related notion of ordinals, for instance, is not uniquely defined, as per Kraus, Nordvall Forsberg and Xu [16].

We first seek properties such a notion should meet, properties that can be fulfilled by many distinct notions. That is, we do not define a notion of cardinal ordering, but many such notions. We do so for many reasons: defining cardinals is difficult, the core of this internship was the DLS theorem, it allows to have a constructive proof up to some prerequisite rather than a non-constructive one. Additionally, it allows for a greater generality.

We split these specifications into two parts: first, a cardinal-like ordering, then, infiniteness.

## IV.1 Less-than relations

We define the property, for a relation on types, to be less-than. The aim is to provide a cardinal-like ordering. In set theory, a set $A$ is smaller than another set $B$ if $A$ injects into $B$. Note that the status of Cantor-Bernstein's theorem regarding LEM is unclear, although Pradic and Brown showed this theorem implies LEM in intuitionistic set theory [18]. Thus, in our setting, knowing there are injections both from $A$ to $B$ and from $B$ to $A$ does not necessarily yield a bijection between $A$ and $B$.

**Definition 13.** A relation $\leq$: Type $\rightarrow$ Type $\rightarrow$ Prop is said to be a less-than relation if it has all of the following properties:

1. $\leq$ is reflexive:

$$ \forall X. X \leq X $$
2. $\le$ is transitive:

$$ \forall X, Y, Z. \\ X \leq Y \rightarrow Y \leq Z \rightarrow X \leq Z $$

3. $\le$ follows from the existence of an injection:

$$ \forall X, Y : \text{Type}. \\ (\exists f : X \rightarrow Y. \forall x, x' : X. f(x) = f(x') \rightarrow x = x') \rightarrow \\ X \leq Y $$

4. $\le$ is preserved by binary product:

$$ \forall X, X', Y, Y'. X \leq Y \rightarrow X' \leq Y' \rightarrow X \times X' \leq Y \times Y' $$

5. $\le$ is preserved by the list operator $\mathcal{L}$:

$$ \forall X, Y. X \leq Y \rightarrow \mathcal{L}(X) \leq \mathcal{L}(Y) $$

6. $\le$ is preserved by dependent sums:

$$ \forall J : \text{Type}. \forall X, Y : J \rightarrow \text{Type}. \\ (\forall j : J. X(j) \leq Y(j)) \rightarrow (\sum_{j:J} X(j)) \leq (\sum_{j:J} Y(j)) $$

7. $\le$ follows from changing existential propositions into $\Sigma$-type:

$$ \forall J : \text{Type}. \forall P : J \rightarrow \text{Prop}. \\ (\exists j. P(j)) \leq \sum_{j:J} P(j) $$

Together, the requirements 1 and 2 mean that $\le$ is a preorder. The requirement 3 is a direct translation of the classical notion of cardinal ordering discussed above. The requirements 4, 5 and 6 assert that $\le$ is compatible with some operations on types we chose. The requirement 7 allows to compare an existential proposition with a $\Sigma$-type, even though there could be no function from the proposition to the type. Using PI, it can also be understood as the fact that the existential statement has at most one proof, and if it has a proof, then the $\Sigma$-type is inhabited too.

We only state the next example to show how general the specifications are.

**Example 6.** The relation that always holds, whatever argument it is given, also called the full relation, is a less-than relation. This fact is constructively provable.
**Lemma 4.** For any less-than relation and any type $X$, the following always hold:

$$X + X \leq \mathcal{L}(X)$$

and

$$X \times X \leq \mathcal{L}(X)$$

*Proof.* For any type $X$, we have an injection from $X + X$ to $\mathcal{L}(X)$ and from $X \times X$ to $\mathcal{L}(X)$. The first one maps $x: X + X$ to $[x]$ if $x$ comes from the left and $[x; x]$ if $x$ comes from the right. The second one is $(x; x') \mapsto [x; x']$ of type $X \times X \to \mathcal{L}(X)$. $\square$

## IV.2 Infinity

Given a less-than relation on types, we need to tell which ones are infinite. We will do so using a predicate on types.

**Definition 14.** Given $\leq$ a less-than relation, an infinity predicate is any predicate $I: \text{Type} \to \text{Prop}$ having the following properties:

1. the natural numbers are infinite:

$$I(\mathbb{N})$$

2. infinity is preserved upward:

$$\forall X. I(X) \to \forall Y. X \leq Y \to I(Y)$$

3. it is compatible with lists:

$$\forall X. I(X) \to \mathcal{L}(X) \leq X$$

**Example 7.** Continuing the Example 6, in the case where $\leq$ is the full relation, the only admissible infinity predicate is the full predicate, always provable, since for every $X$, $\mathbb{N} \leq X$ and $I(\mathbb{N})$, so by requirement 2 of the less-than definition, we have $I(X)$. Note that it is compatible with the requirement 3.

A nice feature of this definition is that, given $\leq$ a less-than relation and $I$ an infinity predicate, we have the following lemma:

**Lemma 5.** $I$ is compatible with binary sums and products. In other words, for any $X$, we have:

$$I(X) \to X + X \leq X$$

and

$$I(X) \to X \times X \leq X$$

*Proof.* We use the transitivity of $\leq$ on Lemma 4 and the compatibility of $I$ with lists applied to $X$. $\square$
IV.3 Application to model theory

The next lemma is about infiniteness and sizes of some types specific to model
theory.

**Lemma 6.** For any less-than relation and infinity predicate, the following propositions hold:

1. $N \leq T$, $N \leq F$ and $N \leq T + F$;

2. $I(T), I(F)$ and $I(T + F)$.

*Proof.* We have the following:

1. We already defined injections from $N$ to $T$ and from $N$ to $F$ in Section III.2.
Because $T$ injects into $T + F$, we then have, by transitivity, $N \leq T + F$.

2. Any type bigger than $N$ is infinite, because $N$ is and infinity is preserved
upward, hence proving $I(T)$, $I(F)$ and $I(T + F)$ from the previous point.

□

V The DLS theorem

For a less-than relation $\leq$ and an infinity predicate $I$, we state the proposition $\text{DLS}_M$, given a model $\mathcal{M}$ of a signature $\Sigma$.

**Principle 2.** We define $\text{DLS}_M$ to be the statement that there exists an elementary submodel $\mathcal{N}$ of $\mathcal{M}$, with domain $N \subseteq M$ such that $N \leq T + F$.

As discussed in the Section I, Skolem already gave a proof of this fact, using
AC, in his 1920 article [19, 25]. We discuss the link between different statement
involving the DLS principle in Section VI.

For the purpose of this section, we fix a signature $\Sigma$ and a model $\mathcal{M}$, with
domain $\mathcal{M}$, of the signature $\Sigma$. We assume it is inhabited by some element $m_0$.

Before stating the main result, we need a last ingredient: Tarski–Vaught
functions.

V.1 Skolem and Tarski–Vaught functions

The most common proofs of the DLS theorem are done using what are called
Skolem functions, introduced by Skolem. In a model $\mathcal{M}$, with an environment
$\rho$, the Skolem function associated to a formula $\dot{\forall}(\exists\varphi)$, for $\varphi$ a formula, is a
function $f: M \to M$ so that $\mathcal{M} \models_{\rho} \dot{\forall}(\exists\varphi) \to \forall x. \mathcal{M} \models_{x::f(x)::\rho} \varphi$. This Skolem
function is not uniquely defined.

We give a light variation of Skolem functions, by defining functions collecting
a Skolem function for each environment.
**Definition 15.** A function $F: \mathbb{F} \to \mathrm{env}(M) \to M$ is said to respect formula-environment invariance if:

$$ \forall \varphi : \mathbb{F}. \forall \rho_1, \rho_2 : \mathrm{env}(M). \rho_1 \approx_{\nu(\varphi)} \rho_2 \to F(\varphi)(\rho_1) = F(\varphi)(\rho_2) $$

Namely, for two environments interpreting a formula $\varphi$ the same way, $F(\varphi)$ does not distinguish them.

**Definition 16.** Two functions $F^\forall, F^\exists: \mathbb{F} \to \mathrm{env}(M) \to M$ are said to be Tarski-Vaught if:

* they both respect formula-environment invariance

* for any formula $\varphi$ and environment $\rho$, posing $m := F^\forall(\varphi)(\rho)$, we have

$$ M \models_{m::\rho} \varphi \to M \models_{\rho} \dot{\forall}\varphi $$

* for any formula $\varphi$ and environment $\rho$, posing $m := F^\exists(\varphi)(\rho)$, we have

$$ M \models_{\rho} \dot{\exists}\varphi \to M \models_{m::\rho} \varphi $$

Notice how in these properties, the converse implications always hold. Equiv- alently, the implication could then be required to be an equivalence.

The name Tarski-Vaught comes from the Tarski-Vaught criterion, discov- ered by Tarski and Vaught [23].<fnref n="10" /> This criterion allows to check the elementarity of an embedding $h: N \to M$ between two models $\mathcal{N}$ and $\mathcal{M}$. With classical logic, we have

$$ \mathcal{N} \preceq_h \mathcal{M} \leftrightarrow \forall \varphi : \mathbb{F}. \forall \rho : \mathrm{env}(N). (\mathcal{N} \models_{\rho} \dot{\exists}\varphi \to \exists m : \mathcal{M}. \mathcal{M} \models_{m::h \circ \rho} \varphi) $$

The proof given by Tarski and Vaught is essentially classical. It uses a conse- quence of LEM: the fact that universal quantification can be defined in terms of existential quantification.

We at last state our goal. For that purpose, we fix a less-than relation and an infinity predicate. For the sake of generality, we do not make any more assumptions on them.

**Theorem 1** (DLS via Tarski-Vaught functions). For any inhabited model $\mathcal{M}$, if there exists a pair of Tarski-Vaught functions associated to that $\mathcal{M}$, then DLS$_{\mathcal{M}}$ holds.

The Figure 1 is the proof strategy we follow. The assumption are in gray. The individual steps we follow are in green. The name $A$ refers to a singleton set, we know one exists since $\mathcal{M}$ is inhabited.

From Button and Walsh [4, Theorem 7.2, pp 168-169], we use the idea of constructing an elementary submodel by iterating a step operator countably many times in Section V.3. From Skolem [19, 25], we use Skolem functions.

<footnote n="10">¹⁰In their paper, they say $\mathcal{M}$ is an arithmetical extension of $\mathcal{N}$ where one would, nowadays, say $\mathcal{N}$ is an elementary submodel of $\mathcal{M}$.</footnote>
<figure><img src="image_3.png" /><figcaption>Figure 1: The proof strategy for Theorem 1</figcaption></figure>

The general idea of the proof is to turn a subset of $M$ into an elementary submodel of $\mathcal{M}$. To do so, in Section V.3, we define, using the Tarski–Vaught functions, a step operator from $\mathcal{P}(M)$ to $\mathcal{P}(M)$ and iterate it enough on a singleton set of $M$, so that we show, in Section V.4, that the resulting set is an elementary submodel of $\mathcal{M}$. We then prove in Section V.5 that this set fits the size condition of the statement of the DLS principle.

## V.2 Function and Tarski–Vaught-closed sets

We now assume two such Tarski–Vaught functions $F^\exists$ and $F^\forall$ exists for $\mathcal{M}$ and we fix them until the end of Section V.

**Definition 17.** A set $A := \sum_{m:M} P(m)$ with $P: \mathcal{P}(M)$ is said to be function-closed if for any $f: \Sigma_f$ of arity $n := \mathrm{ar}(f)$ and $a_1, \dots, a_n: A$, we have:

$$f^{\mathcal{M}}(a_1, \dots, a_n) \in A$$

where the inclusion map is hidden.

For a set $A$, being function-closed means being a model of the signature $\Sigma$, but not necessarily an elementary submodel of the bigger model. All symbols are interpreted as the restrictions of their interpretation in $\mathcal{M}$, we call this the inclusion interpretation.
**Definition 18.** A set $A$ is Tarski–Vaught-closed if for any $\varphi : \mathbb{F}$ and $\rho : \mathrm{env}(A)$, we have

$$F^{\forall}(\varphi)(\rho) \in A$$

and

$$F^{\exists}(\varphi)(\rho) \in A$$

**Lemma 7.** Any function- and Tarski–Vaught-closed set $A$ of $M$ is an elementary submodel of $M$.

*Proof.* Take as set $A$ that is function- and Tarski-Vaught-closed. We denote the model on $A$ by $\mathcal{A}$. Take $\rho : \mathrm{env} A$ and denote $\pi := \iota \circ \rho$. Take $\varphi : \mathbb{F}$. We do an induction on $\varphi$ in order to prove that $\mathcal{A} \models_{\rho} \varphi \leftrightarrow \mathcal{M} \models_{\pi} \varphi$:

* If $\varphi$ is an atom of the form $P[t_1; \dots; t_n]$ for $P$ a predicate symbol of arity $n$, then $A \models_{\rho} \varphi \leftrightarrow \mathcal{M} \models_{\pi} \varphi$ unfolds into $P(\hat{\rho}(t_1); \dots; \hat{\rho}(t_n)) \leftrightarrow P(\hat{\pi}(t_1); \dots; \hat{\pi}(t_n))$, which holds since we use the inclusion interpretation.

* If it is a build using a binary operator ($\rightarrow$, $\wedge$ or $\vee$) applied to two smaller formulas for which the induction hypothesis holds, one concludes by definition of the inclusion interpretation.

* Consider a universally quantified formula $\varphi = \dot{\forall}\psi$ such that for all environment $\pi$ over $A$ we have $\mathcal{A} \models_{\pi} \psi \leftrightarrow \mathcal{M} \models_{\pi} \psi$. The fact that $\mathcal{M} \models_{\pi} \dot{\forall}\psi \rightarrow \mathcal{A} \models_{\rho} \dot{\forall}\psi$ is trivial, by unfolding the definition of satisfaction. Conversely, assuming $\mathcal{A} \models_{\rho} \dot{\forall}\psi$, put $m := F^{\forall}(\rho)(\psi)$ so that $m \in A$ by Tarski–Vaught-closedness. Because $\mathcal{A} \models_{\rho} \dot{\forall}\psi$, we have that $\mathcal{A} \models_{m::\rho} \psi$, hence by hypothesis $\mathcal{M} \models_{m::\rho} \psi$, hence by the definition of $m$ we have $A \models_{\rho} \dot{\forall}\psi$;

* Consider an existentially quantified formula $\varphi = \exists\psi$ such that for all environment $\pi$ over $A$ we have $\mathcal{A} \models_{\pi} \psi \leftrightarrow \mathcal{M} \models_{\pi} \psi$. The fact that $A \models_{\rho} \exists\psi \rightarrow \mathcal{M} \models_{\pi} \exists\psi$ is trivial, by unfolding the definition of satisfaction. Conversely, assuming $\mathcal{M} \models_{\rho} \exists\psi$, put $m := F^{\exists}(\rho)(\psi)$ so that $m \in A$ by Tarski–Vaught-closedness. Because $\mathcal{M} \models_{\rho} \exists\psi$, we have that $\mathcal{M} \models_{m::\rho} \psi$ by definition of $m$, hence $\mathcal{M} \models_{m::\rho} \psi$ by hypothesis, hence $\mathcal{A} \models_{\rho} \dot{\forall}\psi$.

* Finally, $\mathcal{A} \models_{\rho} \bot \leftrightarrow \mathcal{M} \models_{\pi} \bot$ is equivalent to $\bot \leftrightarrow \bot$, which holds. $\square$

## V.3 Step operators

Using the two Tarski–Vaught functions, we can define some operators on $\mathcal{P}(M)$. The goal is, starting from any set $A : \mathcal{P}(M)$, to build the smallest set that is function-closed and then to add it enough elements so that it is Tarski–Vaught-closed. We do so by steps.
**Definition 19.** We define $s_T : \mathcal{P}(M) \to \mathcal{P}(M)$ as follows:

$$s_T(A) := \{m : M \mid \exists t : T. \exists \rho : \mathrm{env}(A). m = \hat{\rho}(t)\}$$

We define $s_F : \mathcal{P}(M) \to \mathcal{P}(M)$ as follows:

$$s_F(A) := \{m : M \mid \exists \varphi : \mathbb{F}. \exists \rho : \mathrm{env}(A). m = F^{\forall}(\varphi)(\rho) \lor m = F^{\exists}(\varphi)(\rho)\}$$

We define the step operator $s : \mathcal{P}(M) \to \mathcal{P}(M)$ by:

$$s(A) := s_T(A) \cup s_F(A)$$

and its closure by:

$$S(A) := \bigcup_{n:\mathbb{N}} s^n(A)$$

where $s^n$ denotes the n-th iteration of $s$ ($s^0$ being the identity).

The function $s_T$ closes its input set under the interpretation of any function symbol. The function $s_F$ yields a set of elements so that, for any $A$, if $A \cup s_F(A)$ has a $\Sigma$-structure, any formula is satisfied in it if and only if the same formula is satisfied in $M$. This means that if a set $A$ is stable under both operators, it is an elementary submodel of $M$. To show that such a set exists, we will use the following:

**Lemma 8.** The following hold for any sets $A$ and $B$ of $M$:

1. $A \subseteq s_T(A)$;

2. $A \subseteq s(A)$;

3. $A \subseteq S(A)$;

4. $A \subseteq B \to s_F(A) \subseteq s_F(B)$;

5. $A \subseteq B \to s_T(A) \subseteq s_T(B)$;

6. $A \subseteq B \to s(A) \subseteq s(B)$;

7. $A \subseteq B \to S(A) \subseteq S(B)$;

8. $s_T(\emptyset) = s_F(\emptyset) = s(\emptyset) = S(\emptyset) = \emptyset$.

Also, $A$ is not necessarily a subset of $s_F(A)$;

*Proof.* Fix $A$ and $B$ two sets of $M$ so that $A \subseteq B$.

1. Take $a \in A$. Then, $x_0$ is a term and $\rho := n \mapsto a$ is an environment of $A$, then $\hat{\rho}(x_0) = a$, so $a \in s_T(A)$.

2. By definition, one has $s_T(A) \subseteq s(A)$ and then uses the transitivity of $\subseteq$ on the previous item.
3. By definition, one has $s(A) \subseteq S(A)$ and then uses the transitivity of $\subseteq$ on the previous item.

4. For any $x \in s_{\mathbb{T}}(A)$, there exists $t : \mathbb{T}$ and $\rho : \mathrm{env}(A)$ so that $x = \hat{\rho}(t)$. With $\iota : A \to B$ the inclusion map, $\pi := \iota \circ \rho$ is an environment over $B$ and then, $t$ and $\pi$ are such that $\hat{\pi}(t) = x$, hence $x \in s_{\mathbb{T}}(B)$.

5. For any $x \in s_{\mathbb{F}}(A)$, there exists $\varphi : \mathbb{F}$ and $\rho : \mathrm{env}(A)$ so that $x = F^{\varphi}(\varphi)(\rho)$ or $x = F^{\exists}(\varphi)(\rho)$. With $\iota : A \to B$ the inclusion map, $\pi := \iota \circ \rho$ is an environment over $B$ and then, $\varphi$ and $\pi$ are such that $x = F^{\varphi}(\varphi)(\pi)$ or $x = F^{\exists}(\varphi)(\pi)$, hence $x \in s_{\mathbb{F}}(B)$.

6. We have $s_{\mathbb{F}}(A) \subseteq s_{\mathbb{F}}(B)$ and $s_{\mathbb{T}}(A) \subseteq s_{\mathbb{T}}(B)$ by the previous items. $\cup$ is increasing with respect to $\subseteq$, so $s_{\mathbb{T}}(A) \cup s_{\mathbb{F}}(A) \subseteq s_{\mathbb{T}}(B) \cup s_{\mathbb{F}}(B)$.

7. We have $s^n(A) \subseteq s^n(B)$ for any $n$, by induction on $n$ and the previous item. $\cup$ is increasing with respect to $\subseteq$, so $\cup_{n:\mathbb{N}} s^n(A) \subseteq \cup_{n:\mathbb{N}} s^n(B)$.

8. There is no environment over $\emptyset$, so the existential statements in the definitions of $s_{\mathbb{T}}$ and $s_{\mathbb{F}}$ are never fulfilled and are hence equivalent to $\perp$.

Also, in a language with no predicate symbol and in a model of that signature with at least two elements $m$ and $n$, the functions $F^{\exists} = F^{\varphi} := \varphi \mapsto \rho \mapsto m$ are Tarski-Vaught and $s_{\mathbb{F}}(\{n\}) = \{m\}$. $\square$

## V.4 Elementary submodel

We now try to find an elementary submodel starting with any set, using these step operations.

**Lemma 9.** For any non-empty $A : \mathcal{P}(M)$, $A$ is function- and Tarski-Vaught-closed if and only if $s(A) = A$.

*Proof.* Assume $A$ is function- and Tarski-Vaught-closed. We already know that $A \subseteq s(A)$, by Lemma 8. It hence suffices to prove $s_{\mathbb{T}}(A) \subseteq A$ and $s_{\mathbb{F}}(A) \subseteq A$.

To prove $s_{\mathbb{T}}(A) \subseteq A$, take $x \in s_{\mathbb{T}}(A)$ There exists $t : \mathbb{T}$ and $\rho : \mathrm{env}(A)$ so that $x = \hat{\rho}(t)$. By function-closedness of $A$, we deduce that $x \in A$.

To prove $s_{\mathbb{F}}(A) \subseteq A$, take $x \in s_{\mathbb{F}}(A)$. There exists $\varphi : \mathbb{F}$ and $\rho : \mathrm{env}(A)$ so that either $F^{\exists}(\varphi)(\rho) = x$ or $F^{\varphi}(\varphi)(\rho) = x$. By Tarski-Vaught-closedness of $A$, we deduce that $x \in A$ in either case.

For the converse, consider a non-empty set $A$ of $M$ such that $s(A) = A$ and take $a_0 : A$. We show that it is function closed and Tarski-Vaught-closed.

Take $f$ a function symbol and elements $a_1, \dots, a_{\mathrm{ar}(f)} : A$. We consider $\alpha := n \mapsto a_0$ and $\rho := a_1 :: \dots :: a_{\mathrm{ar}(f)} :: \alpha$, they are environments over $A$. Then, $f^{\mathcal{M}}(a_1; \dots; a_{\mathrm{ar}(f)}) = \hat{\rho}(f[x_0; \dots; x_{\mathrm{ar}(f)-1}])$ is in $A$, since $s_{\mathbb{T}}(A) \subseteq A$, so $A$ is function closed.<fnref n="11" />

<footnote n="11">¹¹Note that if $A$ was empty and $f$ of arity 0, $A$, $A$ would not be function closed, but, as there are no environment over $A$, we would have $s_{\mathbb{T}}(A) = A$.</footnote>
Take $\varphi$ a formula and $\rho$ an environment over $A$. We have, by definition of $s_F$, $F^\forall(\varphi)(\rho)$, $F^\exists(\varphi)(\rho) \in s_F(A)$, which is, by hypothesis, included in $A$. So $A$ is Tarski-Vaught-closed. $\square$

**Lemma 10.** For any $A : \mathcal{P}(M)$, $s(A) = A$ and $S(A) = A$ are equivalent.

*Proof.* Assume $s(A) = A$. Then, for any $n$, we have $s^{n+1}(A) = s^n(A)$, hence for all $n$, $s^n(A) = A$. The union $\bigcup_{n:\mathbb{N}} s^n(A)$ is then equal (as a set) to $\bigcup_{n:\mathbb{N}} A$, in turn equal to $A$.

Conversely, we have $s(A) \subseteq S(A) \subseteq A \subseteq s(A)$, so $s(A) = A$. $\square$

**Lemma 11.** The operator $S$ is idempotent, meaning that for any $A : \mathcal{P}(M)$, we have $S(S(A)) = S(A)$.

*Proof.* Take $A$ a set of $M$. We have $S(A) \subseteq S(S(A))$, by Lemma 8. It then suffices to show $(s \circ S)(A) \subseteq S(A)$. If $A$ is empty, that is trivial, since $s(\emptyset) = \emptyset$. If not, take $z \in A$. Take $a_0 \in (s \circ S)(A)$. Then, either:

* $a_0 \in s_{\mathbb{T}}(S(A))$, so $a_0 = \hat{\rho}(t)$ for some $\rho : \text{env}(S(A))$ and $t : \mathbb{T}$. For each $j < \nu(t)$, there exists $n_j$ a natural number so that $\rho(j) \in s^{n_j}(A)$. Take $n$ the max of the $n_j$ for $j < \nu(t)$: we have that $\hat{\rho}(t) \in s^{n+1}(A) \subseteq S(A)$, because the environment $\pi := \rho(0) :: \rho(1) :: \dots :: \rho(\nu(t)) :: (n \mapsto z)$ is over $S(A)$ and is up-to-$\nu(t)$-equivalent to $\rho$.

* or $a_0 \in s_F(S(A))$, so $a_0 = F^\forall(\varphi)(\rho)$ or $a_0 = F^\exists(\varphi)(\rho)$, with $\rho : \text{env}(S(A))$ and $\varphi : \mathbb{F}$. Assume we are in the first case. For each $j < \nu(\varphi)$, there exists $n_j$ a natural number so that $\rho(j) \in s^{n_j}(A)$. Take $n$ the max of the $n_j$ for $j < \nu(\varphi)$: we have $F^\forall(\varphi)(\rho) \in s^{n+1}(A)$, because the environment $\pi := \rho(0) :: \rho(1) :: \dots :: \rho(\nu(\varphi)) :: (n \mapsto z)$ is over $S(A)$, $\pi$ is up-to-$\nu(\varphi)$-equivalent to $\rho$ and by formulas-environment invariance. The case for $F^\exists$ is similar. $\square$

As an immediate corollary to these three lemmas, we have the following key lemma.

**Lemma 12.** For any non-empty $A : \mathcal{P}(M)$, the set $S(A)$ is an elementary submodel of $M$.

Since we assumed $M$ is inhabited by at least an element $m_0$, we can consider the singleton set $A_0 := \{m_0\}$ associated to the predicate $m \mapsto m = m_0$; $S(A_0)$ is an elementary submodel $\mathcal{A}$ of $M$.

## V.5 Size boundedness

Now that we have a candidate elementary submodel $\mathcal{A}$, we can check that it fulfills the size condition of the DLS theorem. We prove a slightly more general lemma.
**Lemma 13.** For any non-empty $A: \mathcal{P}(M)$, if $A \leq T + F$, then we have:

1. $s_T(A) \leq T + F$;

2. $s_F(A) \leq T + F$;

3. $s(A) \leq T + F$;

4. $S(A) \leq T + F$.

It remains to show that $A_0 \leq T + F$. We give a slightly stronger result.

**Lemma 14.** For any type $X$ and any $x_0: X$, the singleton set of $X$ containing $x_0$ is smaller than $N$.

*Proof.* Using PI, one shows that any singleton set $X_0$ is inhabited by a single element, the function $x_* \mapsto 0: X_0 \to N$ is thus injective, proving $X_0 \leq N$. $\square$

We can finally prove the DLS via Tarski-Vaught functions theorem. Recall that it states that, for any model $\mathcal{M}$, if $\mathcal{M}$ is inhabited and if there exists a pair of Tarski-Vaught functions, then the DLS principle holds for $\mathcal{M}$.

*Proof (Theorem 1).* We combine previously proved lemmas: the set $S(A_0)$ is an elementary submodel of $\mathcal{M}$, by Lemma 12, and satisfies $S(A_0) \leq T + F$, by Lemma 14, Lemma 13 and transitivity. $\square$

# VI Related work

## VI.1 The classical DLS theorem in ZF

In 1915, Löwenheim stated the following statement: for any countable signature $\Sigma$ and infinite model $\mathcal{M}$ of $\Sigma$, there exists a model $\mathcal{N}$ the $\Sigma$ and of domain $N$ that is elementarily equivalent to $\mathcal{M}$ [17]. Even though his proof was later deemed incomplete, his paper led to new questions and new discoveries.

Five years later, in 1920, Skolem both strengthened the statement and simplified the proof, by introducing Skolem functions and Skolem normal form [19]. Namely, he proved that, with a countable signature $\Sigma$ and an infinite model $\mathcal{M}$ of $\Sigma$, there exists a countable subset $A \subseteq \mathcal{M}$ that is an elementary submodel of $\mathcal{M}$.

In his proof, Skolem first extends the given signature $\Sigma_0$ with a function symbol for each formula, thus creating a signature $\Sigma_1$ of the same cardinality. Then, he shows that a model $\mathcal{M}$ of $\Sigma_0$ is essentially the same as a model of $\Sigma_1$ when each newly added symbols is interpreted as a Skolem function. He continues by showing that any $\Sigma_0$-formula is equivalent to a $\Sigma_1$ formula in what is now called Skolem normal form and concludes by proving the DLS principle for any model of a countable conjunction of formulas in Skolem normal form. As he does not use nowadays' formalism, it is hard to translate his proof in it.

In the century between Skolem's proof and now, different authors gave different proofs of that statement. For formalization purpose, we picked the one
by Button and Walsh [4]. They prove the following theorem in ZFC: for any signature $\Sigma$ and any model $\mathcal{M}$ of that signature, for any set $A_0 \subseteq \mathcal{M}$, there exists an elementary submodel $\mathcal{A}$ of $\mathcal{M}$ with domain $A$ such that $A_0 \subseteq A \subseteq \mathcal{M}$ and $|A| = |A_0| + |\Sigma| + \aleph_0$. They do so by applying a function from $\mathcal{P}(\mathcal{M})$ to $\mathcal{P}(\mathcal{M})$ countably many times, starting with a given set $A_0$. Their method uses Skolem functions implicitly: they do not use that word, but the construction they use is essentially equivalent.

Note that, in order to have cardinals well-defined, one has to use AC. The use of LEM is also necessary in the proof, but it is an inherent feature of ZF, hence of ZFC. In other words, the classical DLS theorem is a theorem of ZFC but not of ZF.

From a reverse mathematics point of view, within ZF, the DLS principle for all models of countable signature $(\aleph_0$-DLS) is equivalent to DC, the principle of dependent choices. A proof of that equivalence can be found in Espíndola's note on the matter [9].<fnref n="12" /> He also gives a proof of the full DLS principle being equivalent to AC.

In a following note, Karagila proves the equivalence between the DLS principle for any model of a any signature of cardinality at most $\kappa$ ($\kappa$-DLS) and the conjunction of two principles related the axiom of choice: DC and $\kappa$-AC [14]. This is a refinement of Espíndola work, as one easily goes from Karagila's result to Espíndola's one. Remark that since $\aleph_0$-AC follows from DC in ZF, we find again that the $\aleph_0$-DLS principle is equivalent to DC alone.

In both these two last works, because the authors are working in ZF and don't assume AC, cardinals are a slightly difficult to define and all cardinals are not aleph numbers. Additionally, none of them prove their that the relevant variant of AC implies the relevant variant of the DLS principle, they rely on external references for that [13, 12].

## VI.2 In Rocq

Kirst and Zeng carried out a thorough work of constructive reverse mathematics regarding the $\aleph_0$-DLS principle, uncovering its equivalence with four logical principles, two weaker than LEM and two weaker than AC [15]. They focused on the $\aleph_0$-DLS. With a countable signature, both $\mathcal{T}$ and $\mathcal{F}$ are countable too. While it is, in general, always possible to endow $\mathcal{T}$ with a structure of model $\mathcal{T}$, it is the countability of $\mathcal{F}$ that allows to prove that there is an elementary embedding from $\mathcal{T}$ to $\mathcal{M}$.

Since with an arbitrary signature $\Sigma$, there can be only countably many terms but an uncountable amount of predicate symbols (hence of formulas), the terms model $\mathcal{T}$ can be too small for being a candidate elementary submodel of a model of $\Sigma$, showing that their strategy cannot be extended to the general case.

**Example 8.** Consider the signature with no function symbol and a unary predicate symbol $P_r$ for any $r: \mathbb{R}$. A model $\mathcal{R}$ of this signature is the following:

<footnote n="12">¹²The equivalence was known since at least 1989, as it was published as an exercise in Boolos and Jeffrey's book [3], nonetheless, this book does not give any proof.</footnote>
domain is $\mathbb{R}$ and for $r, s : \mathbb{R}$, we interpret $P_r^{\mathbb{R}}(s)$ as $r = s$. No model whose domain is $\mathbb{T}$ is elementarily embeddable into $\mathbb{R}$.

*Proof.* First remark that for any $r : \mathbb{R}$, $\mathcal{R} \models \exists P_r(x_0)$. Assuming $\mathcal{N}$ is a model of $\Sigma$ of domain $\mathbb{N}$ and taking $h : \mathbb{N} \to \mathbb{R}$ an elementary embedding, we can find $\xi : \mathbb{R}$ so that it is not in the image of $h$. Since $h$ is an elementary embedding, we have that for any $\rho$,

$$ \mathcal{N} \models_{\rho} \exists P_{\xi}(x_0) \leftrightarrow \mathcal{R} \models_{\rho} \exists P_{\xi}(x_0) $$

Because the right member above holds, we deduce that for any $\rho$:

$$ \exists n : \mathbb{N}. \mathcal{N} \models_{n::\rho} P_{\xi}(x_0) $$

Take such an $n$. Now, for any $\rho$, we also have:

$$ \mathcal{N} \models_{n::\rho} P_{\xi}(x_0) \leftrightarrow \mathcal{R} \models_{h(n)::h \circ \rho} P_{\xi}(x_0) $$

by elementarity of $h$. The left member holds, so we deduce:

$$ h(n) = \xi $$

Combined with the fact that $\forall n. h(n) \neq \xi$, we have just proved $\perp$. Hence, we proved that $\mathcal{N} \not\subseteq \mathcal{R}$. Hence, since $\mathbb{N}$ and $\mathbb{T}$ are in bijection, a term model cannot be elementarily embeddable into $\mathcal{R}$. $\square$

## VI.3 In other proof assistants

The classical DLS theorem is already part of Lean's MathLib library [1]. As expected, it heavily uses AC. The Lean proof also uses Skolem functions, but makes them internal to an extended signature. This means that, for any model $\mathcal{M}$ of a signature $\Sigma_0$, the initial signature $\Sigma_1$ is expanded into a new signature $\Sigma_1$ by adding a function symbol $f_\varphi$ for each formula $\varphi$. In a subset of $\mathcal{M}$, each new function symbol of $\Sigma_1$ is then interpreted as the Skolem function for the associated formula. The original symbols from $\Sigma_0$ are interpreted as they are in $\mathcal{M}$. Then, being closed under functions of the new signature means being an elementary submodel of $\mathcal{M}$.

Nonetheless, as this proof involves expanding the signature using AC, it was not deemed easily formalizable in Rocq for our purpose. Additionally, there are other arguments involving AC throughout the whole proof: for the existence of cardinals, ...

Berghofer has also implemented the Löwenheim theorem for any signatures in Isabelle/HOL [2]. Caminati gave a Mizar proof of the classical $\aleph_0$-DLS theorem [5].

## References

[1] Aaron Anderson. Skolem Functions and Downward Löwenheim-Skolem. The Mathlib4 Community, 2022.
[2] Stefan Berghofer. First-Order Logic according to Fitting. *Archive of Formal Proof*, August 2007.

[3] George S. Boolos and Richard C. Jeffrey. *Computability and logic*. Cambridge University Press, Cambridge, 3 edition, September 1989.

[4] Tim Button and Sean Walsh. *Philosophy and model theory*. Oxford University Press, 2018.

[5] Marco Bright Caminati. Basic first-order model theory in Mizar. *Journal of Formalized Reasoning*, 3(1):49–77, December 2010.

[6] Chen Chung Chang and Howard Jerome Keisler. *Model Theory*. Studies in Logic and the Foundations of Mathematics. Elsevier, 3e edition, 1990.

[7] Thierry Coquand and Christine Paulin-Mohring. Inductively defined types. In Per Martin-Löf and Grigori Mints, editors, *COLOG-88*, pages 50–66, Berlin, Heidelberg, 1990. Springer Berlin Heidelberg.

[8] Nicolaas Govert de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. *Indagationes Mathematicae (Proceedings)*, 75(5):381–392, 1972.

[9] Christian Espíndola. Löwenheim-Skolem theorems and Choice principles, 2012.

[10] J. Hadamard. Cinq lettres sur la théorie des ensembles. *Bulletin de la Société mathématique de France*, 2:261–273, 1905.

[11] Horst Herrlich. *Axiom of choice*. Springer-Verlag, 2006.

[12] Paul Howard and Jean Rubin. *Consequences of the Axiom of Choice*, volume 59 of *Mathematical Surveys and Monographs*. American Mathematical Society, Providence, Rhode Island, June 1998.

[13] Thomas J. Jech. *The axiom of choice*. Studies in logic and the foundations of mathematics. North-Holland Pub. Co.; American Elsevier Pub. Co, 1973.

[14] Asaf Karagila. Downward Löwenheim-Skolem Theorems and Choice Principles, March 2014.

[15] Dominik Kirst and Haoyi Zeng. The Blurred Drinker Paradox and Blurred Choice Axioms for the Downward Löwenheim-Skolem Theorem. In *Logic in Computer Science*, 2025.

[16] Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Type-theoretic approaches to ordinals. *Theoretical Computer Science*, 957, May 2023.
[17] Leopold Löwenheim. Über Möglichkeiten im Relativkakül. *Mathematische Annalen*, 76:447–470, 1915.

[18] Cécilia Pradic and Chad E. Brown. Cantor-Bernstein implies excluded middle, 2022.

[19] Thoralf Skolem. Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen. *Videnskapsselskapet Skrifter, I. Matematisk-naturvidenskabelig Klasse*, 4:1–36, 1920.

[20] Arnaud Spiwack and Thierry Coquand. Constructively Finite? In *Contribuciones científicas en honor de Mirian Andrés Gómez*. Universidad de La Rioja, 2010.

[21] Juris Steprans. Answer to "Example of two structures". MathOverflow, November 2011.

[22] Alfred Tarski. Contributions to the theory of models I. *Indagationes Mathematicae*, 57:572–581, 1954.

[23] Alfred Tarski and R. L. Vaught. Arithmetical extensions of relational systems. *Compositio Mathematica*, 13:81–102, 1958.

[24] The Rocq Development Team. The Rocq Prover, January 2022.

[25] Jean van Heijenoort. *From Frege to Gödel*. Source books in the history of sciences. Harvard University Press, 1967.

[26] R. L. Vaught. On the axiom of choice and some metamathematical theorems. In *Bulletin of the American Mathematical Society*, volume 62, pages 262–263, New York, NY, February 1956. American Mathematical Society.

[27] E. Zermelo. Neuer Beweis für die Möglichkeit einer Wohlordnung. *Mathematische Annalen*, 65(1):107–128, March 1907.

[28] Ernst Zermelo. Beweis, daß jede Menge wohlgeordnet werden kann (Aus einem an Herrn Hilbert gerichteten Briefe). *Mathematische Annalen*, 59:514–516, 1904.

# A Variants of the DLS theorem

Many different statements bear, throughout the literature, the same name Löwenheim–Skolem theorem or downward Löwenheim–Skolem theorem, even though they are not necessarily equivalent. We give an overview of different variants of set theoretic principles.

The general skeleton is: for any signature $\Sigma$ respecting a property $A$, for any model $\mathcal{M}$ of that signature that is bigger than, there exists a model $\mathcal{N}$ having a model theoretic property $B$ whose domain $\mathcal{N}$ respects a size property $C$.
We list the possible definition of A, B and C, each list is given increasing order of strength. By that, we mean that if one fixes two properties, the three theorems obtained by changing the third property are in increasing order for strength.

The property A of Σ is either:

1. Σ is countable;

2. no condition on Σ;

3. for any given cardinal κ, Σ is less than κ.

The model theoretic property B of N is either:

1. N is elementarily equivalent to M;

2. N is elementarily embeddable into M;

3. N is an elementary submodel of M.

The size property C of N is either:

1. N has cardinality ℵ₀ + |Σ|;

2. N has cardinality κ, for κ a cardinal between ℵ₀ + |Σ| ≤ κ ≤ |M|;

3. N has cardinality ℵ₀ + |Σ| + |N₀|, for some subset N₀ of M and N₀ ⊆ N.

<table><caption>Table 1: Different statement for the same name</caption><thead><tr><th></th><th>A</th><th>B</th><th>C</th></tr></thead><tbody><tr><td>Button and Walsh [4]</td><td>2</td><td>3</td><td>3</td></tr><tr><td>Espíndola [9]</td><td>3</td><td>3</td><td>2</td></tr><tr><td>Karagila [14]</td><td>3</td><td>3</td><td>1</td></tr><tr><td>Kirst and Zeng [15]</td><td>1</td><td>2</td><td>1</td></tr><tr><td>Skolem [19]</td><td>1</td><td>3</td><td>1</td></tr><tr><td>Lean [1]</td><td>2</td><td>3</td><td>3</td></tr><tr><td>Isabelle/HOL [2]</td><td>2</td><td>1</td><td>1</td></tr><tr><td>Mizar [5]</td><td>1</td><td>3</td><td>1</td></tr><tr><td>Chang and Keisler [6]</td><td>3</td><td>1</td><td>1</td></tr><tr><td>Löwenheim [17]</td><td>1</td><td>1</td><td>1</td></tr><tr><td>Vaught [26]</td><td>2</td><td>1</td><td>1</td></tr></tbody></table>

The Table 1 presents what different authors present and study as the DLS theorem, or even simply as the LS theorem. The first lines are the main references of this work, then other implementations in other proof assistants and finally, other authors.