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