IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCSetTheoryParse

   1/-
   2  PrimitiveRecognitionCalculus/PRCSetTheoryParse.lean
   3
   4  Item 4 of the δ frontier, first real corpus parse: hereditarily finite set
   5  theory (ZFC minus the axiom of infinity), faithfully encoded, shown to contain δ.
   6
   7  Prior δ4 work gave a toy set-theory witness: `ofTwoDistinct (∅ : Set Unit) univ`,
   8  which is really just a two-point Boolean. That does not parse set theory; it
   9  relabels a truth value. This module does the genuine thing.
  10
  11  We use the Ackermann coding of the hereditarily finite sets: a natural number `n`
  12  codes the HF set whose members are exactly the codes `i` with bit `i` of `n` set,
  13
  14      i ∈ n   ⟺   bit i of n is 1.
  15
  16  This is the standard bijection between ℕ and the hereditarily finite sets, the
  17  canonical model of ZFC with infinity removed (equivalently, V_ω). On this coding:
  18
  19  * EXTENSIONALITY holds (`ext_iff`): two codes are equal iff they have the same
  20    members. This is the axiom of extensionality, and it is exactly ℕ bit
  21    extensionality.
  22  * The EMPTY SET is coded by 0 (`not_mem_empty`): it has no members.
  23  * The SINGLETON {∅} is coded by 1 (`mem_one_iff`): its only member is 0 = ∅.
  24  * Hence ∅ ≠ {∅} as SETS, because they have different members, not merely
  25    different codes (`distinguishes_iff_extensional`).
  26
  27  `hfSystem` parses this foundation into the `FormalSystem` interface: tokens are HF
  28  set codes, the discrimination relation is the foundation's own extensional set
  29  inequality, the endpoints are the genuine ∅ and {∅} (the von Neumann 0 and 1).
  30  It is `Expressive`, so it realizes the δ core, and it falls on the δ side of the
  31  distinction dichotomy.
  32
  33  HONEST BOUNDARY (now lifted by `PRCFullZFCParse.lean`). This module is HF set
  34  theory (ZFC − infinity): every code is a finite set, so the axiom of infinity is
  35  not modelled here. The δ core needs only the extensional distinction, which HF
  36  already provides. Full ZFC WITH the axiom of infinity is handled in
  37  `PRCFullZFCParse.lean`, over Mathlib's `ZFSet`, where infinity is proved and the
  38  δ embedding still holds; as expected, infinity does not change the δ conclusion.
  39  Type theory (`PRCTypeTheoryParse.lean`) and category theory
  40  (`PRCCategoryTheoryParse.lean`) are parsed the same way; the dichotomy makes each
  41  a matter of exhibiting one extensional distinction.
  42
  43  No project-local axioms. No sorry.
  44-/
  45
  46import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCDistinctionDichotomy
  47
  48namespace IndisputableMonolith
  49namespace Foundation
  50namespace PrimitiveRecognitionCalculus
  51namespace SetTheoryParse
  52
  53open FormalSystem
  54
  55/-- Ackermann membership: code `i` is a member of code `n` iff bit `i` of `n` is
  56set. This is the ∈ relation of the hereditarily finite sets under the standard
  57coding. -/
  58def Mem (i n : ℕ) : Prop := Nat.testBit n i = true
  59
  60/-- **Extensionality.** Two HF codes are equal iff they have the same members. The
  61Ackermann interpretation satisfies the axiom of extensionality; it is exactly ℕ bit
  62extensionality. -/
  63theorem ext_iff (m n : ℕ) : m = n ↔ ∀ i, (Mem i m ↔ Mem i n) := by
  64  refine ⟨fun h i => by rw [h], fun h => Nat.eq_of_testBit_eq fun i => ?_⟩
  65  have hi := h i
  66  cases hm : Nat.testBit m i <;> cases hn : Nat.testBit n i <;> simp_all [Mem]
  67
  68/-- The empty set is coded by `0`: it has no members. -/
  69theorem not_mem_empty (i : ℕ) : ¬ Mem i 0 := by
  70  simp [Mem]
  71
  72/-- The singleton `{∅}` is coded by `1`: its only member is `0 = ∅`. -/
  73theorem mem_one_iff (i : ℕ) : Mem i 1 ↔ i = 0 := by
  74  cases i with
  75  | zero => exact iff_of_true (by show Nat.testBit 1 0 = true; decide) rfl
  76  | succ j =>
  77      refine iff_of_false ?_ (Nat.succ_ne_zero j)
  78      have h2 : (1 : ℕ) / 2 = 0 := by decide
  79      simp [Mem, Nat.testBit_succ, h2]
  80
  81/-- HF set theory parsed into the `FormalSystem` interface. Tokens are HF set
  82codes; the discrimination relation is extensional set inequality; the endpoints are
  83the genuine ∅ (code 0) and {∅} (code 1); the expression order is the
  84derivation-length order, which preserves trace extension. -/
  85def hfSystem : FormalSystem where
  86  Token := ℕ
  87  Expr := ℕ
  88  distinguishes := fun a b => a ≠ b
  89  exprExtends := fun m n => m ≤ n
  90  endpointToken := fun e =>
  91    match e.side with
  92    | Side.left => 0
  93    | Side.right => 1
  94  traceExpr := Trace.length
  95  traceExpr_extends := fun h => InevitabilityInstances.length_le_of_extends h
  96
  97/-- The discrimination relation IS the foundation's own extensional set inequality:
  98two codes are distinguished exactly when they differ in some member. So `hfSystem`
  99discriminates by genuine set difference, not by code accident. -/
 100theorem distinguishes_iff_extensional (a b : ℕ) :
 101    hfSystem.distinguishes a b ↔ ∃ i, ¬ (Mem i a ↔ Mem i b) := by
 102  show a ≠ b ↔ ∃ i, ¬ (Mem i a ↔ Mem i b)
 103  rw [ne_eq, ext_iff a b]
 104  push_neg
 105  rfl
 106
 107/-- `hfSystem` distinguishes its endpoints: ∅ ≠ {∅}. -/
 108theorem hfSystem_expressive : hfSystem.Expressive := by
 109  show (0 : ℕ) ≠ 1
 110  decide
 111
 112/-- **HF set theory contains the δ core.** -/
 113theorem hfSystem_embeds_delta : Nonempty (PRCEmbeddingInto hfSystem) :=
 114  FormalSystemEmbeddingTarget_proved hfSystem hfSystem_expressive
 115
 116theorem hfSystem_exprReflexive : DistinctionDichotomy.ExprReflexive hfSystem :=
 117  fun n => Nat.le_refl n
 118
 119/-- HF set theory falls on the δ side of the distinction dichotomy: it is
 120non-degenerate, hence realizes δ. -/
 121theorem hfSystem_not_degenerate : ¬ DistinctionDichotomy.Degenerate hfSystem :=
 122  DistinctionDichotomy.not_degenerate_of_realizesDelta hfSystem hfSystem_embeds_delta
 123
 124/-- **The faithful parse, packaged.** HF set theory, encoded by Ackermann coding,
 125(i) satisfies extensionality, (ii) has ∅ = code 0 with no members, (iii) has
 126{∅} = code 1 with exactly the member ∅, (iv) discriminates by genuine set
 127difference, and (v) realizes the δ core. The endpoints ∅ and {∅} are the von
 128Neumann 0 and 1, distinguished as sets. -/
 129theorem hf_set_theory_realizes_delta :
 130    (∀ m n : ℕ, m = n ↔ ∀ i, (Mem i m ↔ Mem i n))
 131      ∧ (∀ i, ¬ Mem i 0)
 132      ∧ (∀ i, Mem i 1 ↔ i = 0)
 133      ∧ (∀ a b : ℕ, hfSystem.distinguishes a b ↔ ∃ i, ¬ (Mem i a ↔ Mem i b))
 134      ∧ Nonempty (PRCEmbeddingInto hfSystem) :=
 135  ⟨ext_iff, not_mem_empty, mem_one_iff, distinguishes_iff_extensional,
 136    hfSystem_embeds_delta⟩
 137
 138end SetTheoryParse
 139end PrimitiveRecognitionCalculus
 140end Foundation
 141end IndisputableMonolith
 142