# Zulip Chat Archive

## Stream: maths

### Topic: NBG

#### aes_triplex (Apr 20 2020 at 09:37):

Hi Everybody,

I'm developing the NBG set theory in Lean, just for fun. Any suggestions?

#### Kenny Lau (Apr 20 2020 at 10:16):

take the model of ZFC and translate it to NBG

#### Mario Carneiro (Apr 20 2020 at 10:17):

because lean has higher order quantifiers, the model of ZFC is also a model of NBG, even MK set theory

#### Kenny Lau (Apr 20 2020 at 10:22):

to be clear, I'm talking about https://leanprover-community.github.io/mathlib_docs/set_theory/zfc.html#Set

#### Kenny Lau (Apr 20 2020 at 10:23):

@Mario Carneiro is there an interface `structure model_of_ZFC`

which `Set`

is an instance of?

#### Mario Carneiro (Apr 20 2020 at 10:24):

no

#### Mario Carneiro (Apr 20 2020 at 10:24):

actually Jesse and Floris probably built such a thing

#### Mario Carneiro (Apr 20 2020 at 10:24):

but in `set_theory.zfc`

it's just a bunch of theorems that look like the axioms of ZFC

#### aes_triplex (Apr 20 2020 at 12:13):

@Mario Carneiro thanks.

Is there any feature (regarding set theory or axiomatic theories) on which I could eventually work?

#### Mario Carneiro (Apr 20 2020 at 12:15):

generally speaking, it is easier to work with models than with axiomatic theories described via a deeply embedded formal language

#### Mario Carneiro (Apr 20 2020 at 12:15):

But if you want to go the FOL route, you should check out https://github.com/flypitch/flypitch/

Last updated: May 18 2021 at 08:14 UTC