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