# Zulip Chat Archive

## Stream: maths

### Topic: ZFC in Lean

#### James Palmer (Jun 27 2020 at 11:39):

Hi guys, where can I find the ZFC axioms in Lean? What is there currently in terms of theorems? I want to spend the better part of this week trying to expand on that and maybe even some metatheory on LEAN :)

#### Johan Commelin (Jun 27 2020 at 11:40):

The metatheory of lean and zfc don't have that much to do with each other, I think

#### Johan Commelin (Jun 27 2020 at 11:40):

But see `src/set_theory/zfc.lean`

#### Johan Commelin (Jun 27 2020 at 11:40):

Note that mathlib doesn't use zfc anywhere.

#### Kenny Lau (Jun 27 2020 at 11:41):

Lean uses dependent type theory

#### Alistair Tucker (Jun 27 2020 at 11:46):

There's this as well https://github.com/flypitch/flypitch/blob/master/src/zfc.lean

#### James Palmer (Jun 27 2020 at 11:50):

Forgive me I meant metatheory as in First order logic/predicate logic metatheory

#### Johan Commelin (Jun 27 2020 at 12:00):

@James Palmer In that case the Flypitch link that Alistair gave is quite important.

#### Johan Commelin (Jun 27 2020 at 12:01):

It would be really interesting to get some of that stuff in mathlib

#### James Palmer (Jun 27 2020 at 12:10):

many thanks

#### James Palmer (Jun 30 2020 at 20:06):

i.e. we couldn't write constant A: set and then go from there? (permitting that we've write open fol before so that we can make sense of the axioms)

#### Mario Carneiro (Jun 30 2020 at 20:10):

what are you trying to accomplish exactly?

#### Mario Carneiro (Jun 30 2020 at 20:12):

There are two main ways to talk about systems like ZFC: as a model, a set `Set`

of sets with a binary operation called elementhood, or as a syntactic theory, where you have a definition of formulas and axioms and can define the set of provable theorems of ZFC. The former is done in `set_theory.zfc`

, and the latter is done in flypitch

#### Mario Carneiro (Jun 30 2020 at 20:14):

Your comment seems to involve elements of both approaches

#### James Palmer (Jun 30 2020 at 20:18):

where do I find these?

#### Mario Carneiro (Jun 30 2020 at 20:18):

#### James Palmer (Jun 30 2020 at 20:18):

I was hoping to look at it with regards to its links to module theory

#### Mario Carneiro (Jun 30 2020 at 20:18):

flypitch was linked above

#### Mario Carneiro (Jun 30 2020 at 20:18):

module theory?

#### James Palmer (Jun 30 2020 at 20:19):

*model theory

#### James Palmer (Jun 30 2020 at 20:19):

forgive me my computer is not having the best time communicating things atm

#### Mario Carneiro (Jun 30 2020 at 20:23):

I don't think the general notion of a model of ZFC is defined, but https://github.com/flypitch/flypitch/blob/master/src/bfol.lean defines a boolean valued model of a FOL extension

#### Jesse Michael Han (Jul 01 2020 at 01:58):

@James Palmer basic model theory is in `flypitch/src/fol.lean`

and `flypitch/src/completeness.lean`

you can see on this branch how the API is used to state the theorem that `Set`

, the canonical model of ZFC in Lean, is formally a model of the ZFC axioms

#### James Palmer (Jul 01 2020 at 09:24):

thanks Jesse, good work on the Continuum Hypothesis project btw!

#### James Palmer (Jul 01 2020 at 09:24):

(deleted)

#### James Palmer (Jul 01 2020 at 09:25):

(deleted)

Last updated: May 11 2021 at 16:22 UTC