pi-base
Strengthen T664 (Monotonically normal ⇒ Shrinking)
Original T664 is now T664 + T543.
Allow to derive that several ω₁ spaces are shrinking.
https://topology.pi-base.org/spaces?q=109+%2B+%3F193
Three theorems:
- old T664: Monotonically normal => countably paracompact
- new T664: Monotonically normal => shrinking
- T543: Shrinking => countably paracompact
The old T664 was not an easy result, but it was still accessible, especially with the mathse reference that fixed minor things and explained the result in detail.
But the new T664 from the paper of Balogh & Rudin is really at a higher level of complexity. It's definitely an important result to add. But replacing the old T664 with this one will make the old result more inaccessible for most people, I am afraid. And it would be regrettable to lose the reference for the proof of the old T664.
I don't have a good recommendation here. @StevenClontz @ccaruvana and others: any ideas about this general concern?
I prefer what's true over what's easy
But I think we should make sure that the result is true first. Did @yhx-12243 @prabau any one of you read this result beforehand?
I am not completely trusting of peer review literature, even though it's correct most of the time
How I use pi-base is to check what results are true. And this I think should be the top priority of this site. Both theorems and examples of spaces serve this purpose. The moment we start sacrificing what are the best results, for what's simple to others, I think that will make me stop being interested in this project.
We can try to explain things in simple ways to others, but that shouldn't make us sacrifice the complexity of them, I think that would be absurd.
I prefer what's true over what's easy
I agree, but as much as possible I want my cake and to eat it too.
As I talk with other math database maintainers, the more strongly I feel that I don't want to change existing theorems (even as strict improvements), because we don't have a great way to identify theorems other than their Txxxxxx ID. So I think that, even though our software isn't great at knowing when to use P->R vs. P->Q + Q->R, I'd rather keep the "easy"/"direct" T664, and then add two new theorems, even though they deprecate T664 in terms of automated deduction.
@Moniker1998 Personally I agree with pretty much everything you are saying.
We spend a lot of effort trying to make pi-base as reliable as possible, with precise definitions and statements (which is sometimes lacking in the literature). I think that is one of the great strengths of pi-base.
In this particular instance, I have not read the Balogh-Rudin article, just skimmed it to see it is involved. I was not going to approve this without taking a closer look, or hopefully someone else can check it without taking things on faith.
As far as sacrificing the best results, I am not sure what you mean. I think the proposed result is a great result to add (assuming it is correct of course, but given the caliber of the authors, it's most probably the case). And I am not advocating to replace its proof with something easier to digest for people, which would make no sense here.
But at the same time, I think in this case Steven's suggestion to preserve the old T664 is a good one as it provides valuable and more accessible information to prove P=>R. If we replace it with a very difficult P=>Q plus an existing Q=>R, the overall P=>R becomes less accessible to most people interested in seeing why P=>R. Having both P=>R and P=>Q a little redundant, but it does not hurt anything as far as the deduction system is concerned.
And note that we have other examples of such redundancies. For example, there it theorem T4 => T1. And there is also a long chain of intermediate properties joining T4 to T1. The redundancy in this case has also the advantage that some generated deductions are shorter and more manageable.
I understand that (original) T664 is special case because it contains a (mathse) reference to explain more detailed, rather than a simple reference to some article. So removing it will cause a “resource inaccessibility” (e.g., for that mathse post). So it indeed has a reason to keep it.
In other way, if the theorem itself is just an article link (and the theorem itself not very simple [as T106, as your last paragraph said], e.g., like new T664 itself, it's a complex proposition with only a “pointer” to an article), I think it's better directly replace it.
Generally, I think a redundant theorem can be keeped if [either]:
- It contains resources/informations more than the assertion itself [Old T664].
- It's more easy to understand it rather than complex deduction chain [T98, T106, etc.].
As far as sacrificing the best results, I am not sure what you mean. I think the proposed result is a great result to add (assuming it is correct of course, but given the caliber of the authors, it's most probably the case). And I am not advocating to replace its proof with something easier to digest for people, which would make no sense here.
@prabau alright, it sounded like you meant something different.
Now I am thinking, all of these results here are about very specialized class of properties, so should we really be safekeeping such theorem?
Generally, I think a redundant theorem can be keeped if [either]:
- It contains resources/informations more than the assertion itself [Old T664].
- It's more easy to understand it rather than complex deduction chain [T98, T106, etc.].
Makes sense to me.
Now I am thinking, all of these results here are about very specialized class of properties, so should we really be safekeeping such theorem?
Not sure what is meant by "safekeeping". But I see no reason to avoid these specialized results. If they are correct, they are highly non-trivial and interesting.
Not sure what is meant by "safekeeping". But I see no reason to avoid these specialized results. If they are correct, they are highly non-trivial and interesting.
That Monotonically normal => countably paracompact, which is probably in the article of Rudin, in Handbook of set-theoretic topology, about countably paracompact spaces