Zulip Chat Archive
Stream: maths
Topic: Model for ZFC-I in python
Kenny Lau (Jun 08 2018 at 19:23):
I built a quite straightforward model for ZFC sans infinity in python: here
Kenny Lau (Jun 08 2018 at 19:23):
it's called the hereditarily finite sets
Mario Carneiro (Jun 08 2018 at 22:35):
Why in Python? This could be done in lean computably
Kenny Lau (Jun 08 2018 at 22:36):
sure
Mario Carneiro (Jun 08 2018 at 22:36):
I don't even know what "construct a model in Python" means
Mario Carneiro (Jun 08 2018 at 22:37):
since it doesn't have a proof theory
Kenny Lau (Jun 08 2018 at 22:37):
well, the natural numbers is the model, I just provided the relevant functions
Mario Carneiro (Jun 08 2018 at 22:37):
what is the encoding?
Mario Carneiro (Jun 08 2018 at 22:39):
actually, there is an instance of denumerable (finset N) that you could use for the elementhood predicate in lean
Last updated: Dec 20 2023 at 11:08 UTC