real_has_countable_ee_model
plain-language theorem explainer
Downward Löwenheim–Skolem for the reals: every countable first-order language structure on ℝ admits a countable elementarily equivalent companion. Anyone arguing that first-order distinction cannot force the continuum cites this. The proof is a one-line call to Mathlib's general existence theorem for elementarily equivalent models of a prescribed infinite cardinality.
Claim. Let $L$ be a first-order language of cardinality at most $\aleph_0$ carrying an $L$-structure on $\mathbb{R}$. Then there exists an $L$-structure $N$ such that $\mathbb{R}$ and $N$ are elementarily equivalent and $|N|=\aleph_0$.
background
The module builds the model-theory half of the Primitive Recognition Calculus non-forcing argument: first-order distinction written in a countable language cannot pin the continuum down to a unique model up to isomorphism.
Elementary equivalence means the two structures satisfy exactly the same $L$-sentences. Classical downward Löwenheim–Skolem supplies, for any infinite model of a countable language, a model of every infinite cardinality at most that of the original. Here the target cardinality is $\aleph_0$ and the original model is $\mathbb{R}$.
The hypothesis that the language has cardinality at most $\aleph_0$ is the Recognition Science premise that distinction can name only countably many primitive symbols (relations, functions, constants).
proof idea
One-line term wrapper. It applies Mathlib's FirstOrder.Language.exists_elementarilyEquivalent_card_eq at language $L$, structure $\mathbb{R}$, and target cardinality $\aleph_0$. The two side conditions are discharged by reflexivity of $\le$ on cardinals and by the countable-language hypothesis (after a simpa).
why it matters
This is the engine of the model-theory non-forcing argument in the module. Downstream it feeds real_not_first_order_categorical (a countable elementary companion of different cardinality, so not isomorphic even as bare types) and real_first_order_underdetermined (the packaged triple: elementary equivalence, countability of the companion, and continuum $\ne \aleph_0$).
For the $\delta$ program the moral is sharp: no first-order description in a countable language fixes $\mathbb{R}$ up to isomorphism. Distinction may force a complete first-order theory of its number line, and $\mathbb{R}$ may be one model of that theory, but a countable model of the same theory always exists. The continuum is not forced by any amount of first-order distinction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.