Ostaszewski space

[hpecora1]

Was just doing some absentminded exploring and noticed that hereditarily separable does not show up as a property. An obvious example of a space to add here would be A.J. Ostaszewski's example. Good follow-up to this might be Fedorcuk's space from one of the papers in this MO post: https://mathoverflow.net/questions/440984/how-to-construct-large-hereditarily-separable-compact-spaces.

[StevenClontz]

Hereditarily separable is a good property to add. Any examples need to be constructable in ZFC - we don't have infrastructure to say things only work assuming diamond or anything like that.

[prabau]

https://dantopology.wordpress.com/tag/hereditarily-separable/ has useful info about "hereditary separable". A related notion is a space of "countable spread" (see first article in the link above). Do we have this in pi-base?

[hpecora1]

Ok that makes sense. Well at least hereditarily separable then and maybe another example. Of course, second countable separables work, but I bet the pi-base will immediately prove that. Since S-spaces are independent, maybe Justin Moore's ZFC L-space as a nice addition for hereditarily Lindelof.

It looks like no version of spread or cellularity is in pi-base already, and since hS and hL both imply countable spread it seems a natural thing to add.

[prabau]

For cellularity there is https://topology.pi-base.org/properties/P000029.

[hpecora1]

Oh perfect well that accounts for countable spread then.

[GeoffreySangston]

Just going through open issues. I'll try to summarize the status of this one. The quick assessment is, based on new comments below, items 2, 3, and 5 are still unresolved.

1. Hereditarily separable was suggested in OP, and it does exist in pi-base today P180. So this suggestion has been resolved.
2. Ostaszewski's space was suggested in OP. I don't know what this is, but based on page 175 of Encyclopedia of General Topology, its construction depends on the diamond principle. So @StevenClontz's comment https://github.com/pi-base/data/issues/312#issuecomment-1536827352 means it will not be added in the near future. Hence this suggestion should, unfortunately but necessarily, be disregarded for now. (Nevermind, see below.)
3. Fedorcuk's space's was suggested in OP. I also don't know what this is. Based on page 171 of Encyclopedia of General Topology, its construction depends on the continuum hypothesis, so is independent of ZFC, and @StevenClontz's comment means it also must be presently disregarded, unfortunately. (Nevermind, see below.)
4. @prabau suggested countable spread in https://github.com/pi-base/data/issues/312#issuecomment-1536906506. This property exists in pi-base today P000197. So this suggestion has been resolved.
5. @hpecora1 suggested Justin Moore's ZFC L-space in https://github.com/pi-base/data/issues/312#issuecomment-1537173685. I also don't know what this is, but I assume it is from Justin Moore's paper with a relevant sounding title. This space does not appear to have been added to pi-base yet.
6. @hpecora1 suggested a "version of spread or cellularity" in https://github.com/pi-base/data/issues/312#issuecomment-1537173685. As noted, 'has countable spread' exists in pi-base. I don't understand the comment about cellularity or prabau's response, but it seems to have been resolved?

[prabau]

For 2. and 3., we may want to ask @StevenClontz for his current opinion, which may have changed since.

[StevenClontz]

I believe we have some spaces that require CH to construct already. I see no reason to ban examples that require $\diamond$. My only concern is internal consistency of the database, but I don't think we have problems adding spaces that require additional axioms beyond ZFC.

[prabau]

And to complement this: As far as theorems are concerned, those cannot make any assumption beyond ZFC. Right?

[GeoffreySangston]

@prabau @StevenClontz I'll modify the conclusion of the comment.

[StevenClontz]

And to complement this: As far as theorems are concerned, those cannot make any assumption beyond ZFC. Right?

Both that, and traits as well. I remember the day in graduate school when we learned about V=L and everyone in the class said "wait that makes perfect sense, let's just assume that always" lol. But plenty of mathematicians don't want to make such strong assumptions; we shouldn't confound our database with results that are only true in such models. I think it would take a very thoughtful refactor of our software to support results modulo different models of ZFC, but I don't see any issues by having spaces that are constructed in incompatible models.

[prabau]

Not sure I follow for traits.

Traits for the particular space making the special set-theoretic assumption can/should rely on that assumption for their proof, right?