Reorganization of cardinalities to be <, =, or <= (and fix the beth numbers)

[StevenClontz]

I don't have time to write this issue up now, but I'm posting this placeholder to remind me to get back to this.

[StevenClontz]

As brought up in #96 there are some issues related to how cardinality is represented on the pi-base. Here are how they appear now:

• https://topology.pi-base.org/properties/P000125 "has distinct points", >= 2
• https://topology.pi-base.org/properties/P000078 "finite", < omega
• https://topology.pi-base.org/properties/P000057 "countable", <= omega
• https://topology.pi-base.org/properties/P000058 < 2^omega
• https://topology.pi-base.org/properties/P000065 2^omega
• https://topology.pi-base.org/properties/P000059 <= 2^(2^omega)

These were either chosen based on Counterexamples to match the reference chart, or added over time. I propose we reorganize as follows.

• Keep >=2 (while this is not consistent with how I've organized the rest of the proposal, this is how the property is most frequently used and based on recent discussion trivial spaces #14 we should keep it this way)
• All other carnality properties moving forward should be equivalent to <kappa for some cardinal kappa. Since this is a ZFC database, we will carefully use aleph and beth numbers. Note that our canonical name doesn't be exactly <kappa ("finite" is better than "<beth0") but the property should be equivalent to <kappa.
  • finite is equivalent to <beth0=aleph0
  • countable is equivalent to <aleph1
  • <2^omega is equivalent to <beth1
  • 2^omega is equivalent to <beth2 and not <beth1
  • <=2^(2^omega) is equivalent to <beth3

So most of what I propose is some possible renaming or modification of descriptions, except for handling P65 (=beth1). We should certainly add a <beth2 property, and theorems connecting it to P65 and P58 (<beth1). Whether we need to dig through the entire database to purge P65 is up for discussion: we have redundancies elsewhere (e.g. listing T_3 for regular+T_0), and I think keeping this one =beth1 property is possibly useful for historical reasons.

[prabau]

I think we should also mention that P59's current name is (<= 2^omega), and that does not match (<= 2^(2^omega)).

[prabau]

I think keeping P65 (beth1) is kind of useful because it can be asserted for many examples that have an obvious cardinality of the continuum, and from that we can automatically derive the fact that many other cardinality properties are true or false. It simplifies the management of the data in many cases, I think.

[prabau]

One comment about that last two bullets in your list. "2^omega is equivalent to <beth2 and not <beth1" and "<=2^(2^omega) is equivalent to <beth3". That would be the case if GCH holds, but otherwise there could be many cardinals strictly between two consecutive beths, so they don't seem to be equivalent. It does not seem to be the case that one can express cases of equality or <= in terms of < of beth numbers. I guess one can always say: <= beth3 is the same as <(beth3)+, where the + indicates the successor cardinal, and =beth1 is the same as [not(<beth1) and <(beth1)+ ], but that does not seem too useful.

[StevenClontz]

Oh yeah, that was a silly oversight from me. Yes, beth_(n+1)=(beth_n)+ fails in many models of ZFC, so some of my beth_(n+1)s should be (beth_n)+ (but really it's easier to just say <=beth_n than <(beth_n)+, which is what we should do).

[prabau]

Hi @StevenClontz . Would it be possible for you to fix just the title for https://topology.pi-base.org/properties/P000059 ("smaller or same as the continuum", but seemingly meant to be something else)?

After that, there are many many examples that have the cardinality of the continuum by construction. That's why I really think we should keep P65. It allows to claim the correct cardinality in an obvious fashion for these spaces, and then the other cardinality properties can be deduced appropriately. That will allow to remove a lot of redundant traits files, which is what I had started doing in PR #96. I can work on that, independently of any further tweaking of cardinality properties that you have in mind. Would you be ok with that approach?

[StevenClontz]

I opened a PR for @lyengulalp or @ccaruvana to approve to make the necessary fix to the title of P59; will review the rest of this comment when I can.

[prabau]

Hi. Quoting below from my Nov 6 comment. Would you be ok with this for now?

After that, there are many many examples that have the cardinality of the continuum by construction. That's why I really think we should keep P65. It allows to claim the correct cardinality in an obvious fashion for these spaces, and then the other cardinality properties can be deduced appropriately. That will allow to remove a lot of redundant traits files, which is what I had started doing in PR #96. I can work on that, independently of any further tweaking of cardinality properties that you have in mind. Would you be ok with that approach?

[StevenClontz]

Responding to this is way-overdue, but I think I want this refactor done programmatically rather than by hand. So unless it's blocking something critical, let's keep this on the back-burner.

[StevenClontz]

In today's meeting we decided it was reasonable to fix cardinality >=3 and >=4 to be <=2 and <=3 and flip the booleans.

We decided to make the exception for "has multiple points (cardinality >=2)"

[prabau]

One thing that came up in the review for #561.

We have a "convenience property" P65 (card = c), which could be expressed as (card <= c and not < c) but is really convenient for data entry in particular. Similarly, to express that a space is countably infinite, we currently must say (countable + not finite). But I think it would be really convenient to add a property (card = $\aleph_0$).

[marswill]

I hate to throw a monkey wrench into something we already decided on in the meeting, but it has dawned on me that for finite cardinalities, it is probably literally always going to be the case that a theorem requires cardinality at least $n$, rather than at most $n$. There is really little point in making theorems about all spaces of cardinality at most $n$, since there are only finitely many of them, and I doubt the premises of any of our theorems will ever* include $|X|\leq n$.

[*Edit: I guess I should have actually looked at our theorems, I see we have one or two like this, though arguably those could have just been asserted traits on the relevant spaces. I think broadly speaking the point stands.]

So we might reconsider that change, and have instead a convention that finite cardinal properties all have the form $|X|\geq n$ (we could even flip the bits on "Empty" to "Nonempty" to conform to this, which would make a lot of sense in my view, as there are almost never theorems that require "empty" as a hypothesis.)

So our rule could be:

• finite cardinal properties always equate to $|X|\geq n$.
• infinite cardinals have the form $|X| &lt;\kappa$ (which includes $|X|\leq \kappa$ as has been pointed out). Note the finite rule is just a negation of this rule, so we still have some governing logical principle here.
• As @prabau suggests, convenience properties for equality of extremely common infinite cardinalities, probably just $|X|=\mathfrak c$ and $|X|=\aleph_0$, though I think we currently have $|X|=\aleph_1$, so maybe that stays if we feel generous enough.

In practice, I think this just means leaving everything the way it is except for

• changing P137 from empty to nonempty and flipping the bits on asserted traits and theorems.
• adding $|X|=\aleph_0$.
• possibly removing P114 ($|X|=\aleph_1$), and adding $|X|\leq \aleph_1$, or alternatively leaving the convenience property and just adding $|X|\leq \aleph_1$. Or doing nothing at the moment since we may not have a use for $|X|\leq \aleph_1$, in which case we simply add it if we ever need it.

[prabau]

I am ok with most of what you are proposing. Except for the elimination of the convenience $|X|=\aleph_1$ and of $|X|\leq \kappa$ for infinite cardinals. We have various theorems with a conclusion of that form, which seems more "convenient" than $|X|\lt\kappa^+$ in my opinion (what is $\mathfrak c^+$ or $(2^{\mathfrak c})^+$ anyway, it's neither well determined in the aleph scale nor on the beth scale for example). We should give this some thought.

[marswill]

I am ok with most of what you are proposing. Except for the elimination of the convenience |X|=ℵ1 and of |X|≤κ for infinite cardinals. We have various theorems with a conclusion of that form, which seems more "convenient" than |X|<κ+ in my opinion (what is c+ or (2c)+ anyway, it's neither well determined in the aleph scale nor on the beth scale for example). We should give this some thought.

I maybe mis-explained. $|X|\leq \kappa$ properties would not be eliminated - they are equivalent to $|X|&lt;\kappa^+$. As @StevenClontz mentioned earlier the actual name isn't important as long as it is equivalent to $|X|&lt;\kappa$ for a cardinal $\kappa$.

As for $\mathfrak c^+$ (or even $\mathfrak c$ itself) not being well-determined on $\aleph$ scale, I don't think that's a problem. We need only include those ZFC theorems that relate it to other cardinals in the database. Which is what we currently do.

I mostly agree with, or at least am neutral towards, keeping the convenient $\aleph_1$, was just keeping its elimination as a possibility in case others thought that we should limit the number of "convenience cardinals."

[StevenClontz]

I have slight unhappiness with "not nonempty" being the phrasing for "empty" on pi-Base. I wouldn't block a PR from someone who really wants that to happen, but I'm going to skip that suggestion for now.

Otherwise I'm cool with having contrary conventions for finite vs infinite cardinals.