Аналіз I, Глава 3.2

У цій главі ми пропонуємо версію теорії множин Цермело-Франкеля (з атомами), яка намагається максимально точно наслідувати оригінальний тексту Аналізу I, Глава 3.2. Вся нумерація посилається на оригінальний текст.

Я (пр.перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним рішенням Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підбуцнути", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Цей розділ переважно необов'язковий, хоча в ньому чітко зазначено аксіому регулярності, яка використовується в другорядній ролі у вправі в розділі 3.5.

Основні конструкції та результати цього розділу:

Парадокс Рассела (виключення аксіоми універсальної специфікації)
Аксіома регулярності - аксіома, розроблена для уникнення парадоксу Рассела

namespace Chapter3export SetTheory (Set Object)variable [SetTheory]

Аксіома 3.8 (Універсальне визначення)

abbrev axiom_of_universal_specification : Prop :=
  ∀ P : Object → Prop, ∃ A : Set, ∀ x : Object, x ∈ A ↔ P x

theorem Russells_paradox : ¬ axiom_of_universal_specification := byinst✝:SetTheory⊢ ¬axiom_of_universal_specification
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  intro hinst✝:SetTheoryh:axiom_of_universal_specification⊢ False
  set P : Object → Prop := fun x ↦ ∃ X:Set, x = X ∧ x ∉ Xinst✝:SetTheoryh:axiom_of_universal_specificationP:Object → Prop := fun x => ∃ X, x = SetTheory.set_to_object X ∧ x ∉ X⊢ False
  obtain ⟨Ω, hΩ⟩ := h Pintroinst✝:SetTheoryh:axiom_of_universal_specificationP:Object → Prop := fun x => ∃ X, x = SetTheory.set_to_object X ∧ x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P x⊢ False
  by_cases h: (Ω:Object) ∈ Ωposinst✝:SetTheoryh✝:axiom_of_universal_specificationP:Object → Prop := fun x => ∃ X, x = SetTheory.set_to_object X ∧ x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P xh:SetTheory.set_to_object Ω ∈ Ω⊢ Falseneginst✝:SetTheoryh✝:axiom_of_universal_specificationP:Object → Prop := fun x => ∃ X, x = SetTheory.set_to_object X ∧ x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P xh:SetTheory.set_to_object Ω ∉ Ω⊢ False
  .posinst✝:SetTheoryh✝:axiom_of_universal_specificationP:Object → Prop := fun x => ∃ X, x = SetTheory.set_to_object X ∧ x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P xh:SetTheory.set_to_object Ω ∈ Ω⊢ False have : P (Ω:Object) := (hΩ _).mp hposinst✝:SetTheoryh✝:axiom_of_universal_specificationP:Object → Prop := fun x => ∃ X, x = SetTheory.set_to_object X ∧ x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P xh:SetTheory.set_to_object Ω ∈ Ωthis:P (SetTheory.set_to_object Ω)⊢ False
    obtain ⟨ Ω', ⟨ hΩ1, hΩ2⟩ ⟩ := thispos.intro.introinst✝:SetTheoryh✝:axiom_of_universal_specificationP:Object → Prop := fun x => ∃ X, x = SetTheory.set_to_object X ∧ x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P xh:SetTheory.set_to_object Ω ∈ ΩΩ':SethΩ1:SetTheory.set_to_object Ω = SetTheory.set_to_object Ω'hΩ2:SetTheory.set_to_object Ω ∉ Ω'⊢ False
    simp at hΩ1pos.intro.introinst✝:SetTheoryh✝:axiom_of_universal_specificationP:Object → Prop := fun x => ∃ X, x = SetTheory.set_to_object X ∧ x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P xh:SetTheory.set_to_object Ω ∈ ΩΩ':SethΩ2:SetTheory.set_to_object Ω ∉ Ω'hΩ1:Ω = Ω'⊢ False
    rw [←hΩ1] at hΩ2pos.intro.introinst✝:SetTheoryh✝:axiom_of_universal_specificationP:Object → Prop := fun x => ∃ X, x = SetTheory.set_to_object X ∧ x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P xh:SetTheory.set_to_object Ω ∈ ΩΩ':SethΩ2:SetTheory.set_to_object Ω ∉ ΩhΩ1:Ω = Ω'⊢ False
    contradictionAll goals completed! 🐙
  have : P (Ω:Object) := byinst✝:SetTheory⊢ ¬axiom_of_universal_specification use ΩAll goals completed! 🐙
  replace this := (hΩ _).mpr thisneginst✝:SetTheoryh✝:axiom_of_universal_specificationP:Object → Prop := fun x => ∃ X, x = SetTheory.set_to_object X ∧ x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P xh:SetTheory.set_to_object Ω ∉ Ωthis:SetTheory.set_to_object Ω ∈ Ω⊢ False
  contradictionAll goals completed! 🐙

Аксіома 3.9 (Регулярність )

theorem SetTheory.Set.axiom_of_regularity {A:Set} (h: A ≠ ∅) :
    ∃ x:A, ∀ S:Set, x.val = S → Disjoint S A := byinst✝:SetTheoryA:Seth:A ≠ ∅⊢ ∃ x, ∀ (S : Set), ↑x = set_to_object S → Disjoint S A
  obtain ⟨ x, h, h' ⟩ := SetTheory.regularity_axiom A (nonempty_def h)intro.introinst✝:SetTheoryA:Seth✝:A ≠ ∅x:Objecth:mem x Ah':∀ (S : Set), x = set_to_object S → ¬∃ y, mem y A ∧ mem y S⊢ ∃ x, ∀ (S : Set), ↑x = set_to_object S → Disjoint S A
  use ⟨x, h⟩hinst✝:SetTheoryA:Seth✝:A ≠ ∅x:Objecth:mem x Ah':∀ (S : Set), x = set_to_object S → ¬∃ y, mem y A ∧ mem y S⊢ ∀ (S : Set), ↑⟨x, h⟩ = set_to_object S → Disjoint S A
  intro S hShinst✝:SetTheoryA:Seth✝:A ≠ ∅x:Objecth:mem x Ah':∀ (S : Set), x = set_to_object S → ¬∃ y, mem y A ∧ mem y SS:SethS:↑⟨x, h⟩ = set_to_object S⊢ Disjoint S A
  specialize h' S hShinst✝:SetTheoryA:Seth✝:A ≠ ∅x:Objecth:mem x AS:SethS:↑⟨x, h⟩ = set_to_object Sh':¬∃ y, mem y A ∧ mem y S⊢ Disjoint S A
  rw [disjoint_iff, eq_empty_iff_forall_notMem]hinst✝:SetTheoryA:Seth✝:A ≠ ∅x:Objecth:mem x AS:SethS:↑⟨x, h⟩ = set_to_object Sh':¬∃ y, mem y A ∧ mem y S⊢ ∀ (x : Object), x ∉ S ∩ A
  contrapose! h'hinst✝:SetTheoryA:Seth✝:A ≠ ∅x:Objecth:mem x AS:SethS:↑⟨x, h⟩ = set_to_object Sh':∃ x, x ∈ S ∩ A⊢ ∃ y, mem y A ∧ mem y S
  simp at h'hinst✝:SetTheoryA:Seth✝:A ≠ ∅x:Objecth:mem x AS:SethS:↑⟨x, h⟩ = set_to_object Sh':∃ x ∈ S, x ∈ A⊢ ∃ y, mem y A ∧ mem y S
  obtain ⟨ y, h1, h2 ⟩ := h'h.intro.introinst✝:SetTheoryA:Seth✝:A ≠ ∅x:Objecth:mem x AS:SethS:↑⟨x, h⟩ = set_to_object Sy:Objecth1:y ∈ Sh2:y ∈ A⊢ ∃ y, mem y A ∧ mem y S
  exact ⟨ y, h2, h1 ⟩All goals completed! 🐙

Вправа 3.2.1. Дух цієї вправи полягає в тому, щоб встановити ці результати без використання парадоксу Рассела чи порожньої множини.

theorem declaration uses 'sorry'SetTheory.Set.emptyset_exists (h: axiom_of_universal_specification):
    ∃ (X:Set), ∀ x, x ∉ X := byinst✝:SetTheoryh:axiom_of_universal_specification⊢ ∃ X, ∀ (x : Object), x ∉ X
  sorryAll goals completed! 🐙

Вправа 3.2.1. Дух цієї вправи полягає в тому, щоб встановити ці результати без використання парадоксу Рассела чи сінглетона.

theorem declaration uses 'sorry'SetTheory.Set.singleton_exists (h: axiom_of_universal_specification) (x:Object):
    ∃ (X:Set), ∀ y, y ∈ X ↔ y = x := byinst✝:SetTheoryh:axiom_of_universal_specificationx:Object⊢ ∃ X, ∀ (y : Object), y ∈ X ↔ y = x
  sorryAll goals completed! 🐙

Вправа 3.2.1. Дух цієї вправи полягає в тому, щоб встановити ці результати без використання парадоксу Рассела чи пари.

theorem declaration uses 'sorry'SetTheory.Set.pair_exists (h: axiom_of_universal_specification) (x₁ x₂:Object):
    ∃ (X:Set), ∀ y, y ∈ X ↔ y = x₁ ∨ y = x₂ := byinst✝:SetTheoryh:axiom_of_universal_specificationx₁:Objectx₂:Object⊢ ∃ X, ∀ (y : Object), y ∈ X ↔ y = x₁ ∨ y = x₂
  sorryAll goals completed! 🐙

Вправа 3.2.1. Дух цієї вправи полягає в тому, щоб встановити ці результати без використання парадоксу Рассела чи операції об'єднання.

theorem declaration uses 'sorry'SetTheory.Set.union_exists (h: axiom_of_universal_specification) (A B:Set):
    ∃ (Z:Set), ∀ z, z ∈ Z ↔ z ∈ A ∨ z ∈ B := byinst✝:SetTheoryh:axiom_of_universal_specificationA:SetB:Set⊢ ∃ Z, ∀ (z : Object), z ∈ Z ↔ z ∈ A ∨ z ∈ B
  sorryAll goals completed! 🐙

Вправа 3.2.1. Дух цієї вправи полягає в тому, щоб встановити ці результати без використання парадоксу Рассела, or the specify operation.

theorem declaration uses 'sorry'SetTheory.Set.specify_exists (h: axiom_of_universal_specification) (A:Set) (P: A → Prop):
    ∃ (Z:Set), ∀ z, z ∈ Z ↔ ∃ h : z ∈ A, P ⟨ z, h ⟩ := byinst✝:SetTheoryh:axiom_of_universal_specificationA:SetP:A.toSubtype → Prop⊢ ∃ Z, ∀ (z : Object), z ∈ Z ↔ ∃ (h : z ∈ A), P ⟨z, h⟩
  sorryAll goals completed! 🐙

Вправа 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the specify operation.

theorem declaration uses 'sorry'SetTheory.Set.replace_exists (h: axiom_of_universal_specification) (A:Set)
  (P: A → Object → Prop) (hP: ∀ x y y', P x y ∧ P x y' → y = y') :
    ∃ (Z:Set), ∀ y, y ∈ Z ↔ ∃ a : A, P a y := byinst✝:SetTheoryh:axiom_of_universal_specificationA:SetP:A.toSubtype → Object → ProphP:∀ (x : A.toSubtype) (y y' : Object), P x y ∧ P x y' → y = y'⊢ ∃ Z, ∀ (y : Object), y ∈ Z ↔ ∃ a, P a y
  sorryAll goals completed! 🐙

Вправа 3.2.2

theorem declaration uses 'sorry'SetTheory.Set.not_mem_self (A:Set) : (A:Object) ∉ A := byinst✝:SetTheoryA:Set⊢ set_to_object A ∉ A sorryAll goals completed! 🐙

Вправа 3.2.2

theorem declaration uses 'sorry'SetTheory.Set.not_mem_mem (A B:Set) : (A:Object) ∉ B ∨ (B:Object) ∉ A := byinst✝:SetTheoryA:SetB:Set⊢ set_to_object A ∉ B ∨ set_to_object B ∉ A sorryAll goals completed! 🐙

Вправа 3.2.3

theorem declaration uses 'sorry'SetTheory.Set.univ_imp (U: Set) (hU: ∀ x, x ∈ U) :
    axiom_of_universal_specification := byinst✝:SetTheoryU:SethU:∀ (x : Object), x ∈ U⊢ axiom_of_universal_specification sorryAll goals completed! 🐙

Вправа 3.2.3

theorem declaration uses 'sorry'SetTheory.Set.no_univ : ¬ ∃ (U:Set), ∀ (x:Object), x ∈ U := byinst✝:SetTheory⊢ ¬∃ U, ∀ (x : Object), x ∈ U sorryAll goals completed! 🐙

end Chapter3