Zulip Chat Archive

Stream: maths

Topic: NBG


view this post on Zulip aes_triplex (Apr 20 2020 at 09:37):

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

view this post on Zulip Kenny Lau (Apr 20 2020 at 10:16):

take the model of ZFC and translate it to NBG

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 20 2020 at 10:23):

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

view this post on Zulip Mario Carneiro (Apr 20 2020 at 10:24):

no

view this post on Zulip Mario Carneiro (Apr 20 2020 at 10:24):

actually Jesse and Floris probably built such a thing

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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