Sets as predicates vs ZFC

Stream: Analysis I

[Dan Abramov]

When I looked a the powerset definition in Mathlib itself, I was surprised to find it was just

/-- `𝒫 s` is the set of all subsets of `s`. -/
def powerset (s : Set α) : Set (Set α) := {t | t ⊆ s}

Given how much attention we pay to construct things "from the ground up" without using universal specification in the book, "eh, it's just a set of all subsets" in Mathlib confused me.

I then remembered that in Mathlib, Sets are literally just predicates. And it does make sense that type theory protects us from the Russell's paradox. So I guess it's not really "universal" specification — we're only selecting from the Set (Set α) type — and presumably somehow that construction can be shown to satisfy the ZFC axioms.

Is there a good intuitive way to think about why type theory makes it "okay" to think about Sets as predicates? And how to bridge that with the axioms we use in the book? I know there's the 3.x epilogue which sets up the mapping but I get lost reading that.

[Kenny Lau]

The mental translation that one should make is:

Type theory | Set theory
========================
Type        | Set
Set         | Subset

i.e. when you see the word Set in Lean, just say "subset" in your head --

with this translation, it becomes obvious that Set (Set α) is allowed, because in ZFC P(P(A)) is also allowed.

Recall also that in ZFC you are allowed to form any (definable) subset of a set, with the axiom schema of specification.

[Dan Abramov]

Ok that seems insightful.

So in Lean, the type theory takes care of building the hierarchy "upwards" that we can select from, and then the actual Set is like a way to "specify" a smaller thing from that already "prebuilt" hierarchy.

And I guess we can think of the "specifying predicate" we pass to Lean Set as being 1:1 with the ZFC subsets of that type? Because a function to true/false is 1:1 with powerset elements?

[Kenny Lau]

yes, i mean, this is also "literally true" in mathlib's standard model of ZFC

[Dan Abramov]

Thanks for explaining, kind of obvious in retrospect but I had difficulty with it.

[Kenny Lau]

@Dan Abramov here's the lean proof:

import Mathlib

universe u

open ZFSet

def set_ (x : ZFSet.{u}) : Set x ≃ x.powerset where
  toFun s := ⟨x.sep fun y ↦ ∃ h : y ∈ x, Subtype.mk y h ∈ s, by
    simp_rw [mem_powerset, subset_def, mem_sep]; tauto⟩
  invFun s := { y : x | y.1 ∈ s.1 }
  left_inv s := by simp
  right_inv s := by
    obtain ⟨s, hs⟩ := s
    rw [mem_powerset] at hs
    ext y
    simpa using @hs y

[Kenny Lau]

(and please don't PR this to mathlib)