real_not_first_order_categorical
plain-language theorem explainer
In any countable first-order language, the reals are not categorical: there is always an elementarily equivalent structure that is countable, hence not equinumerous with ℝ. Anyone arguing that first-order distinction cannot force the continuum cites this packaging lemma. The proof is a short assembly of downward Löwenheim–Skolem plus the aleph-zero/continuum gap.
Claim. Let $L$ be a first-order language of cardinality at most $\aleph_0$, and equip $\mathbb{R}$ with an $L$-structure. Then there exists an $L$-structure $N$ such that $\mathbb{R}$ and $N$ are elementarily equivalent ($\mathbb{R} \equiv_L N$) and $|\mathbb{R}| \neq |N|$.
background
Elementary equivalence $\mathbb{R} \equiv_L N$ means $N$ satisfies exactly the same $L$-sentences as $\mathbb{R}$. First-order categoricity would require every model of $\mathrm{Th}_L(\mathbb{R})$ to be isomorphic to $\mathbb{R}$ as an $L$-structure; the theorem shows this fails already at the level of bare cardinality.
The engine is downward Löwenheim–Skolem for the reals: for any countable language $L$ with an $L$-structure on $\mathbb{R}$, there is a countable $N$ with $\mathbb{R} \equiv_L N$ and $|N|=\aleph_0$. The hypothesis $L.\mathrm{card}\le\aleph_0$ encodes that distinction can name only countably many primitives.
The local module packages model-theoretic non-forcing for the Primitive Recognition Calculus: first-order theories of the number line never pin down the continuum.
proof idea
Invoke the sibling theorem that supplies a countable elementarily equivalent companion $N$ (downward Löwenheim–Skolem specialized to $\mathbb{R}$). Return that same $N$ as the witness. The elementary-equivalence half is immediate. For the cardinality half, rewrite $|N|=\aleph_0$ and $|\mathbb{R}|=2^{\aleph_0}$, then apply the standard inequality $\aleph_0 < 2^{\aleph_0}$ to obtain $|\mathbb{R}|\neq|N|$. No further model theory is needed.
why it matters
This is the packaged non-forcing witness for the $\delta$ program: 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 model it, but a countable model of the same theory always exists. The continuum is not forced by any amount of first-order distinction.
Downstream, the native-cost uniqueness development (including the $\delta$-act ladder limit that recovers the calibration invariant $c^2$) sits in the same Primitive Recognition Calculus stack; the non-forcing fact keeps first-order model theory from short-circuiting the continuum-scale content that the cost ladder must supply by other means. It is a foundation lemma, not a physics derivation step (T0–T8), but it delimits what first-order forcing can and cannot do before the recognition calculus begins.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.