Zulip Chat Archive

Stream: maths

Topic: Model for ZFC-I in python


view this post on Zulip Kenny Lau (Jun 08 2018 at 19:23):

I built a quite straightforward model for ZFC sans infinity in python: here

view this post on Zulip Kenny Lau (Jun 08 2018 at 19:23):

it's called the hereditarily finite sets

view this post on Zulip Mario Carneiro (Jun 08 2018 at 22:35):

Why in Python? This could be done in lean computably

view this post on Zulip Kenny Lau (Jun 08 2018 at 22:36):

sure

view this post on Zulip Mario Carneiro (Jun 08 2018 at 22:36):

I don't even know what "construct a model in Python" means

view this post on Zulip Mario Carneiro (Jun 08 2018 at 22:37):

since it doesn't have a proof theory

view this post on Zulip Kenny Lau (Jun 08 2018 at 22:37):

well, the natural numbers is the model, I just provided the relevant functions

view this post on Zulip Mario Carneiro (Jun 08 2018 at 22:37):

what is the encoding?

view this post on Zulip 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: May 10 2021 at 07:15 UTC