constructing Russell's paradox

Stream: general

[Liang Zhang]

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]

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

[Kevin Buzzard]

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

[Kyle Miller]

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]

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]

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]

@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]

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

[Kyle Miller]

@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]

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]

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