ZFC intersection

Stream: general

[Violeta Hernández]

I've been thinking about the intersection of a ZFC docs#Set. In contrast to the usual docs#set.sInter, we can't just define sInter Ø = univ, since there's no such thing as a universal ZFC set. I don't think it's desirable to have sInter return a Class, either.

[Violeta Hernández]

We could of course just case on whether the input set is empty, and return some default value if it is, but I think this would lose computability - is that something we care about here?

[Violeta Hernández]

Alternatively, we could have sInter take in an explicit member s of the set t, so that it could be defined as {x ∈ s | ∀ y ∈ t, x ∈ y}. This of course has the annoyance that different choices of this member don't lead to definitionally equal sets.

[Mario Carneiro]

Violeta Hernández said:

We could of course just case on whether the input set is empty, and return some default value if it is, but I think this would lose computability - is that something we care about here?

No, we don't care about computability here

[Mario Carneiro]

Although, I suspect that you don't actually need noncomputability to write this definition

[Mario Carneiro]

ZFC sets are generally "trivially computable" in the same way that proofs are