Foundation Primitive Recognition Calculus Prcmodel Theory Non Forcing Real Has C

The countable twin

In classical model theory, a first-order language is one in which you can write down sentences using variables, quantifiers, logical connectives, and a fixed list of relation, function, and constant symbols. A countable language has at most countably many such symbols. The real numbers ℝ carry a structure in any such language, meaning the symbols are interpreted as actual operations and relations on the reals.

The theorem real_has_countable_ee_model states that for any countable first-order language in which the reals carry a structure, there exists a countable structure N that is elementarily equivalent to ℝ. Elementarily equivalent means N satisfies exactly the same first-order sentences as ℝ: every sentence true of the reals is true of N, and vice versa. The theorem is proved in the framework's machine-checked library of formal theorems.

The countable twin N is not isomorphic to ℝ, because N is countable while ℝ has cardinality continuum. This is the engine of the model-theory non-forcing argument: no first-order description in a countable language fixes ℝ up to isomorphism. Distinction may force a complete first-order theory of its number line, and ℝ may be one model of it, but a countable model of the very same theory always exists. The continuum is not forced by any amount of first-order distinction.

What the theorem does not claim: it does not say the reals are undefinable, nor that no structure can distinguish them. It says only that first-order logic in a countable language cannot pin them down uniquely. The theorem is a statement about the expressive limits of a specific formal system, not about the nature of the real numbers themselves.

/-- **Downward Löwenheim–Skolem for the reals.**
For any countable first-order language `L` in which `ℝ` carries a structure,
there is a *countable* `L`-structure `N` that is elementarily equivalent to
`ℝ` (i.e. `ℝ ≅[L] N`): `N` satisfies exactly the same `L`-sentences as `ℝ`.

This is the engine of the model-theory non-forcing argument. The hypothesis
`hL : L.card ≤ ℵ₀` is the "countable language" assumption: distinction can
only write down countably many primitive relations, functions, and constants. -/
theorem real_has_countable_ee_model
    {L : FirstOrder.Language.{0, 0}} [L.Structure ℝ] (hL : L.card ≤ Cardinal.aleph0) :
    ∃ N : CategoryTheory.Bundled L.Structure, (ℝ ≅[L] N) ∧ Cardinal.mk N = Cardinal.aleph0 :=
  FirstOrder.Language.exists_elementarilyEquivalent_card_eq L ℝ Cardinal.aleph0
    le_rfl (by simpa using hL)

/-- **The reals are not first-order categorical (in any countable language).**
For any countable language structure on `ℝ`, there is a structure `N`
elementarily equivalent to `ℝ` that is *not* isomorphic to `ℝ` even as a bare
type: it is countable while `ℝ` has cardinality continuum.

Consequence for the δ program: no first-order description in a countable
language fixes `ℝ` up to isomorphism. Distinction may force a complete
first-order theory of its number line, and `ℝ` may be one model of it, but a
countable model of the very same theory always exists. The continuum is not
forced by any amount of first-order distinction. -/
theorem real_not_first_order_categorical
    {L : FirstOrder.Language.{0, 0}} [L.Structure ℝ] (hL : L.card ≤ Cardinal.aleph0) :
    ∃ N : CategoryTheory.Bundled L.Structure,
      (ℝ ≅[L] N) ∧ Cardinal.mk ℝ ≠ Cardinal.mk N := by
  obtain ⟨N, hee, hcard⟩ := real_has_countable_ee_model hL
  refine ⟨N, hee, ?_⟩
  rw [hcard, Cardinal.mk_real]
  exact Cardinal.aleph0_lt_continuum.ne'

What this page does not claim

The theorem does not claim the reals are undefinable in any language. It does not claim that no structure can distinguish the reals from a countable model. It does not claim that the continuum is impossible to force by any means other than first-order logic.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCModelTheoryNonForcing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: