pi-base
Guidelines when cleaning up traits
What should the guidelines be when cleaning up traits for a space?
On the one hand, it is logically pleasing to have a minimal set of asserted traits. It also reduces clutter in the list of the asserted traits for a space. And it has also become easier for us to detect redundant traits, as pi-base conveniently gives an indication by displaying the alternate derivation if the trait were not asserted.
On the other hand, some traits that have a simple justification can be derived from other traits in a much more complicated way.
For an instructive example, see #1334 or #1337. P22 (pseudocompact) is true for the irrational numbers with an immediate justification (https://topology.pi-base.org/spaces/S000028/properties/P000022). Looking at the S28-cleanup branch from #1337, the same property has an automated full derivation using 13 theorems, some of which are highly non-trivial. Or the fact that the irrationals have cardinality of the continuum (P65) can be derived in 24 steps.
So what should be the pi-base guidelines when cleaning up traits for pi-base? Do we go for deep cleaning or shallow cleaning?
Anyone involved in pi-base, please share your opinion. (pinging @StevenClontz @ccaruvana if you don't have automatic notification)
I don't see a problem in some properties going through complicated theorems.
Sometimes an intermediary implication $A\implies B\implies C$ is a non-trivial theorem while $A\implies C$ is quite trivial, too.
Moreover it's a matter of bias whatever or not some properties should stay and some should leave, I'm not a fan of this because it's quite subjective, a matter of taste.
I think we should either strive for a minimal set of properties from which all other are derived, or strive for explicit proofs for any property and don't delete the proofs at all. That way we're grounded in specific rules towards what to do.
Some traits have an obvious justification (e.g., the irrationals are pseudocompact), understandable by anyone who knows the definitions. But replacing this with a long derivation involving non-trivial results would make it much more involved if one needed to follow every step. In this particular case, one would have to know about selection principles, Cech complete, realcompact among other things. This would make it out of reach to people who have not studied these things. In particular, it would be inaccessible to an undergraduate audience,
Now as you say, some intermediary implications $A\implies B\implies C$ can often be bypassed if $A\implies C$ is simple. So the problem is often not as bad as it seems. But some essential steps in the derivation could be difficult.
Personally, I don't want to see a direct proof for every single thing. But I have no problem in having some simple derivations in some cases. It's a matter of judgment which ones we want to have. We should discuss more about what would be deciding factors, even if it's not clear cut.
Looking forward to hear more opinions, pro or con.
One thing that we discussed in previous community (zoom) meetings and would help is to enhance what is displayed when a trait is redundant.
(1) On the trait page itself (e.g, https://topology.pi-base.org/spaces/S000028/properties/P000022) it currently shows the written justification and below that it gives a list of theorems that could be used in a derivation. But it's not always clear how that derivation would work. I think it would be more useful to have this second part show something closer to what it would display if we did not have the written justification at the top. Namely, list the necessary asserted other traits, and then the theorems used.
(2) In the list of properties for a space, in particular when displaying the list of asserted traits, give some kind of indication that some traits are derivable. Maybe a change of color or some other indication to be decided.
In that way, one could quickly know which traits are not derivable from others and are more essential for that space. I think that would help.
"Obvious", "understandable", "simple", "not as bad", "difficult" Those are all subjective things, on which we all will disagree on. If you want consistency then we need specific rules being put down. I've proposed two systems of rules that immediately jump out to me. If you want to insist on keeping "simple" theorems then please give specific criteria on what constitutes as "simple" etc., or at least sketch on what such rules could be.
Without rules all of our judgements are arbitrary.
At some point I believed that we should never have redundancies in the database. Each assertion is a liability (possible error) and responsibility (maintanance).
But, I do like having our automated deductions being simpler, and allowing some redundant assertions results in this. So, I think it is acceptable for us as a community to exercise subjective editorial judgement on when a result is "immediate" from the definitions, and allow such redundant assertions.
I've closed my recent cleanup PR's, I will not participate in cleanups in the future if no rules or guidelines for them will be made Subjective editorial judgement to me means no guidelines, we figure things out on the fly.
There are certain criteria we could apply, such as the minimal amount of deductions needed to deduce certain property. If its more than a certain threshold we don't remove a property.
But I don't think it would solve what you want. You are concerned with the psychological, societal and ideological aspect. I see it as an inner conflict with what pi-base is supposed to be, place for researchers and topology enthusiasts, or place for undergraduates. As such I don't see any rules being established in the future.
I think the proposal to clearly indicate (by a different color or ...) in the list of properties which ones are redundant, even if they are given a justification, would help. So if we are interested to know what would be a minimal set of properties, we can just ignore the colored ones. And if someone wants an easy proof of those, they can see it right there, together with a derivation from the other properties (given that we enhance that in the web interface). That seems a good compromise.
At the same time, I totally agree that which ones to include is subjective. That is not ideal. But again if they are easily ignorable, it seems acceptable to me. Personally I don't want to push for adding more easy proofs of redundant properties, and I still want to remove redundant properties in many cases. It's just that in some immediate cases like the cardinality of the reals or of the irrationals, having only the automated derivation seemed excessive.
@yhx-12243 I'd be curious to hear your opinion on this topic.
Anyway I have no special comment on this [^1], however I'm tend to give the tolerance of the redundancy, if they're easy to proof directly.
After all pi-base is instructive for humans, not a completely formal tool (also it may serve for that purpose, uh?), otherwise why don't you use mathlib/etc😆
[^1]: I'll neither agree nor disagree for those PR/discussions that excise traits or even add traits. While, for me, I'll keep it minimize when I try to add a new space.
Thanks @yhx-12243 for the feedback. You make a good point that compared with purely formal tools, one of the benefits of pi-base is that it is much more accessible and usable for humans.
So some redundancy is maybe acceptable sometimes. The suggestion I made further above to visually indicate when this happens would be useful so one could more easily ignore those redundancies at a glance. Because I also think there is a benefit to see what can be deduced from a minimal set of conditions.
The original PR #1334 that triggered this whole discussion is special, as it concerns the real numbers $\mathbb R$, which play a special role in the definition of many properties. For now we have left some redundancies like $\mathbb R$ is metrizable, or it has cardinality continuum, or it is not pseudocompact. Eliminating some of those would be a false savings. For example one can derive that it is metrizable by using theorems that imply it is embeddable in some Euclidean space, and hence metrizable. That's completely circular! Same for some of the other ones. That's why I was reluctant to remove those.
But for the record, after having done some space cleanups recently, I see the benefit of minimal sets of hypotheses, and I have tried to get to minimal sets.
FYI @StevenClontz @Moniker1998