ZFC

Stream: general

[Yaël Dillies]

set_theory/zfc is never imported (or at least the docs say so) and it does seem like it shouldn't. Should we move it to archive?

[Mario Carneiro]

No? No one has built on it yet but that doesn't mean it's not in scope for mathlib

[Mario Carneiro]

In particular I would expect some relations between it and set_theory.surreal, set_theory.lists (which is about ZFA) and model theory

[Mario Carneiro]

There just aren't too many set theorists working in mathlib, so it doesn't get much traffic

[Yaël Dillies]

Ah okay, good to know

[Violeta Hernández]

Bump just to say I'm glad we didn't move it into archive :stuck_out_tongue:

[Violeta Hernández]

Also, because I wanted to ask @Mario Carneiro a question. What's the philosophy with pSet? I imagine that unlike the analogous pgame, pre-sets are just not very interesting, and so we want to do as little as possible with them.

[Violeta Hernández]

i.e. we build the basic set-theoretic constructions, like unions or powersets, and then use Set for everything else

[Mario Carneiro]

Yes, that sounds correct

[Mario Carneiro]

It's maybe interesting in some type theory sense, but it's not a set theoretic object of interest

[Mario Carneiro]

on the other hand I wouldn't call pgame very interesting for the same reason, so perhaps you have a different perspective. A pSet is just a one player pgame

[Violeta Hernández]

Well, the thing with pgame is that we don't actually have the correct mathematical notion of an unquotiented game, which would be the quotient of pgame by extensionality. And we don't really care a lot about the difference. So we've instead built a lot of API on pgame directly.