Permutation Models

Stream: Is there code for X?

[Brian Pinsky]

I'm a set theorist with essentially no background on lean. I do work on permutation models, which are models of set theory with atoms. Atoms/urelements can be elements of sets, but have no elements themselves. To keep atoms from being equal to the empty set, extensionality must be weakened to only talk about non-atoms. These are useful to show the independence of AC from the rest of ZF set thoery.

It doesn't look like the existing code for ZFC models is well equipped to talk about permutation models; or for that mater any interesting model of set theory not produced by just cutting the universe off at an inaccessible (like L).

Is implementing these a reasonable first project, or are there some major difficulties I don't see yet?

[Yaël Dillies]

Have you heard about the Con(NF) project? This is in essence constructing a big permutation model.

[Brian Pinsky]

I had not. This does look interesting, although there is a sizable amount of mathematics I would need to learn before helping on this (ZFA models are much closer to classical set theory).

[Esteban Castillo Vargas]

Brian Pinsky said:

I'm a set theorist with essentially no background on lean. I do work on permutation models, which are models of set theory with atoms. Atoms/urelements can be elements of sets, but have no elements themselves. To keep atoms from being equal to the empty set, extensionality must be weakened to only talk about non-atoms. These are useful to show the independence of AC from the rest of ZF set thoery.

It doesn't look like the existing code for ZFC models is well equipped to talk about permutation models; or for that mater any interesting model of set theory not produced by just cutting the universe off at an inaccessible (like L).

Is implementing these a reasonable first project, or are there some major difficulties I don't see yet?

Have you done any progress implementing such models in Lean?