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αα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