## 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

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: May 10 2021 at 07:15 UTC