Strengthen T664 (Monotonically normal ⇒ Shrinking)

[yhx-12243]

Original T664 is now T664 + T543.

Allow to derive that several ω₁ spaces are shrinking.

https://topology.pi-base.org/spaces?q=109+%2B+%3F193

[prabau]

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?

[Moniker1998]

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.

[StevenClontz]

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.

[prabau]

@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.

[yhx-12243]

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.].

[Moniker1998]

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?

[prabau]

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.

[prabau]

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.

[prabau]

@yhx-12243 Just curious, were you able to read the Balogh-Rudin paper?

[Moniker1998]

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

[Moniker1998]

I am currently reading this article by Beogh and Rudin FYI, and will probably approve this PR after.

@prabau if that's okay with you.
I also want to point out MSE will eventually die and so safekeeping posts is not really that worth it

[prabau]

After you convince yourself of the proposed result, it's fine to approve.

What do you mean that MSE will eventually die?
@StevenClontz FYI

[Moniker1998]

@prabau after the traffic will be gone, people who own MSE will probably close it.
And so all the data, except perhaps for the people who downloaded it (and you can do so but apparently, it's made more difficult now with AI). So it won't be perfectly reliable across the years, it will shut down eventually. At least that's what is expected.
So I think it's good to preemptively make some sort of change with our policies in how we always reference MSE?

[prabau]

@Moniker1998 Actually, I reread my comment in #1455 (comment) (especially the last paragraph about T4 => T1) and @yhx-12243 's comment in #1455 (comment) and I still think it's preferable to add the suggested theorem separately and not replace the old one.

As discussed before, we don't lose anything by doing so, and we keep useful information for the old T664.

[prabau]

@yhx-12243 Since this is your PR, and assuming you still agree with your previous comments, can you change things so the the old T664 is kept and we use a new theorem number for this one?

[prabau]

@StevenClontz assuming you are still around (I hope you are), would you mind commenting on this?

[Moniker1998]

@prabau To me it's more important to have a new theorem so that's alright.

As for the article, it's very hard so it'll take me few days.

[prabau]

@yhx-12243 thanks for the additional sentences in T664

[Moniker1998]

So far in the article, I want to comment that in order for the lemma 1.2 to hold, we do need $\mathcal{P}$ to be a cover. The authors don't specify that, but it does need to be true.
Because we need singletons to be in $\mathcal{J}_{u\mathcal{P}}$ and it won't be true otherwise. (singletons are always GO-ordinals)
Thankfully it seems that in the article it always is a cover.

[felixpernegger]

I am currently reading this article by Beogh and Rudin FYI, and will probably approve this PR after.

@prabau if that's okay with you. I also want to point out MSE will eventually die and so safekeeping posts is not really that worth it

I would be seriously surprised if MSE closes before pibase. Also internet archive does not seem to shut down anytime soon

[felixpernegger]

@yhx-12243 I looked over all traits and how they relate to LOTS. And as far as I can tell this one of only two remaining implications of "LOTS => ..." we are still missing and pibase and would be an important step to completing all LOTS (which isnt so far fetched anymore), so it would be great if you could finish the requested changes by the other commenters so we can merge this. :)

[Moniker1998]

@felixpernegger The changes were done I believe, and I'm still reviewing the article by Beogh and Rudin. It will probably take me few more days (currently stuck at lemma 1.6). I'm sorry but I want to be throughout

[felixpernegger]

Ok my bad sorry

[Moniker1998]

As for lemma 1.6 I really couldn't make the original proof work, but if you change $\rho(q)\leq \rho(q_m)$ to $\rho(p) < \rho(q_m)$ then everything works out.