# Zulip Chat Archive

## Stream: new members

### Topic: ZFC in Mathlib

#### Lucas Teixeira (Oct 27 2021 at 07:43):

Mathlib defines ZFC sets in these 4 steps:

- Define pre-sets inductively.
- Define extensional equivalence on pre-sets and give it a setoid instance.
- Define ZFC sets by quotienting pre-sets by extensional equivalence.
- Define classes as sets of ZFC sets. Then the rest is usual set theory.

https://leanprover-community.github.io/mathlib_docs/set_theory/zfc.html

I'm curious to the motivation behind this, and why it isn't sufficient to just use the regular `set`

and then define all the axioms as constants

#### Kevin Buzzard (Oct 27 2021 at 07:48):

`S : set X`

means "S is a subset of X" and there's no X such that every set is a subset of it.

#### Kevin Buzzard (Oct 27 2021 at 07:50):

and mathlib doesn't have any axioms, so I doubt that an exception would be made for this.

#### Yaël Dillies (Oct 27 2021 at 07:55):

The point is to construct a model of ZFC, not to define it axiomatically.

#### Yaël Dillies (Oct 27 2021 at 07:55):

I wrote that docstring, but Mario would be a better person to ask about.

#### Kyle Miller (Oct 27 2021 at 07:56):

This also proves that Lean is at least as powerful as ZFC, and we can trust that this ZFC is consistent assuming that Lean/mathlib without any additional axioms is consistent.

#### Kevin Buzzard (Oct 27 2021 at 07:57):

My understanding is that Mario's thesis also proves the converse -- that ZFC is strong enough to model all the constructions which Lean's dependent type theory is capable of, giving an equiconsistency result.

Last updated: Dec 20 2023 at 11:08 UTC