## Stream: general

#### Liang Zhang (Jul 11 2021 at 19:33):

I thought it was impossible to construct Russell's paradox in lean, until I found that this works

#check {x | x ∉ x} ∈ { x | x ∉ x}  -- prints "Prop"


What does it mean? Is it really Russell's paradox or something different?

#### Kevin Buzzard (Jul 11 2021 at 19:34):

It means that what you have written is a true-false statement.

#### Kevin Buzzard (Jul 11 2021 at 19:34):

#check 2 + 2 = 4 -- Prop
#check 2 + 2 = 5 -- Prop


#### Kyle Miller (Jul 11 2021 at 19:36):

This is an incomplete expression, too. Take a look at the type of just the first part:

#check {x | x ∉ x}

{x : ?M_1 | x ∉ x} : set ?M_1


That's a metavariable.

#### Kyle Miller (Jul 11 2021 at 19:37):

You can make it complete manually, though:

def foo {α : Type*} [has_mem α α] : set α := {x | x ∉ x}


This isn't Russell's paradox because has_mem instances can do whatever you want -- they have no axioms.

#### Kyle Miller (Jul 11 2021 at 19:48):

Here's a version of Russell's paradox. It says that if you have a has_mem instance that is "set-like" in that every set of α can be represented as a term of α (where the has_mem instance is what lets you go the other way), then you reach a contradiction.

theorem russell {α : Type*} [has_mem α α]
(from_set : set α → α)
(from_set_prop : ∀ (s : set α) (z : α), z ∈ s ↔ z ∈ from_set s) :
false :=
begin
let uhoh : α := from_set {x : α | x ∉ x},
by_cases h : uhoh ∈ uhoh,
{ have h' := (from_set_prop _ _).mpr h,
exact h' h, },
{ apply h,
rw ←from_set_prop,
exact h, },
end


#### Liang Zhang (Jul 11 2021 at 19:48):

@Kevin Buzzard I don't think it a simple false statement. If the statement is false, then it should be true. That's what Russell's paradox is supposed to mean, right?

@Kyle Miller thanks for pointing it out. I'm very new to lean, can you elaborate a little bit on what you mean by "they have no axioms"? Thanks.

#### Liang Zhang (Jul 11 2021 at 19:50):

@Kyle Miller thanks. I'll take a look.

#### Kyle Miller (Jul 11 2021 at 19:52):

@Liang Zhang The notation x ∈ y is defined to be has_mem.mem x y, and this is the definition of has_mem:

class has_mem (α : out_param \$ Type u) (γ : Type v) := (mem : α → γ → Prop)


It is a typeclass that requires nothing but a definition explaining how to decide whether has_mem.mem x y should hold or not. From a certain point of view, it's simply a way to turn y into a set (that may or may not have anything to do with the original y!)

#### Kyle Miller (Jul 11 2021 at 20:06):

For russell, I should point out that it's a notationally complicated way of saying that there's no injection from set α to α. The type set α is defined to be α -> Prop, and since Prop is a two-term type, in other words it's proving that there's no injection $2^\alpha \to \alpha$.

#### Mario Carneiro (Jul 12 2021 at 04:28):

Just to emphasize the importance of the notation meaning what you expect, here's a completely contradiction free proof that "the russell set is a member of itself":

instance foo : has_mem unit unit := ⟨λ _ _, true⟩
instance bar : has_mem (set unit) (set unit) := ⟨λ _ _, true⟩

example : {x | x ∉ x} ∈ {x : unit | x ∉ x} := trivial


Last updated: Aug 03 2023 at 10:10 UTC