# Zulip Chat Archive

## Stream: general

### Topic: constructing Russell's paradox

#### 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: Dec 20 2023 at 11:08 UTC