ZFC in Mathlib

Stream: new members

[Lucas Teixeira]

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]

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]

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

[Yaël Dillies]

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

[Yaël Dillies]

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

[Kyle Miller]

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]

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.