NBG

Stream: maths

[aes_triplex]

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

[Kenny Lau]

take the model of ZFC and translate it to NBG

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

@Mario Carneiro is there an interface structure model_of_ZFC which Set is an instance of?

[Mario Carneiro]

no

[Mario Carneiro]

actually Jesse and Floris probably built such a thing

[Mario Carneiro]

but in set_theory.zfc it's just a bunch of theorems that look like the axioms of ZFC

[aes_triplex]

@Mario Carneiro thanks.
Is there any feature (regarding set theory or axiomatic theories) on which I could eventually work?

[Mario Carneiro]

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

[Mario Carneiro]

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