pi-base
Non-triviality conditions in theorems
@danflapjax @StevenClontz Sorry I did not have the chance to comment. But I don't think this change is an improvement.
I agree it is in general preferable to use "true" properties in theorems. However that does not apply to "non-triviality conditions", i.e., conditions meant to exclude trivial uninteresting boundary cases from the discussion. Things like "non empty" or "not indiscrete", etc. Non-triviality conditions are often expressed as the negation of some property.
In this case, what we want to express is that R1 spaces are not hyperconnected. And that holds mostly true, except in the trivial case that the space has the indiscrete topology. So we say instead: If the space is R1 and we are not in a trivial condition, then the space is not hyperconnected.
But the new change turns this into: if the space is both R1 and hyperconnected, then we are in a trivial condition. That is of course logically equivalent. But the previous formulation is more natural, as that's the common one that is used when applying this to particular spaces, to determine if a space is hyperconnected or not.
Originally posted by @prabau in https://github.com/pi-base/data/issues/738#issuecomment-2327281261
Does this need to be discussed at another Zoom meeting? What was the consensus at the previous one?
T109 is similar to the new version of T262 suggested by @danflapjax, so if some reversion were to be made (not that I have an opinion either way) then I think these should be changed together.
I'm not certain I understand the Issue, but I think it suggests that "non-triviality conditions" should not be positive conclusions of theorems. No theorem has Empty as a conclusion at present, though a few do have Indiscrete as a conclusion, as can be seen on the Indiscrete page. Are any other properties "non-triviality conditions"?
Our conclusion was that the underlying dispute (that is, the differing aesthetic preferences) would be better ameliorated by enhancements to the user interface than any style policy. As it stands, the site will only display proof or counterexamples of one converse of a theorem, but we should at least allow visitors to switch which property is treated as the consequence for this analysis.
Agreed; I don't think we'll find a "right" way to do this for every scenario, so I think it's up to the opinion of the contributor and reviewer what makes sense in a given context, and eventually we can provide tooling as @danflapjax suggests to switch the consequence.
And given this discussion we had, I suppose this can be closed, but note the issue I made at pi-base/web to implement this UI change someday.
Our conclusion was that the underlying dispute (that is, the differing aesthetic preferences) would be better ameliorated by enhancements to the user interface than any style policy. As it stands, the site will only display proof or counterexamples of one converse of a theorem, but we should at least allow visitors to switch which property is treated as the consequence for this analysis.
@danflapjax @GeoffreySangston @StevenClontz
I agree that better tooling will let users explore different equivalent formulations of a theorem.
But the discussion was not simply about aesthetic preferences. I still think it's more important to display a version of the theorem that is most likely to be useful to a user applying it to some situation. And that is done by having the non-triviality condition as a hypothesis, and not by moving it to a triviality condition in the conclusion. (By moving that condition to a triviality condition in the conclusion, we will indeed have an equivalence between the hypotheses and the conclusion. But who cares? That's not an important thing at all.)
No offense, but that is literally an aesthetic preference about how to present a theorem. My preference differs. That's all this is about, even if the two versions would communicate the information differently.
For what it's worth, to expound on my contrary stance a little, since it appears I only did so over Zoom: I tend to think of properties like indiscrete or discrete not as trivial but as strong. That is, they say a lot about a space, so I think having one as the consequence of a theorem is actually quite valuable, just the same as saying a space is, say, a manifold. I could discuss this much further, but I think it's of little value, since it has no impact on the actual mathematical content. If anything, I think trivial changes like the one I made in the PR that sparked this issue should be avoided regardless, simply because it is not worth the fuss.
I sat here for a full five minutes trying to decide how to diplomatically respond to both of you, who I believe both make good points. And then I decided that we all have higher-impact things to do on this repository, so I'm moving on. (-: