IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCFullZFCParse

   1/-
   2  PrimitiveRecognitionCalculus/PRCFullZFCParse.lean
   3
   4  Item 4 of the δ frontier: removing the honest-boundary caveat on the set-theory
   5  leg. The pass-354 parse (`PRCSetTheoryParse.lean`) handled HEREDITARILY FINITE set
   6  theory (ZFC minus the axiom of infinity) via Ackermann coding on ℕ. That left one
   7  caveat: infinity was not modelled. This module removes it by working with
   8  Mathlib's `ZFSet`, the genuine von Neumann universe of ZFC WITH the axiom of
   9  infinity.
  10
  11  We prove the substantive set-theoretic content directly about the real `ZFSet`:
  12
  13  * EXTENSIONALITY (`ZFSet.ext_iff`, restated in `full_zfc_realizes_delta`): two sets
  14    are equal iff they have the same members. This is the actual axiom of
  15    extensionality of ZFC, as Mathlib formalizes it.
  16  * The empty set ∅ has no members (`ZFSet.notMem_empty`); the singleton {∅} has ∅ as
  17    its only member (`ZFSet.mem_singleton`); hence ∅ ≠ {∅} as SETS
  18    (`empty_ne_singleton`), distinguished extensionally
  19    (`empty_distinct_singleton_extensionally`).
  20  * The AXIOM OF INFINITY holds (`infinity_modeled`): the von Neumann ω is a set
  21    containing ∅ and closed under the successor x ↦ x ∪ {x}, and it is distinct from
  22    the empty set (`omega_ne_empty`). This is exactly what HF could not provide.
  23
  24  PARSE INTO THE INTERFACE, AND ITS HONEST BOUNDARY. The `FormalSystem` interface
  25  fixes `Token : Type` (universe 0), whereas `ZFSet : Type 1`. So `ZFSet` itself
  26  cannot be the token type; this is a universe wall, not a defect of the parse. We
  27  therefore parse via a Type-0 token set `Bool` injected faithfully into the ZF
  28  universe (`zfWitness`, `zfWitness_injective`), with the discrimination relation
  29  defined as GENUINE ZF EXTENSIONAL DIFFERENCE of the represented sets:
  30
  31      distinguishes a b  :=  ∃ z : ZFSet, ¬ (z ∈ zfWitness a ↔ z ∈ zfWitness b).
  32
  33  `distinguishes_iff_ne` shows this is exactly inequality of the represented `ZFSet`s.
  34  So the discrimination is not a relabelled Boolean: it is real set difference in
  35  Mathlib's ZF universe. The endpoints are the genuine ∅ and {∅}. `zfSystem` is
  36  `Expressive`, realizes the δ core (`zfSystem_embeds_delta`), and falls on the δ
  37  side of the distinction dichotomy (`zfSystem_not_degenerate`).
  38
  39  The δ conclusion concerns the distinction, and the injection preserves it exactly;
  40  enlarging the token carrier (which the universe wall forbids inside this interface)
  41  cannot change it.
  42
  43  No project-local axioms. No sorry.
  44-/
  45
  46import Mathlib.SetTheory.ZFC.Basic
  47import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCDistinctionDichotomy
  48
  49namespace IndisputableMonolith
  50namespace Foundation
  51namespace PrimitiveRecognitionCalculus
  52namespace FullZFCParse
  53
  54open FormalSystem
  55
  56/-- The ZF universe, pinned to a fixed universe level (the `FormalSystem` interface
  57is `Type`-0, so we work at the smallest level). -/
  58abbrev ZF := ZFSet.{0}
  59
  60/-- ∅ and {∅} are distinct as sets: ∅ ∈ {∅} but ∅ ∉ ∅. The von Neumann 0 and 1. -/
  61theorem empty_ne_singleton : (∅ : ZF) ≠ ({∅} : ZF) := by
  62  intro h
  63  have h1 : (∅ : ZF) ∈ ({∅} : ZF) := ZFSet.mem_singleton.mpr rfl
  64  rw [← h] at h1
  65  exact ZFSet.notMem_empty ∅ h1
  66
  67/-- The distinction between ∅ and {∅} is genuinely extensional: they differ in the
  68member ∅. -/
  69theorem empty_distinct_singleton_extensionally :
  70    ∃ z : ZF, ¬ (z ∈ (∅ : ZF) ↔ z ∈ ({∅} : ZF)) := by
  71  refine ⟨∅, ?_⟩
  72  intro h
  73  exact ZFSet.notMem_empty ∅ (h.mpr (ZFSet.mem_singleton.mpr rfl))
  74
  75/-- **Axiom of infinity, modelled.** The von Neumann ω contains ∅ and is closed
  76under the successor operation x ↦ x ∪ {x} = `insert x x`. This is exactly what HF
  77set theory could not provide. -/
  78theorem infinity_modeled :
  79    (∅ : ZF) ∈ ZFSet.omega ∧ ∀ n, n ∈ ZFSet.omega → insert n n ∈ ZFSet.omega :=
  80  ⟨ZFSet.omega_zero, fun _ h => ZFSet.omega_succ h⟩
  81
  82/-- The infinite set ω is distinct from the empty set: the carrier genuinely
  83contains an infinite set. -/
  84theorem omega_ne_empty : ZFSet.omega ≠ (∅ : ZF) := by
  85  intro h
  86  have hz : (∅ : ZF) ∈ ZFSet.omega := ZFSet.omega_zero
  87  rw [h] at hz
  88  exact ZFSet.notMem_empty ∅ hz
  89
  90/-- Faithful injection of a Type-0 token set into the ZF universe: `false ↦ ∅`,
  91`true ↦ {∅}`. The universe wall (`Token : Type` but `ZFSet : Type 1`) forces the
  92token carrier to be small; the injection carries it into the genuine ZF universe. -/
  93noncomputable def zfWitness : Bool → ZF
  94  | false => ∅
  95  | true => {∅}
  96
  97/-- The token-to-set map is injective: distinct tokens name distinct ZF sets. -/
  98theorem zfWitness_injective : Function.Injective zfWitness := by
  99  intro a b h
 100  cases a <;> cases b <;> simp only [zfWitness] at h <;>
 101    first
 102      | rfl
 103      | exact absurd h empty_ne_singleton
 104      | exact absurd h.symm empty_ne_singleton
 105
 106/-- Full ZFC parsed into the `FormalSystem` interface. Tokens are a small carrier
 107injected into the ZF universe; the discrimination relation is GENUINE ZF extensional
 108difference of the represented sets; the endpoints are the real ∅ and {∅}; the
 109expression order is the derivation-length order. -/
 110noncomputable def zfSystem : FormalSystem where
 111  Token := Bool
 112  Expr := ℕ
 113  distinguishes := fun a b => ∃ z : ZF, ¬ (z ∈ zfWitness a ↔ z ∈ zfWitness b)
 114  exprExtends := fun m n => m ≤ n
 115  endpointToken := fun e =>
 116    match e.side with
 117    | Side.left => false
 118    | Side.right => true
 119  traceExpr := Trace.length
 120  traceExpr_extends := fun h => InevitabilityInstances.length_le_of_extends h
 121
 122/-- The discrimination relation IS inequality of the represented ZF sets: two tokens
 123are distinguished exactly when the sets they name differ in some member. So the
 124parse discriminates by real set difference, not by token accident. -/
 125theorem distinguishes_iff_ne (a b : Bool) :
 126    zfSystem.distinguishes a b ↔ zfWitness a ≠ zfWitness b := by
 127  show (∃ z : ZF, ¬ (z ∈ zfWitness a ↔ z ∈ zfWitness b)) ↔ zfWitness a ≠ zfWitness b
 128  rw [ne_eq, ZFSet.ext_iff, not_forall]
 129
 130/-- `zfSystem` distinguishes its endpoints: the genuine ∅ and {∅} differ
 131extensionally. -/
 132theorem zfSystem_expressive : zfSystem.Expressive := by
 133  show ∃ z : ZF, ¬ (z ∈ (∅ : ZF) ↔ z ∈ ({∅} : ZF))
 134  exact empty_distinct_singleton_extensionally
 135
 136/-- **Full ZFC contains the δ core.** -/
 137theorem zfSystem_embeds_delta : Nonempty (PRCEmbeddingInto zfSystem) :=
 138  FormalSystemEmbeddingTarget_proved zfSystem zfSystem_expressive
 139
 140theorem zfSystem_exprReflexive : DistinctionDichotomy.ExprReflexive zfSystem :=
 141  fun n => Nat.le_refl n
 142
 143/-- Full ZFC falls on the δ side of the distinction dichotomy: it is non-degenerate,
 144hence realizes δ. -/
 145theorem zfSystem_not_degenerate : ¬ DistinctionDichotomy.Degenerate zfSystem :=
 146  DistinctionDichotomy.not_degenerate_of_realizesDelta zfSystem zfSystem_embeds_delta
 147
 148/-- **The faithful parse, packaged.** Full ZFC (Mathlib's `ZFSet`): (i) satisfies
 149extensionality, (ii) has ∅ ≠ {∅} as sets, (iii) discriminates by genuine ZF
 150extensional difference, (iv) models the axiom of infinity (ω with ∅ and successor
 151closure), and (v) realizes the δ core. -/
 152theorem full_zfc_realizes_delta :
 153    (∀ a b : ZF, a = b ↔ ∀ z, z ∈ a ↔ z ∈ b)
 154      ∧ ((∅ : ZF) ≠ ({∅} : ZF))
 155      ∧ (∀ a b : Bool, zfSystem.distinguishes a b ↔ zfWitness a ≠ zfWitness b)
 156      ∧ ((∅ : ZF) ∈ ZFSet.omega ∧ ∀ n, n ∈ ZFSet.omega → insert n n ∈ ZFSet.omega)
 157      ∧ Nonempty (PRCEmbeddingInto zfSystem) :=
 158  ⟨fun _ _ => ZFSet.ext_iff, empty_ne_singleton, distinguishes_iff_ne,
 159    infinity_modeled, zfSystem_embeds_delta⟩
 160
 161end FullZFCParse
 162end PrimitiveRecognitionCalculus
 163end Foundation
 164end IndisputableMonolith
 165