IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCModelTheoryNonForcing

   1/-
   2  PrimitiveRecognitionCalculus/PRCModelTheoryNonForcing.lean
   3
   4  Round-trip source:
   5    δ/Delta_Continuum_Is_Not_Forced.tex  (the model-theory / definability
   6    non-forcing argument, the fourth of the paper's four independent
   7    arguments that the continuum is not forced).
   8
   9  This module formalizes that fourth argument. The paper gives four
  10  independent routes to "distinction does not force the continuum":
  11
  12    1. cardinality              (real_not_countable, etc.)
  13    2. generative countability  (generated_countable, in PRCNativeCostUniqueness)
  14    3. measure zero             (generated_volume_zero, in PRCNativeCostUniqueness)
  15    4. model theory             (this file)
  16
  17  The model-theory route is the sharpest: it says no *first-order* description
  18  in a countable language can pin ℝ down to isomorphism, because downward
  19  Löwenheim–Skolem produces a countable structure that satisfies exactly the
  20  same first-order sentences as ℝ yet cannot be isomorphic to it (it has the
  21  wrong cardinality). Whatever first-order theory distinction writes about its
  22  number line, a countable companion validates every sentence of it.
  23
  24  We isolate the heavy `Mathlib.ModelTheory` import in this sibling module so
  25  the rest of the PRC cost-uniqueness development does not pay the build cost.
  26-/
  27
  28import Mathlib.ModelTheory.Satisfiability
  29import Mathlib.Analysis.Real.Cardinality
  30import Mathlib.SetTheory.Cardinal.Continuum
  31
  32namespace IndisputableMonolith
  33namespace Foundation
  34namespace PrimitiveRecognitionCalculus
  35namespace ModelTheoryNonForcing
  36
  37open Cardinal FirstOrder
  38
  39/-- **Downward Löwenheim–Skolem for the reals.**
  40For any countable first-order language `L` in which `ℝ` carries a structure,
  41there is a *countable* `L`-structure `N` that is elementarily equivalent to
  42`ℝ` (i.e. `ℝ ≅[L] N`): `N` satisfies exactly the same `L`-sentences as `ℝ`.
  43
  44This is the engine of the model-theory non-forcing argument. The hypothesis
  45`hL : L.card ≤ ℵ₀` is the "countable language" assumption: distinction can
  46only write down countably many primitive relations, functions, and constants. -/
  47theorem real_has_countable_ee_model
  48    {L : FirstOrder.Language.{0, 0}} [L.Structure ℝ] (hL : L.card ≤ Cardinal.aleph0) :
  49    ∃ N : CategoryTheory.Bundled L.Structure, (ℝ ≅[L] N) ∧ Cardinal.mk N = Cardinal.aleph0 :=
  50  FirstOrder.Language.exists_elementarilyEquivalent_card_eq L ℝ Cardinal.aleph0
  51    le_rfl (by simpa using hL)
  52
  53/-- **The reals are not first-order categorical (in any countable language).**
  54For any countable language structure on `ℝ`, there is a structure `N`
  55elementarily equivalent to `ℝ` that is *not* isomorphic to `ℝ` even as a bare
  56type: it is countable while `ℝ` has cardinality continuum.
  57
  58Consequence for the δ program: no first-order description in a countable
  59language fixes `ℝ` up to isomorphism. Distinction may force a complete
  60first-order theory of its number line, and `ℝ` may be one model of it, but a
  61countable model of the very same theory always exists. The continuum is not
  62forced by any amount of first-order distinction. -/
  63theorem real_not_first_order_categorical
  64    {L : FirstOrder.Language.{0, 0}} [L.Structure ℝ] (hL : L.card ≤ Cardinal.aleph0) :
  65    ∃ N : CategoryTheory.Bundled L.Structure,
  66      (ℝ ≅[L] N) ∧ Cardinal.mk ℝ ≠ Cardinal.mk N := by
  67  obtain ⟨N, hee, hcard⟩ := real_has_countable_ee_model hL
  68  refine ⟨N, hee, ?_⟩
  69  rw [hcard, Cardinal.mk_real]
  70  exact Cardinal.aleph0_lt_continuum.ne'
  71
  72/-- The countable elementarily-equivalent companion exists and is a genuine
  73witness of non-forcing: it agrees with `ℝ` on every first-order sentence yet
  74is countable, hence not equinumerous with `ℝ`. Packaged form combining all
  75three facts for downstream citation. (Equinumerosity is necessary for any
  76structure isomorphism, so distinct cardinals rule out `ℝ ≃ N` of any kind.) -/
  77theorem real_first_order_underdetermined
  78    {L : FirstOrder.Language.{0, 0}} [L.Structure ℝ] (hL : L.card ≤ Cardinal.aleph0) :
  79    ∃ N : CategoryTheory.Bundled L.Structure,
  80      (ℝ ≅[L] N) ∧ Cardinal.mk N = Cardinal.aleph0 ∧ Cardinal.mk ℝ ≠ Cardinal.mk N := by
  81  obtain ⟨N, hee, hcard⟩ := real_has_countable_ee_model hL
  82  refine ⟨N, hee, hcard, ?_⟩
  83  rw [hcard, Cardinal.mk_real]
  84  exact Cardinal.aleph0_lt_continuum.ne'
  85
  86end ModelTheoryNonForcing
  87end PrimitiveRecognitionCalculus
  88end Foundation
  89end IndisputableMonolith
  90