From fb4a1c8b5fad14e305a1809b48cb02a94f31ecb9 Mon Sep 17 00:00:00 2001
From: palalansouki <palalansouki@gmail.com>
Date: Mon, 10 Nov 2025 18:48:21 +0900
Subject: [PATCH 1/5] name

---
 .../FirstOrder/SetTheory/Forcing/Name.lean    | 61 +++++++++++++++++++
 1 file changed, 61 insertions(+)
 create mode 100644 Foundation/FirstOrder/SetTheory/Forcing/Name.lean

diff --git a/Foundation/FirstOrder/SetTheory/Forcing/Name.lean b/Foundation/FirstOrder/SetTheory/Forcing/Name.lean
new file mode 100644
index 000000000..6f8c900ed
--- /dev/null
+++ b/Foundation/FirstOrder/SetTheory/Forcing/Name.lean
@@ -0,0 +1,61 @@
+import Foundation.FirstOrder.SetTheory.Z
+import Mathlib.Data.QPF.Univariate.Basic
+
+/-! # $\mathbf{P}$-name -/
+
+namespace LO.FirstOrder.SetTheory
+
+variable (ℙ : Type u) [Preorder ℙ]
+
+/-- ref:
+  https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/ZFSet.20and.20computability
+  https://github.com/vihdzp/combinatorial-games/blob/9130275873edbae2fba445e0c9fa4a9e17546b36/CombinatorialGames/Game/Functor.lean -/
+@[ext]
+structure NameFunctor (α : Type (u + 1)) : Type _ where
+  toFun : ℙ → Set α
+  small : ∀ p, Small.{u} (toFun p)
+  monotone {p q} : q ≤ p → toFun p ⊆ toFun q
+
+variable {ℙ}
+
+instance : CoeFun (NameFunctor ℙ α) (fun _ ↦ ℙ → Set α) := ⟨fun F ↦ F.toFun⟩
+
+instance (F : NameFunctor ℙ α) (p : ℙ) : Small.{u} (F p) := F.small p
+
+#check QPF.abs
+
+instance : Functor (NameFunctor ℙ) where
+  map m F := ⟨fun p ↦ m '' F p, fun _ ↦ inferInstance, fun h b ↦ by
+    simp only [Set.mem_image, forall_exists_index, and_imp]
+    rintro a ha rfl
+    exact ⟨a, F.monotone h ha, rfl⟩⟩
+
+variable {F : NameFunctor ℙ α}
+
+lemma mem_of_le {p q : ℙ} (x : F p) (hqp : q ≤ p) : ↑x ∈ F q := F.monotone hqp x.prop
+
+noncomputable
+instance : QPF (NameFunctor ℙ) where
+  P := ⟨(C : Type u) × (ℙ → Set C), fun s ↦ s.1⟩
+  abs {α} s := ⟨fun p ↦ s.2 '' s.1.2 p, fun _ ↦ inferInstance, fun h a ↦ by
+    simp
+    rintro c hc rfl
+    sorry⟩
+  repr F :=
+    let C := (p : ℙ) × Shrink (F p)
+    ⟨⟨C, fun p ↦ {c | p ≤ c.1}⟩, fun c ↦ ((equivShrink _).symm c.2).val⟩
+  abs_repr {α} F := by
+    ext p a; simp
+    constructor
+    · rintro ⟨q, h, x, rfl⟩
+      exact mem_of_le _ h
+    · rintro ha
+      refine ⟨p, by rfl, equivShrink (F p) ⟨a, ha⟩, by simp⟩
+  abs_map := by {
+    rintro α β m ⟨⟨C, s⟩, s⟩
+    simp at s
+    ext p b; simp
+    sorry
+   }
+
+end LO.FirstOrder.SetTheory

From 4722d173693e32d457b2f1c3ab824493d66ff395 Mon Sep 17 00:00:00 2001
From: palalansouki <palalansouki@gmail.com>
Date: Tue, 11 Nov 2025 01:47:07 +0900
Subject: [PATCH 2/5] =?UTF-8?q?Name=20=E2=84=99?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Foundation/FirstOrder/Kripke/Basic.lean       |  11 +-
 .../FirstOrder/SetTheory/Forcing/Name.lean    | 110 +++++++++++++++---
 2 files changed, 100 insertions(+), 21 deletions(-)

diff --git a/Foundation/FirstOrder/Kripke/Basic.lean b/Foundation/FirstOrder/Kripke/Basic.lean
index ed9cc086f..c03aaedce 100644
--- a/Foundation/FirstOrder/Kripke/Basic.lean
+++ b/Foundation/FirstOrder/Kripke/Basic.lean
@@ -4,13 +4,18 @@ import Foundation.Logic.Predicate.Relational
 import Foundation.Logic.ForcingRelation
 import Mathlib.Order.PFilter
 
-namespace LO.FirstOrder
+namespace LO
+
+abbrev IsSetMonotone {α : Type*} (R : α → α → Prop) (f : α → Set β) :=
+  ∀ {a b}, R a b → f a ⊆ f b
+
+namespace FirstOrder
 
 /-- Kripke model for relational first-order language -/
 class KripkeModel (L : outParam Language) [L.Relational] (World : Type*) [Preorder World] (Carrier : outParam Type*) where
   Domain : World → Set Carrier
-  domain_nonempty : ∀ w, ∃ x, x ∈ Domain w
-  domain_antimonotone : w ≥ v → Domain w ⊆ Domain v
+  domain_nonempty : ∀ w, Set.Nonempty (Domain w)
+  domain_antimonotone : IsSetMonotone (· ≥ ·) Domain
   Rel (w : World) {k : ℕ} (R : L.Rel k) : (Fin k → Carrier) → Prop
   rel_monotone : Rel w R t → ∀ v ≤ w, Rel v R t
 
