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)

@[reducible, inline]

abbrev Chapter3.axiom_of_universal_specification [SetTheory] : Prop

Axiom 3.8 (Universal specification)

Equations

• Chapter3.axiom_of_universal_specification = ∀ (P : Chapter3.Object → Prop), ∃ (A : Chapter3.Set), ∀ (x : Chapter3.Object), x ∈ A ↔ P x

theorem Chapter3.Russells_paradox [SetTheory] : ¬axiom_of_universal_specification

theorem Chapter3.SetTheory.Set.axiom_of_regularity [SetTheory] {A : Set} (h : A ≠ ∅) : ∃ (x : A.toSubtype), ∀ (S : Set), ↑x = set_to_object S → Disjoint S A

Axiom 3.9 (Regularity)

theorem Chapter3.SetTheory.Set.emptyset_exists [SetTheory] (h : axiom_of_universal_specification) : ∃ (X : Set), ∀ (x : Object), x ∉ X

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 Chapter3.SetTheory.Set.singleton_exists [SetTheory] (h : axiom_of_universal_specification) (x : Object) : ∃ (X : Set), ∀ (y : Object), y ∈ X ↔ y = x

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 Chapter3.SetTheory.Set.pair_exists [SetTheory] (h : axiom_of_universal_specification) (x₁ x₂ : Object) : ∃ (X : Set), ∀ (y : Object), y ∈ X ↔ y = x₁ ∨ y = x₂

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 Chapter3.SetTheory.Set.union_exists [SetTheory] (h : axiom_of_universal_specification) (A B : Set) : ∃ (Z : Set), ∀ (z : Object), z ∈ Z ↔ z ∈ A ∨ z ∈ B

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 Chapter3.SetTheory.Set.specify_exists [SetTheory] (h : axiom_of_universal_specification) (A : Set) (P : A.toSubtype → Prop) : ∃ (Z : Set), ∀ (z : Object), z ∈ Z ↔ ∃ (h : z ∈ A), P ⟨z, h⟩

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 Chapter3.SetTheory.Set.replace_exists [SetTheory] (h : axiom_of_universal_specification) (A : Set) (P : A.toSubtype → Object → Prop) (hP : ∀ (x : A.toSubtype) (y y' : Object), P x y ∧ P x y' → y = y') : ∃ (Z : Set), ∀ (y : Object), y ∈ Z ↔ ∃ (a : A.toSubtype), P a y

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 Chapter3.SetTheory.Set.not_mem_self [SetTheory] (A : Set) : set_to_object A ∉ A

Exercise 3.2.2

theorem Chapter3.SetTheory.Set.not_mem_mem [SetTheory] (A B : Set) : set_to_object A ∉ B ∨ set_to_object B ∉ A

Exercise 3.2.2

theorem Chapter3.SetTheory.Set.univ_iff [SetTheory] : axiom_of_universal_specification ↔ ∃ (U : Set), ∀ (x : Object), x ∈ U

Exercise 3.2.3

theorem Chapter3.SetTheory.Set.no_univ [SetTheory] : ¬∃ (U : Set), ∀ (x : Object), x ∈ U

Exercise 3.2.3