real_first_order_underdetermined
plain-language theorem explainer
For any countable first-order language carrying a structure on the reals, a countable elementary equivalent companion exists and is not equinumerous with ℝ. Foundation workers cite this packaged non-forcing witness to show first-order sentences cannot pin down the continuum. The proof is a short packaging of the downward Löwenheim–Skolem companion plus the continuum cardinality gap.
Claim. Let $L$ be a first-order language of cardinality at most $\aleph_0$ with an $L$-structure on $\mathbb{R}$. Then there exists an $L$-structure $N$ such that $\mathbb{R}$ and $N$ are elementarily equivalent, $|N|=\aleph_0$, and $|\mathbb{R}|\neq|N|$.
background
This sits in the Primitive Recognition Calculus model-theory non-forcing layer. The goal is to show that first-order sentences in a countable language cannot force the continuum structure of $\mathbb{R}$: any such theory admits a countable model agreeing on every sentence.
Elementary equivalence $\mathbb{R} \cong[L] N$ means $N$ satisfies exactly the same $L$-sentences as $\mathbb{R}$. Equinumerosity is necessary for any structure isomorphism, so distinct cardinals immediately rule out $\mathbb{R} \simeq N$ of any kind.
The engine is the upstream downward Löwenheim–Skolem fact: for countable $L$ with an $L$-structure on $\mathbb{R}$, there is a countable $N$ with $\mathbb{R} \cong[L] N$. The hypothesis $L.\mathrm{card} \le \aleph_0$ encodes that distinction can write down only countably many primitive symbols.
proof idea
One-line packaging of the upstream companion. Invoke the downward Löwenheim–Skolem theorem for the reals to obtain a bundled $L$-structure $N$ that is elementarily equivalent to $\mathbb{R}$ and has cardinality $\aleph_0$. Return that triple, discharging the remaining inequality by rewriting the cardinality of $N$ and applying the standard fact that $\aleph_0$ is strictly below the continuum (so $\mathrm{mk},\mathbb{R} \neq \aleph_0$).
why it matters
Packages the three non-forcing facts (elementary equivalence, countability, non-equinumerosity) into a single citation target for the PRC foundation. Downstream it is used in the native-cost uniqueness development, where the $\delta$-act ladder is shown to determine the calibration invariant $c^2$ and nothing more: first-order underdetermination of $\mathbb{R}$ blocks any claim that a countable first-order theory alone forces the continuum-scale cost structure.
In the broader Recognition chain this supports the stance that continuum geometry and the forced constants (phi, eight-tick octave, $D=3$) must come from the Recognition Composition Law and the T0–T8 forcing steps, not from first-order model theory of the reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.