diff --git a/Foundation/FirstOrder/SetTheory/Forcing/Name.lean b/Foundation/FirstOrder/SetTheory/Forcing/Name.lean
index 6f8c900ed..f8eb861c4 100644
--- a/Foundation/FirstOrder/SetTheory/Forcing/Name.lean
+++ b/Foundation/FirstOrder/SetTheory/Forcing/Name.lean
@@ -1,7 +1,18 @@
+import Foundation.FirstOrder.Kripke.Basic
 import Foundation.FirstOrder.SetTheory.Z
 import Mathlib.Data.QPF.Univariate.Basic
 
-/-! # $\mathbf{P}$-name -/
+/-! # $\mathbb{P}$-name -/
+
+section Small
+
+variable {α β : Type*}
+
+def small_preimage_of_injective (f : α → β) (h : Function.Injective f) (s : Set β) [Small.{u} s] :
+    Small.{u} (f ⁻¹' s) := small_of_injective (β := s) (f := fun x ↦ ⟨f x, x.prop⟩) fun x y ↦ by
+  simp [Function.Injective.eq_iff h, SetCoe.ext_iff]
+
+end Small
 
 namespace LO.FirstOrder.SetTheory
 
@@ -14,16 +25,18 @@ variable (ℙ : Type u) [Preorder ℙ]
 structure NameFunctor (α : Type (u + 1)) : Type _ where
   toFun : ℙ → Set α
   small : ∀ p, Small.{u} (toFun p)
-  monotone {p q} : q ≤ p → toFun p ⊆ toFun q
+  monotone : IsSetMonotone (· ≥ ·) toFun
+
+attribute [coe] NameFunctor.toFun
 
 variable {ℙ}
 
+namespace NameFunctor
+
 instance : CoeFun (NameFunctor ℙ α) (fun _ ↦ ℙ → Set α) := ⟨fun F ↦ F.toFun⟩
 
 instance (F : NameFunctor ℙ α) (p : ℙ) : Small.{u} (F p) := F.small p
 
-#check QPF.abs
-
 instance : Functor (NameFunctor ℙ) where
   map m F := ⟨fun p ↦ m '' F p, fun _ ↦ inferInstance, fun h b ↦ by
     simp only [Set.mem_image, forall_exists_index, and_imp]
@@ -32,30 +45,91 @@ instance : Functor (NameFunctor ℙ) where
 
 variable {F : NameFunctor ℙ α}
 
+@[simp] lemma map_app (m : α → β) (p : ℙ) : (m <$> F) p = m '' F p := by rfl
+
 lemma mem_of_le {p q : ℙ} (x : F p) (hqp : q ≤ p) : ↑x ∈ F q := F.monotone hqp x.prop
 
-noncomputable
-instance : QPF (NameFunctor ℙ) where
-  P := ⟨(C : Type u) × (ℙ → Set C), fun s ↦ s.1⟩
-  abs {α} s := ⟨fun p ↦ s.2 '' s.1.2 p, fun _ ↦ inferInstance, fun h a ↦ by
-    simp
+variable (ℙ)
+
+abbrev MonotoneFunction (C : Type u) := {f : ℙ → Set C // IsSetMonotone (· ≥ ·) f}
+
+noncomputable instance qpf : QPF.{u + 1, u + 1, u + 1} (NameFunctor ℙ) where
+  P := ⟨(C : Type u) × MonotoneFunction ℙ C, fun s ↦ PLift s.1⟩
+  abs {α} s := ⟨fun p ↦ s.2 ∘ PLift.up '' s.1.2.val p, fun _ ↦ inferInstance, fun h a ↦ by
+    simp only [Set.mem_image, forall_exists_index, and_imp]
     rintro c hc rfl
-    sorry⟩
+    exact ⟨c, s.1.2.property h hc, by rfl⟩⟩
   repr F :=
     let C := (p : ℙ) × Shrink (F p)
-    ⟨⟨C, fun p ↦ {c | p ≤ c.1}⟩, fun c ↦ ((equivShrink _).symm c.2).val⟩
+    ⟨⟨C, fun p ↦ {c | p ≤ c.1}, fun h c ha ↦ le_trans h ha⟩, fun c ↦ ((equivShrink _).symm c.down.2).val⟩
   abs_repr {α} F := by
-    ext p a; simp
+    ext p a
+    suffices (∃ q, p ≤ q ∧ ∃ x, (equivShrink (F q)).symm x = a) ↔ a ∈ F p by simpa
     constructor
     · rintro ⟨q, h, x, rfl⟩
       exact mem_of_le _ h
     · rintro ha
       refine ⟨p, by rfl, equivShrink (F p) ⟨a, ha⟩, by simp⟩
-  abs_map := by {
-    rintro α β m ⟨⟨C, s⟩, s⟩
-    simp at s
-    ext p b; simp
-    sorry
-   }
+  abs_map := by
+    rintro α β m ⟨⟨C, s⟩, f⟩
+    ext p b; simp [PFunctor.map]
+
+@[simp] lemma liftp_iff {P : α → Prop} {f : NameFunctor ℙ α} :
+    Functor.Liftp P f ↔ ∀ p, ∀ a ∈ f p, P a := by
+  constructor
+  · rintro ⟨u, rfl⟩
+    intro p; simp; tauto
+  · intro h
+    refine ⟨
+      ⟨fun p ↦ Subtype.val ⁻¹' f p,
+       fun p ↦ small_preimage_of_injective Subtype.val Subtype.val_injective (f p),
+       fun h ⟨a, _⟩ ha ↦ f.monotone h ha⟩, ?_⟩
+    ext p a
+    simp; tauto
+
+end NameFunctor
+
+variable (ℙ)
+
+/-- ℙ-name for forcing notion of set theory -/
+def Name : Type (u + 1) := QPF.Fix (NameFunctor ℙ)
+
+variable {ℙ}
+
+namespace Name
+
+/-- constructor of name -/
+noncomputable def mk (x : NameFunctor ℙ (Name ℙ)) : Name ℙ :=
+  QPF.Fix.mk x
+
+/-- destructor of name -/
+noncomputable def dest (σ : Name ℙ) : NameFunctor ℙ (Name ℙ) := QPF.Fix.dest σ
+
+/-- The underlying fibre of name -/
+noncomputable def fibre (σ : Name ℙ) : ℙ → Set (Name ℙ) := σ.dest
+
+instance fibre_small (σ : Name ℙ) (p : ℙ) : Small.{u} (σ.fibre p) := σ.dest.small p
+
+@[simp] lemma fibre_monotone (σ : Name ℙ) : IsSetMonotone (· ≥ ·) σ.fibre := σ.dest.monotone
+
+@[simp] lemma mk_dest (σ : Name ℙ) : .mk σ.dest = σ := QPF.Fix.mk_dest _
+
+@[simp] lemma dest_mk (x : NameFunctor ℙ (Name ℙ)) :
+    (mk x).dest = x := QPF.Fix.dest_mk x
+
+@[simp] lemma fibre_mk (f : NameFunctor ℙ (Name ℙ)) : (mk f).fibre p = f p := by simp [fibre]
+
+noncomputable def rec (g : NameFunctor ℙ α → α) : Name ℙ → α := QPF.Fix.rec g
+
+lemma rec_mk (g : NameFunctor ℙ α → α) (x : NameFunctor ℙ (Name ℙ)) :
+    rec g (mk x) = g (rec g <$> x) := QPF.Fix.rec_eq _ _
+
+theorem ind
+    {P : Name ℙ → Prop}
+    (ind : ∀ σ, (∀ p, ∀ τ ∈ σ.fibre p, P τ) → P σ)
+    (σ : Name ℙ) : P σ :=
+  QPF.Fix.ind P (fun f hf ↦ ind (mk f) (by simpa using hf)) σ
+
+end Name
 
 end LO.FirstOrder.SetTheory

From 498a7130f718c200a3325b485ae7a35f0b811812 Mon Sep 17 00:00:00 2001
From: palalansouki <palalansouki@gmail.com>
Date: Tue, 11 Nov 2025 04:31:19 +0900
Subject: [PATCH 3/5] universe

---
 .../FirstOrder/SetTheory/Forcing/Name.lean    |  14 +-
 .../FirstOrder/SetTheory/StandardModel.lean   | 140 +++++++++++++++---
 Foundation/Vorspiel/Small.lean                |  12 ++
 3 files changed, 133 insertions(+), 33 deletions(-)
 create mode 100644 Foundation/Vorspiel/Small.lean

diff --git a/Foundation/FirstOrder/SetTheory/Forcing/Name.lean b/Foundation/FirstOrder/SetTheory/Forcing/Name.lean
index f8eb861c4..ffe55b9af 100644
--- a/Foundation/FirstOrder/SetTheory/Forcing/Name.lean
+++ b/Foundation/FirstOrder/SetTheory/Forcing/Name.lean
@@ -1,19 +1,11 @@
 import Foundation.FirstOrder.Kripke.Basic
 import Foundation.FirstOrder.SetTheory.Z
+import Foundation.Vorspiel.Small
 import Mathlib.Data.QPF.Univariate.Basic
+import Mathlib.SetTheory.Cardinal.Aleph
 
 /-! # $\mathbb{P}$-name -/
 
-section Small
-
-variable {α β : Type*}
-
-def small_preimage_of_injective (f : α → β) (h : Function.Injective f) (s : Set β) [Small.{u} s] :
-    Small.{u} (f ⁻¹' s) := small_of_injective (β := s) (f := fun x ↦ ⟨f x, x.prop⟩) fun x y ↦ by
-  simp [Function.Injective.eq_iff h, SetCoe.ext_iff]
-
-end Small
-
 namespace LO.FirstOrder.SetTheory
 
 variable (ℙ : Type u) [Preorder ℙ]
@@ -130,6 +122,8 @@ theorem ind
     (σ : Name ℙ) : P σ :=
   QPF.Fix.ind P (fun f hf ↦ ind (mk f) (by simpa using hf)) σ
 
+
+
 end Name
 
 end LO.FirstOrder.SetTheory
diff --git a/Foundation/FirstOrder/SetTheory/StandardModel.lean b/Foundation/FirstOrder/SetTheory/StandardModel.lean
index 60dad6615..d403a4799 100644
--- a/Foundation/FirstOrder/SetTheory/StandardModel.lean
+++ b/Foundation/FirstOrder/SetTheory/StandardModel.lean
@@ -1,36 +1,130 @@
+import Foundation.Vorspiel.Small
 import Foundation.FirstOrder.SetTheory.Basic
-import Mathlib.SetTheory.ZFC.Class
+import Mathlib.Data.QPF.Univariate.Basic
+import Mathlib.SetTheory.Cardinal.Aleph
 
-/-! # Standard model of set theory -/
+/-!
+# Standard model of set theory
 
-namespace ZFSet
+reference:
+  https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/ZFSet.20and.20computability
+  https://github.com/vihdzp/combinatorial-games/blob/9130275873edbae2fba445e0c9fa4a9e17546b36/CombinatorialGames/Game/Functor.lean
 
-/-- ? -/
-noncomputable instance allFunctionDefinable (f : (Fin n → ZFSet.{u}) → ZFSet.{u}) : ZFSet.Definable n f where
-  out v := Quotient.out <| f fun i ↦ ZFSet.mk (v i)
+ -/
 
-noncomputable def choose₁ (x : ZFSet) : ZFSet := Classical.epsilon fun z ↦ z ∈ x
+namespace LO.FirstOrder.SetTheory
 
-lemma choose₁_mem_self {x : ZFSet} (h : x ≠ ∅) : x.choose₁ ∈ x := Classical.epsilon_spec (by contrapose! h; ext; simp_all)
+/-- QPF functor to generate universe -/
+@[ext]
+structure UniverseFunctor (α : Type (u + 1)) : Type _ where
+  set : Set α
+  small : Small.{u} set
 
-noncomputable def choice' (𝓧 : ZFSet) : ZFSet := image choose₁ 𝓧
+attribute [coe] UniverseFunctor.set
 
-lemma choice'_uniqueExists {𝓧 X : ZFSet}
-    (he : ∅ ∉ 𝓧)
-    (pairwise_disjoint : ∀ X ∈ 𝓧, ∀ Y ∈ 𝓧, (∃ z, z ∈ X ∧ z ∈ Y) → X = Y)
-    (hX : X ∈ 𝓧) : ∃! x, x ∈ 𝓧.choice' ∧ x ∈ X := by
-  apply ExistsUnique.intro X.choose₁
-  · exact ⟨ZFSet.mem_image.mpr ⟨X, hX, rfl⟩, choose₁_mem_self <| by rintro rfl; contradiction⟩
-  · rintro y ⟨hy, hyx⟩
-    rcases ZFSet.mem_image.mp hy with ⟨Y, hY, rfl⟩
-    have : X = Y :=
-      pairwise_disjoint X hX Y hY ⟨Y.choose₁, hyx, choose₁_mem_self <| by rintro rfl; contradiction⟩
-    rcases this
-    rfl
+namespace UniverseFunctor
 
-end ZFSet
+variable {α : Type (u + 1)}
 
-namespace LO.FirstOrder.SetTheory
+instance : SetLike (UniverseFunctor α) α where
+  coe := set
+  coe_injective' _ _ := UniverseFunctor.ext
+
+instance (s : UniverseFunctor α) : Small.{u} s.set := s.small
+
+instance : Functor UniverseFunctor.{u} where
+  map m f := ⟨m '' f.set, inferInstance⟩
+
+lemma mem_def {a : α} {f : UniverseFunctor α} : a ∈ f ↔ a ∈ f.set := by rfl
+
+@[simp] lemma mem_mk {a : α} {s : Set α} {h : Small.{u} s} : a ∈ UniverseFunctor.mk s h ↔ a ∈ s := by rfl
+
+@[simp] lemma map_functor (m : α → β) (f : UniverseFunctor α) : (m <$> f).set = m '' f := by rfl
+
+noncomputable instance : QPF.{u + 1, u + 1, u + 1} UniverseFunctor.{u} where
+  P := ⟨Type u, fun α ↦ PLift α⟩
+  abs p := ⟨Set.range p.2, inferInstance⟩
+  repr f := ⟨Shrink f.set, fun x ↦ ((equivShrink _).symm x.down).val⟩
+  abs_repr f := by
+    ext a; simp only [Set.mem_range, PLift.exists]
+    constructor
+    · rintro ⟨x, rfl⟩
+      simp
+    · intro ha
+      refine ⟨equivShrink _ ⟨a, ha⟩, by simp⟩
+  abs_map m p := by
+    ext b
+    rcases p
+    simp [PFunctor.map]
+
+@[simp] lemma liftp_iff {P : α → Prop} {f : UniverseFunctor α} :
+    Functor.Liftp P f ↔ ∀ a ∈ f, P a := by
+  constructor
+  · rintro ⟨f, rfl⟩
+    intro a
+    simp [mem_def]; tauto
+  · intro h
+    refine ⟨
+      ⟨Subtype.val ⁻¹' f, small_preimage_of_injective Subtype.val Subtype.val_injective f.set⟩, ?_⟩
+    ext p
+    simp; tauto
+
+end UniverseFunctor
+
+/-- The standard model of set theory -/
+def Universe : Type (u + 1) := QPF.Fix UniverseFunctor
+
+namespace Universe
+
+/-- constructor of name -/
+noncomputable def mk (s : Set Universe.{u}) [Small s] : Universe.{u} :=
+  QPF.Fix.mk ⟨s, inferInstance⟩
+
+/-- destructor of name -/
+noncomputable def dest (x : Universe) : UniverseFunctor Universe := QPF.Fix.dest x
+
+instance : SetLike Universe.{u} Universe.{u} where
+  coe x := x.dest.set
+  coe_injective' x y e := by
+    have h (x : Universe.{u}) : mk x.dest.set = x := QPF.Fix.mk_dest _
+    have : mk x.dest.set = mk y.dest.set := by simp_all
+    simpa [h] using this
+
+lemma mem_def {x y : Universe.{u}} : x ∈ y ↔ x ∈ y.dest.set := by rfl
+
+lemma mem_def' {x y : Universe.{u}} : x ∈ y ↔ x ∈ (y : Set Universe) := by rfl
+
+instance coe_small (x : Universe.{u}) : Small.{u} (x : Set Universe) := x.dest.small
+
+@[simp] lemma mk_coe (x : Universe.{u}) : mk (↑x : Set Universe.{u}) = x := QPF.Fix.mk_dest _
+
+@[simp] lemma coe_mk (s : Set Universe.{u}) [Small.{u} s] : ↑(mk s) = s :=
+  UniverseFunctor.ext_iff.mp <| QPF.Fix.dest_mk (F := UniverseFunctor) ⟨s, inferInstance⟩
+
+@[simp] lemma mem_mk {x} {s : Set Universe.{u}} [Small s] :
+    x ∈ mk s ↔ x ∈ s := by simp [mem_def']
+
+@[ext] lemma mem_ext {x y : Universe.{u}} (h : ∀ z, z ∈ x ↔ z ∈ y) : x = y := calc
+  x = mk (↑x : Set Universe.{u}) := by simp
+  _ = mk (↑y : Set Universe.{u}) := by
+    have : (↑x : Set Universe.{u}) = ↑y := by ext; simp [h]
+    congr
+  _ = y := by simp
+
+noncomputable def rec (g : (s : Set α) → [Small.{u} s] → α) : Universe → α :=
+  QPF.Fix.rec (F := UniverseFunctor) fun p ↦ g p.set
+
+lemma rec_mk (g : (s : Set α) → [Small.{u} s] → α) (s : Set Universe.{u}) [Small.{u} s] :
+    rec g (mk s) = g (rec g '' s) := by
+  simpa using QPF.Fix.rec_eq (F := UniverseFunctor) (fun p ↦ g p.set) ⟨s, inferInstance⟩
+
+theorem ind
+    {P : Universe.{u} → Prop}
+    (ind : ∀ x, (∀ y ∈ x, P y) → P x)
+    (x : Universe) : P x :=
+  QPF.Fix.ind P (fun s hs ↦ ind (mk s.set) (by simpa using hs)) x
+
+/--/
 
 namespace Standard
 
diff --git a/Foundation/Vorspiel/Small.lean b/Foundation/Vorspiel/Small.lean
new file mode 100644
index 000000000..fc4e00306
--- /dev/null
+++ b/Foundation/Vorspiel/Small.lean
@@ -0,0 +1,12 @@
+import Foundation.Vorspiel.Vorspiel
+import Mathlib.Logic.Small.Basic
+
+section Small
+
+variable {α β : Type*}
+
+def small_preimage_of_injective (f : α → β) (h : Function.Injective f) (s : Set β) [Small.{u} s] :
+    Small.{u} (f ⁻¹' s) := small_of_injective (β := s) (f := fun x ↦ ⟨f x, x.prop⟩) fun x y ↦ by
+  simp [Function.Injective.eq_iff h, SetCoe.ext_iff]
+
+end Small

From a076db978bc970f14145bde15e88e81e94ff1703 Mon Sep 17 00:00:00 2001
From: palalansouki <palalansouki@gmail.com>
Date: Fri, 14 Nov 2025 04:17:53 +0900
Subject: [PATCH 4/5] wf model

---
 .../SetTheory/WellFoundedModel.lean           | 36 +++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 Foundation/FirstOrder/SetTheory/WellFoundedModel.lean

diff --git a/Foundation/FirstOrder/SetTheory/WellFoundedModel.lean b/Foundation/FirstOrder/SetTheory/WellFoundedModel.lean
new file mode 100644
index 000000000..ed00fbcfc
--- /dev/null
+++ b/Foundation/FirstOrder/SetTheory/WellFoundedModel.lean
@@ -0,0 +1,36 @@
+import Foundation.FirstOrder.SetTheory.Basic
+
+/-!
+# Well-Founded Model of Set Theory
+
+In type theory, a transitive model (at the meta level) is nonsense. Therefore, we instead work with a well-founded model.
+-/
+
+namespace LO.FirstOrder.SetTheory
+
+class WellFoundedModel (V : Type*) extends SetStructure V where
+  wf : WellFounded (α := V) (· ∈ ·)
+
+namespace WellFoundedModel
+
+variable {V : Type*} [WellFoundedModel V]
+
+instance : IsWellFounded (α := V) (· ∈ ·) := ⟨wf⟩
+
+instance : WellFoundedRelation V where
+  rel := (· ∈ ·)
+  wf := wf
+
+noncomputable def rec' {C : V → Sort*}
+    (h : (x : V) → ((y : V) → y ∈ x → C y) → C x)
+    (x : V) : C x :=
+  WellFounded.recursion wf x h
+
+theorem ind {P : V → Prop}
+    (h : ∀ x, (∀ y ∈ x, P y) → P x)
+    (x : V) : P x :=
+  WellFounded.induction wf x h
+
+end WellFoundedModel
+
+end LO.FirstOrder.SetTheory

From ebabd4dfd403c9170a704cc4b19bda06bd05ee00 Mon Sep 17 00:00:00 2001
From: palalansouki <palalansouki@gmail.com>
Date: Sat, 15 Nov 2025 02:46:16 +0900
Subject: [PATCH 5/5] add Universe

---
 .../FirstOrder/SetTheory/StandardModel.lean   | 182 +++++++++++++-----
 .../SetTheory/WellFoundedModel.lean           |   7 +
 Foundation/Vorspiel/Small.lean                |   2 +-
 3 files changed, 141 insertions(+), 50 deletions(-)

diff --git a/Foundation/FirstOrder/SetTheory/StandardModel.lean b/Foundation/FirstOrder/SetTheory/StandardModel.lean
index d403a4799..d369ec398 100644
--- a/Foundation/FirstOrder/SetTheory/StandardModel.lean
+++ b/Foundation/FirstOrder/SetTheory/StandardModel.lean
@@ -83,6 +83,8 @@ noncomputable def mk (s : Set Universe.{u}) [Small s] : Universe.{u} :=
 /-- destructor of name -/
 noncomputable def dest (x : Universe) : UniverseFunctor Universe := QPF.Fix.dest x
 
+noncomputable def mkFun {ι : Type u} (f : ι → Universe.{u}) : Universe.{u} := mk (Set.range f)
+
 instance : SetLike Universe.{u} Universe.{u} where
   coe x := x.dest.set
   coe_injective' x y e := by
@@ -96,6 +98,8 @@ lemma mem_def' {x y : Universe.{u}} : x ∈ y ↔ x ∈ (y : Set Universe) := by
 
 instance coe_small (x : Universe.{u}) : Small.{u} (x : Set Universe) := x.dest.small
 
+instance coe_small' (x : Universe.{u}) : Small.{u} (x : Type _) := x.dest.small
+
 @[simp] lemma mk_coe (x : Universe.{u}) : mk (↑x : Set Universe.{u}) = x := QPF.Fix.mk_dest _
 
 @[simp] lemma coe_mk (s : Set Universe.{u}) [Small.{u} s] : ↑(mk s) = s :=
@@ -104,7 +108,13 @@ instance coe_small (x : Universe.{u}) : Small.{u} (x : Set Universe) := x.dest.s
 @[simp] lemma mem_mk {x} {s : Set Universe.{u}} [Small s] :
     x ∈ mk s ↔ x ∈ s := by simp [mem_def']
 
-@[ext] lemma mem_ext {x y : Universe.{u}} (h : ∀ z, z ∈ x ↔ z ∈ y) : x = y := calc
+@[simp] lemma mem_mkFun {x} {ι : Type u} {f : ι → Universe.{u}} :
+    x ∈ mkFun f ↔ ∃ i, f i = x := by simp [mkFun]
+
+@[simp] lemma coe_nonempty_iff_isNonempty {x : Universe} : (x : Set Universe).Nonempty ↔ IsNonempty x := by
+  simp [isNonempty_def]; rfl
+
+@[ext] lemma ext {x y : Universe.{u}} (h : ∀ z, z ∈ x ↔ z ∈ y) : x = y := calc
   x = mk (↑x : Set Universe.{u}) := by simp
   _ = mk (↑y : Set Universe.{u}) := by
     have : (↑x : Set Universe.{u}) = ↑y := by ext; simp [h]
@@ -118,123 +128,197 @@ lemma rec_mk (g : (s : Set α) → [Small.{u} s] → α) (s : Set Universe.{u})
     rec g (mk s) = g (rec g '' s) := by
   simpa using QPF.Fix.rec_eq (F := UniverseFunctor) (fun p ↦ g p.set) ⟨s, inferInstance⟩
 
+@[elab_as_elim]
 theorem ind
     {P : Universe.{u} → Prop}
     (ind : ∀ x, (∀ y ∈ x, P y) → P x)
     (x : Universe) : P x :=
   QPF.Fix.ind P (fun s hs ↦ ind (mk s.set) (by simpa using hs)) x
 
-/--/
+lemma wellFounded : WellFounded (α := Universe.{u}) (· ∈ ·) := ⟨ind fun x ih ↦ Acc.intro x ih⟩
+
+lemma minimal_exists_of_isNonempty {x : Universe.{u}} (hx : IsNonempty x) : ∃ y ∈ x, ∀ z ∈ x, z ∉ y := by
+  let z := WellFounded.min wellFounded x (by simp [hx])
+  exact ⟨z, WellFounded.min_mem wellFounded x _, fun w hw ↦ WellFounded.not_lt_min wellFounded x _ hw⟩
+
+noncomputable def empty : Universe := .mk {}
+
+noncomputable instance : Inhabited Universe := ⟨empty⟩
+
+@[simp] lemma mem_empty_iff {x : Universe} : ¬x ∈ empty := by simp [empty]
+
+protected noncomputable def insert (x y : Universe) : Universe := mk ({x} ∪ y)
+
+@[simp] lemma mem_insert_iff {x y z : Universe} : z ∈ x.insert y ↔ z = x ∨ z ∈ y := by simp [Universe.insert]
+
+noncomputable def ofNat : ℕ → Universe
+  |     0 => empty
+  | n + 1 => (ofNat n).insert (ofNat n)
+
+noncomputable def omega : Universe.{u} := mk (Set.range ofNat)
+
+@[simp] lemma empty_mem_omega : empty.{u} ∈ omega.{u} := by
+  simp only [omega, mem_mk, Set.mem_range]
+  exact ⟨0, by rfl⟩
+
+lemma omega_succ : x ∈ omega.{u} → x.insert x ∈ omega := by
+  simp only [omega, mem_mk, Set.mem_range, forall_exists_index]
+  rintro n rfl
+  exact ⟨n + 1, by rfl⟩
 
-namespace Standard
+noncomputable def image (x : Universe) (F : Universe → Universe) : Universe := mk (Set.image F x)
 
-@[simp] lemma isEmpty_iff_eq_empty {x : ZFSet.{u}} :
-    IsEmpty x ↔ x = ∅ := by
-  simpa [IsEmpty] using Iff.symm (ZFSet.eq_empty x)
+@[simp] lemma mem_image {F : Universe → Universe} {x z : Universe} :
+    z ∈ x.image F ↔ ∃ y ∈ x, F y = z := by simp [image]
 
-instance models_zf : ZFSet.{u} ⊧ₘ* 𝗭𝗙 where
+noncomputable def choice₁ (x : Universe) : Universe := Classical.epsilon fun z ↦ z ∈ x
+
+lemma choice₁_mem_self {x : Universe} (hx : IsNonempty x) : x.choice₁ ∈ x := Classical.epsilon_spec hx.nonempty
+
+lemma isNonempty_iff_ne_empty {x : Universe} : IsNonempty x ↔ x ≠ empty := by
+  simp [Universe.ext_iff, isNonempty_def]
+
+lemma isEmpty_iff_eq_empty {x : Universe} : IsEmpty x ↔ x = empty := by
+  simp [Universe.ext_iff, IsEmpty]
+
+noncomputable def choice (x : Universe) : Universe := x.image choice₁
+
+lemma choice_existsUnique {𝓧 X : Universe}
+    (he : empty ∉ 𝓧)
+    (pairwise_disjoint : ∀ X ∈ 𝓧, ∀ Y ∈ 𝓧, (∃ z, z ∈ X ∧ z ∈ Y) → X = Y)
+    (hX : X ∈ 𝓧) : ∃! x, x ∈ 𝓧.choice ∧ x ∈ X := by
+  apply ExistsUnique.intro X.choice₁
+  · exact ⟨mem_image.mpr ⟨X, hX, rfl⟩,
+      choice₁_mem_self <| isNonempty_iff_ne_empty.mpr <| by rintro rfl; contradiction⟩
+  · rintro y ⟨hy, hyx⟩
+    rcases mem_image.mp hy with ⟨Y, hY, rfl⟩
+    have : X = Y :=
+      pairwise_disjoint X hX Y hY ⟨Y.choice₁, hyx,
+        choice₁_mem_self <| isNonempty_iff_ne_empty.mpr <| by rintro rfl; contradiction⟩
+    rcases this
+    rfl
+
+noncomputable def sep (x : Universe.{u}) (p : Universe.{u} → Prop) : Universe.{u} := mk {z ∈ x | p z}
+
+@[simp] lemma mem_spec {z x : Universe.{u}} {p : Universe.{u} → Prop} :
+    z ∈ sep x p ↔ z ∈ x ∧ p z := by simp [sep]
+
+noncomputable def powerset (x : Universe.{u}) : Universe.{u} :=
+  mkFun fun z : Shrink (Set.powerset (↑x : Set Universe)) ↦
+    sep x fun v ↦ v ∈ ((equivShrink _).symm z).val
+
+@[simp] lemma mem_powerset {z x : Universe.{u}} :
+    z ∈ x.powerset ↔ z ⊆ x := by
+  simp only [powerset, sep, mem_mkFun]
+  constructor
+  · rintro ⟨i, rfl⟩
+    intro z
+    simp; tauto
+  · intro hzx
+    refine ⟨equivShrink _ ⟨z, by simpa⟩, ?_⟩
+    simp [Universe.ext_iff]; tauto
+
+instance models_zf : Universe.{u} ⊧ₘ* 𝗭𝗙 where
   models_set φ hφ := by
     rcases hφ
     case axiom_of_equality h =>
-      have : ZFSet.{u} ⊧ₘ* (𝗘𝗤 : Theory ℒₛₑₜ) := inferInstance
+      have : Universe.{u} ⊧ₘ* (𝗘𝗤 : Theory ℒₛₑₜ) := inferInstance
       simpa [models_iff] using modelsTheory_iff.mp this h
     case axiom_of_empty_set =>
       suffices ∃ x, ∀ y, y ∉ x by simpa [models_iff, Axiom.empty]
-      exact ⟨∅, by simp⟩
+      exact ⟨empty, by simp⟩
     case axiom_of_extentionality =>
-      simp [models_iff, Axiom.extentionality, ZFSet.ext_iff]
+      simp [models_iff, Axiom.extentionality, Universe.ext_iff]
     case axiom_of_pairing =>
       suffices
-          ∀ x y : ZFSet.{u}, ∃ z, ∀ v, v ∈ z ↔ v = x ∨ v = y by
+          ∀ x y : Universe.{u}, ∃ z, ∀ v, v ∈ z ↔ v = x ∨ v = y by
         simpa [models_iff, Axiom.pairing]
       intro x y
-      exact ⟨{x, y}, by simp⟩
+      exact ⟨mk {x, y}, by simp⟩
     case axiom_of_union =>
       suffices
-          ∀ x : ZFSet.{u}, ∃ y, ∀ z, z ∈ y ↔ ∃ v ∈ x, z ∈ v by
+          ∀ x : Universe.{u}, ∃ y, ∀ z, z ∈ y ↔ ∃ v ∈ x, z ∈ v by
         simpa [models_iff, Axiom.union]
       intro x
-      exact ⟨x.sUnion, by simp⟩
+      exact ⟨mk (⋃ i : x, i), by simp⟩
     case axiom_of_power_set =>
       suffices
-          ∀ x : ZFSet.{u}, ∃ y, ∀ z, z ∈ y ↔ z ⊆ x by
+          ∀ x : Universe.{u}, ∃ y, ∀ z, z ∈ y ↔ z ⊆ x by
         simpa [models_iff, Axiom.power]
       intro x
       exact ⟨x.powerset, by simp⟩
     case axiom_of_infinity =>
       suffices
-          ∃ ω, (∅ ∈ ω) ∧
+          ∃ ω, (empty ∈ ω) ∧
             ∀ x ∈ ω, ∀ y, (∀ z, z ∈ y ↔ z = x ∨ z ∈ x) → y ∈ ω by
-        simpa [models_iff, Axiom.infinity, val_isSucc_iff]
-      refine ⟨ZFSet.omega, ?_, ?_⟩
+        simpa [models_iff, Axiom.infinity, val_isSucc_iff, isEmpty_iff_eq_empty]
+      refine ⟨omega, ?_, ?_⟩
       · simp
       · intro x hx y  hy
-        have : y = insert x x := by
+        have : y = x.insert x := by
           ext; simp_all
-        simpa [this] using ZFSet.omega_succ hx
+        simpa [this] using Universe.omega_succ hx
     case axiom_of_foundation =>
       suffices
-          ∀ x : ZFSet.{u}, IsNonempty x → ∃ y ∈ x, ∀ z ∈ x, z ∉ y by
+          ∀ x : Universe.{u}, IsNonempty x → ∃ y ∈ x, ∀ z ∈ x, z ∉ y by
         simpa [models_iff, Axiom.foundation]
       intro x hx
-      rcases hx with ⟨y, hx⟩
-      refine ⟨ZFSet.mem_wf.min x.toSet ⟨y, by simpa using hx⟩,
-        WellFounded.min_mem _ _ _,
-        fun _ hx ↦ ZFSet.mem_wf.not_lt_min _ _ (by simpa using hx)⟩
+      exact minimal_exists_of_isNonempty hx
     case axiom_of_separation φ =>
-      let P (f : ℕ → ZFSet.{u}) (x : ZFSet.{u}) : Prop :=
-        Semiformula.Eval (standardStructure ZFSet.{u}) ![x] f φ
+      let P (f : ℕ → Universe.{u}) (x : Universe.{u}) : Prop :=
+        Semiformula.Eval (standardStructure Universe.{u}) ![x] f φ
       suffices
-          ∀ (f : ℕ → ZFSet.{u}) (x : ZFSet.{u}),
-          ∃ y, ∀ z : ZFSet.{u}, z ∈ y ↔ z ∈ x ∧ P f z by
+          ∀ (f : ℕ → Universe.{u}) (x : Universe.{u}),
+          ∃ y, ∀ z : Universe.{u}, z ∈ y ↔ z ∈ x ∧ P f z by
         simpa [models_iff, Axiom.separationSchema, Matrix.constant_eq_singleton, P]
       intro f x
-      refine ⟨ZFSet.sep (P f) x, ?_⟩
+      refine ⟨sep x (P f), ?_⟩
       intro z; simp
     case axiom_of_replacement φ =>
-      let R (f : ℕ → ZFSet.{u}) (x y : ZFSet.{u}) : Prop :=
-        Semiformula.Eval (standardStructure ZFSet.{u}) ![x, y] f φ
+      let R (f : ℕ → Universe.{u}) (x y : Universe.{u}) : Prop :=
+        Semiformula.Eval (standardStructure Universe.{u}) ![x, y] f φ
       suffices
-          ∀ f : ℕ → ZFSet.{u},
+          ∀ f : ℕ → Universe.{u},
           (∀ x, ∃! y, R f x y) →
-          ∀ X : ZFSet.{u}, ∃ Y : ZFSet.{u}, ∀ y, y ∈ Y ↔ ∃ x ∈ X, R f x y by
+          ∀ X : Universe.{u}, ∃ Y : Universe.{u}, ∀ y, y ∈ Y ↔ ∃ x ∈ X, R f x y by
         simpa [models_iff, Axiom.replacementSchema, Matrix.constant_eq_singleton, Matrix.comp_vecCons']
       intro f h X
       have : ∀ x, ∃ y, R f x y := fun x ↦ (h x).exists
       choose F hF using this
-      have (x y : ZFSet) : R f x y ↔ F x = y :=
+      have (x y : Universe) : R f x y ↔ F x = y :=
         ⟨fun hxy ↦ (h x).unique (hF x) hxy, by rintro rfl; exact hF x⟩
-      refine ⟨ZFSet.image F X, fun _ ↦ by simp [this]⟩
+      refine ⟨X.image F, fun _ ↦ by simp [this]⟩
 
-instance models_ac : ZFSet.{u} ⊧ₘ* 𝗔𝗖 where
+instance models_ac : Universe.{u} ⊧ₘ* 𝗔𝗖 where
   models_set φ hφ := by
     rcases hφ
     suffices
-        ∀ 𝓧 : ZFSet.{u},
+        ∀ 𝓧 : Universe.{u},
           (∀ X ∈ 𝓧, IsNonempty X) →
           (∀ X ∈ 𝓧, ∀ Y ∈ 𝓧, (∃ x ∈ X, x ∈ Y) → X = Y) →
           ∃ C, ∀ X ∈ 𝓧, ∃! x, x ∈ C ∧ x ∈ X by
       simpa [models_iff, Axiom.choice]
     intro 𝓧 nonempty pairwise_disjoint
-    refine ⟨𝓧.choice', ?_⟩
+    refine ⟨𝓧.choice, ?_⟩
     intro X hX
-    exact 𝓧.choice'_uniqueExists
-      (by intro h; rcases nonempty ∅ h; simp_all) pairwise_disjoint hX
+    exact 𝓧.choice_existsUnique
+      (by intro h; rcases nonempty empty h; simp_all) pairwise_disjoint hX
+
 
-instance models_zfc : ZFSet.{u} ⊧ₘ* 𝗭𝗙𝗖 := inferInstance
+instance models_zfc : Universe.{u} ⊧ₘ* 𝗭𝗙𝗖 := inferInstance
 
-instance models_z : ZFSet.{u} ⊧ₘ* 𝗭 := ModelsTheory.of_ss inferInstance z_subset_zf
+instance models_z : Universe.{u} ⊧ₘ* 𝗭 := ModelsTheory.of_ss inferInstance z_subset_zf
 
-instance models_zc : ZFSet.{u} ⊧ₘ* 𝗭𝗖 := inferInstance
+instance models_zc : Universe.{u} ⊧ₘ* 𝗭𝗖 := inferInstance
 
-end Standard
+end Universe
 
-instance z_consistent : Entailment.Consistent 𝗭 := consistent_of_model 𝗭 ZFSet.{0}
+instance z_consistent : Entailment.Consistent 𝗭 := consistent_of_model 𝗭 Universe.{0}
 
-instance zc_consistent : Entailment.Consistent 𝗭𝗖 := consistent_of_model 𝗭𝗖 ZFSet.{0}
+instance zc_consistent : Entailment.Consistent 𝗭𝗖 := consistent_of_model 𝗭𝗖 Universe.{0}
 
-instance zf_consistent : Entailment.Consistent 𝗭𝗙 := consistent_of_model 𝗭𝗙 ZFSet.{0}
+instance zf_consistent : Entailment.Consistent 𝗭𝗙 := consistent_of_model 𝗭𝗙 Universe.{0}
 
-instance zfc_consistent : Entailment.Consistent 𝗭𝗙𝗖 := consistent_of_model 𝗭𝗙𝗖 ZFSet.{0}
+instance zfc_consistent : Entailment.Consistent 𝗭𝗙𝗖 := consistent_of_model 𝗭𝗙𝗖 Universe.{0}
 
 end LO.FirstOrder.SetTheory
diff --git a/Foundation/FirstOrder/SetTheory/WellFoundedModel.lean b/Foundation/FirstOrder/SetTheory/WellFoundedModel.lean
index ed00fbcfc..216bd448d 100644
--- a/Foundation/FirstOrder/SetTheory/WellFoundedModel.lean
+++ b/Foundation/FirstOrder/SetTheory/WellFoundedModel.lean
@@ -31,6 +31,13 @@ theorem ind {P : V → Prop}
     (x : V) : P x :=
   WellFounded.induction wf x h
 
+noncomputable def rankMin (s : Set V) (h : s.Nonempty) : V := WellFounded.min wf s h
+
+@[simp] lemma rankMin_mem (s : Set V) (h : s.Nonempty) : rankMin s h ∈ s := WellFounded.min_mem wf s h
+
+lemma not_mem_rankMin (s : Set V) (h : s.Nonempty) {x} (hx : x ∈ s) :
+    x ∉ rankMin s h := WellFounded.not_lt_min wf s h hx
+
 end WellFoundedModel
 
 end LO.FirstOrder.SetTheory
diff --git a/Foundation/Vorspiel/Small.lean b/Foundation/Vorspiel/Small.lean
index fc4e00306..58c2fbfd8 100644
--- a/Foundation/Vorspiel/Small.lean
+++ b/Foundation/Vorspiel/Small.lean
@@ -3,7 +3,7 @@ import Mathlib.Logic.Small.Basic
 
 section Small
 
-variable {α β : Type*}
+variable {α : Type uα} {β : Type uβ}
 
 def small_preimage_of_injective (f : α → β) (h : Function.Injective f) (s : Set β) [Small.{u} s] :
     Small.{u} (f ⁻¹' s) := small_of_injective (β := s) (f := fun x ↦ ⟨f x, x.prop⟩) fun x y ↦ by