Russell's paradox

Analysis I, Section 3.2: Russell's paradox

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

This section is mostly optional, though it does make explicit the axiom of foundation which is used in a minor role in an exercise in Section 3.5.

Main constructions and results of this section:

Russell's paradox (ruling out the axiom of universal specification).
The axiom of regularity (foundation) - an axiom designed to avoid Russell's paradox.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

(Add tip here)

namespace Chapter3export SetTheory (Set Object)variable [SetTheory]

Axiom 3.8 (Universal specification)

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
  -- This proof is written to follow the structure of the original text.
  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! 🐙

Axiom 3.9 (Regularity)

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! 🐙

Exercise 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the empty set.

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! 🐙

Exercise 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the singleton set.

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! 🐙

Exercise 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the pair set.

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! 🐙

Exercise 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the union operation.

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! 🐙

Exercise 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.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! 🐙

Exercise 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the replace 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! 🐙

Exercise 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! 🐙

Exercise 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! 🐙

Exercise 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! 🐙

Exercise 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