Analysis
3.2. Russell's paradox

Imports

import Mathlib.Tactic
import Analysis.Section_3_1

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:Object → Prop := fun x ↦ ∃ X, x = SetTheory.set_to_object X ∧ x ∉ X⊢ False
  choose Ω hΩ using h Pinst✝: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⟩ ⟩ := thisposinst✝: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Ω1posinst✝: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Ω2posinst✝: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! 🐙
  rw [←hΩ] at 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! 🐙

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 (no set contains itself)

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 (no two sets contain each other)

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 (universal specification)

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 (there is no universal set)

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