Парадок Рассела

Аналіз I, Розділ 3.2: Парадокс Рассела

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

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

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

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

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

Підказки від попередніх користувачів

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

(Додайте підказку тут)

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:Chapter3.Object → Prop := 
  fun x =>
    ∃ X,
      x =
          @DFunLike.coe (Chapter3.Set ↪ Chapter3.Object) Chapter3.Set (fun x => Chapter3.Object)
            Function.instFunLikeEmbedding Chapter3.SetTheory.set_to_object X ∧
        x ∉ X⊢ False
  choose Ω hΩ using h Pinst✝:SetTheoryh:axiom_of_universal_specificationP:Chapter3.Object → Prop := 
  fun x =>
    ∃ X,
      x =
          @DFunLike.coe (Chapter3.Set ↪ Chapter3.Object) Chapter3.Set (fun x => Chapter3.Object)
            Function.instFunLikeEmbedding Chapter3.SetTheory.set_to_object X ∧
        x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P x⊢ False
  by_cases h: (Ω:Object) ∈ Ωpos._@._hyg.157inst✝:SetTheoryh✝:axiom_of_universal_specificationP:Chapter3.Object → Prop := 
  fun x =>
    ∃ X,
      x =
          @DFunLike.coe (Chapter3.Set ↪ Chapter3.Object) Chapter3.Set (fun x => Chapter3.Object)
            Function.instFunLikeEmbedding Chapter3.SetTheory.set_to_object X ∧
        x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P xh:SetTheory.set_to_object Ω ∈ Ω⊢ Falseneg._@._hyg.157inst✝:SetTheoryh✝:axiom_of_universal_specificationP:Chapter3.Object → Prop := 
  fun x =>
    ∃ X,
      x =
          @DFunLike.coe (Chapter3.Set ↪ Chapter3.Object) Chapter3.Set (fun x => Chapter3.Object)
            Function.instFunLikeEmbedding Chapter3.SetTheory.set_to_object X ∧
        x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P xh:SetTheory.set_to_object Ω ∉ Ω⊢ False
  .pos._@._hyg.157inst✝:SetTheoryh✝:axiom_of_universal_specificationP:Chapter3.Object → Prop := 
  fun x =>
    ∃ X,
      x =
          @DFunLike.coe (Chapter3.Set ↪ Chapter3.Object) Chapter3.Set (fun x => Chapter3.Object)
            Function.instFunLikeEmbedding Chapter3.SetTheory.set_to_object X ∧
        x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P xh:SetTheory.set_to_object Ω ∈ Ω⊢ False have : P (Ω:Object) := (hΩ _).mp hpos._@._hyg.157inst✝:SetTheoryh✝:axiom_of_universal_specificationP:Chapter3.Object → Prop := 
  fun x =>
    ∃ X,
      x =
          @DFunLike.coe (Chapter3.Set ↪ Chapter3.Object) Chapter3.Set (fun x => Chapter3.Object)
            Function.instFunLikeEmbedding Chapter3.SetTheory.set_to_object X ∧
        x ∉ XΩ:SethΩ:∀ (x : Object), x ∈ Ω ↔ P xh:SetTheory.set_to_object Ω ∈ Ωthis:@_fvar.270
  (@DFunLike.coe (Chapter3.Set ↪ Chapter3.Object) Chapter3.Set (fun x => Chapter3.Object) Function.instFunLikeEmbedding
    Chapter3.SetTheory.set_to_object _fvar.327) := 
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ False
    obtain ⟨ Ω', ⟨ hΩ1, hΩ2⟩ ⟩ := thispos.intro.intro._@._hyg.157inst✝:SetTheoryh✝:axiom_of_universal_specificationP:Chapter3.Object → Prop := 
  fun x =>
    ∃ X,
      x =
          @DFunLike.coe (Chapter3.Set ↪ Chapter3.Object) Chapter3.Set (fun x => Chapter3.Object)
            Function.instFunLikeEmbedding Chapter3.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.intro._@._hyg.157inst✝:SetTheoryh✝:axiom_of_universal_specificationP:Chapter3.Object → Prop := 
  fun x =>
    ∃ X,
      x =
          @DFunLike.coe (Chapter3.Set ↪ Chapter3.Object) Chapter3.Set (fun x => Chapter3.Object)
            Function.instFunLikeEmbedding Chapter3.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.intro._@._hyg.157inst✝:SetTheoryh✝:axiom_of_universal_specificationP:Chapter3.Object → Prop := 
  fun x =>
    ∃ X,
      x =
          @DFunLike.coe (Chapter3.Set ↪ Chapter3.Object) Chapter3.Set (fun x => Chapter3.Object)
            Function.instFunLikeEmbedding Chapter3.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! 🐙
  rw [←hΩ] at thisneg._@._hyg.157inst✝:SetTheoryh✝:axiom_of_universal_specificationP:Chapter3.Object → Prop := 
  fun x =>
    ∃ X,
      x =
          @DFunLike.coe (Chapter3.Set ↪ Chapter3.Object) Chapter3.Set (fun x => Chapter3.Object)
            Function.instFunLikeEmbedding Chapter3.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
  choose x h h' using regularity_axiom A (nonempty_def h)inst✝: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
  aesopAll 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. Суть вправи полягає в тому, щоб встановити ці результати, не використовуючи ані парадокс Рассела, ані операцію заміни.

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_iff : axiom_of_universal_specification ↔
  ∃ (U:Set), ∀ x, x ∈ U := byinst✝:SetTheory⊢ axiom_of_universal_specification ↔ ∃ U, ∀ (x : Object), x ∈ U 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