pi-base
Meta-properties section in Property pages
As we have remarked multiple times in the past, it would be a nice long-term goal if pi-base understood meta-properties of properties (like hereditary, hereditary for closed sets, preserved by finite products, etc, etc.) and was able to derive traits of spaces based on combinations of our current theorems and theorems involving meta-properties.
(See also for example this comment: https://github.com/pi-base/data/issues/1057#issuecomment-2535430024)
At one point, we had discussed the first steps we could take to enhance the pi-base data infrastructure to support some of this meta-information in a more organized fashion, even without the web engine deduction enhancements. But even that seems out of reach at the moment.
So a more modest goal for now could be to allow an optional "Meta-properties" section in Property pages, where it may make sense. I'd say certainly if it is useful in proofs of traits or theorems for now. But of course, it could be expanded a lot beyond that.
For an example, see at the bottom of https://topology.pi-base.org/properties/P000109 (monotonically normal). (I added that section, as I needed to refer to the fact that "monotonically normal" is hereditary, as that was used in a few of the proofs of theorems.) One advantage of such a consolidation is that we can quote a reference proving the meta-property in just one place, and then refer to it multiple times from traits and theorems that use it.
Another example: https://topology.pi-base.org/properties/P000187 (W-space). See the Note at the end.
I'd be curious to see what people think about adding meta-property information in this fashion in general.
Wow it's indeed a great idea I've waiting for a long time (after all, product, subspace, quotient, sum with finite, countably infinite, arbitrary ...), and it'll be a better database for it 👏 But maybe it is a vast project and maybe need many steps (My thought is that, in the later stage, for example, we may have:
- if A + B => C, A hereditary, B hereditary, and automatically C hereditary,
- We can also mark relationship between spaces. Take product as an example, we can mark S31 = S29^2, and auto deduce some property, e.g., KC, is not product-closed,
- e.g. We can mark T5 as hereditary version of T4 and deduce T663 from T661,
Anyway, this is only a very long-term planning and maybe hard to implement, that's totally OK 😀)
A follow-up step which I think is also not too difficult would be to give meta-properties their own files, either just in the directory for that property, or also in a new top level directly parallel to spaces, properties, and theorems if ever that makes sense. Then when adding a meta-property to the description of a property, we add it as a link to that meta-property's file.
The reason for the claim that this is not too difficult is that I'm not presently suggesting any change about the pi-base logic. I'm just foreseeing an issue where some properties may have a lot of relevant meta-properties, and when that happens it may make the property file very long. This could make it unwieldy to include proper references and justifications for the meta-properties of that property.
It remains to be seen if this will be necessary.
Something that seems be reasonably easy to implement on the software side is a simple tagging system. This could be used however the community feels is useful: we can tag spaces that require CH, properties that are hereditary, etc., and then get lists of things that are tagged. Maybe tags can have Markdown justifications, or that info can just go into the description.
@prabau do we think this would be better as a Discussion thread than an Issue? I can't remember if we drew the line somewhere between Issues/Discussions for this particular project.
A follow-up step which I think is also not too difficult would be to give meta-properties their own files, either just in the directory for that property, or also in a new top level directly parallel to spaces, properties, and theorems if ever that makes sense. Then when adding a meta-property to the description of a property, we add it as a link to that meta-property's file.
The reason for the claim that this is not too difficult is that I'm not presently suggesting any change about the pi-base logic. I'm just foreseeing an issue where some properties may have a lot of relevant meta-properties, and when that happens it may make the property file very long. This could make it unwieldy to include proper references and justifications for the meta-properties of that property.
It remains to be seen if this will be necessary.
Actually, your proposal was exactly what we had discussed of doing, with the help of @Not-Abram. But it seems even that may be too much to implement right now? @StevenClontz
@prabau do we think this would be better as a Discussion thread than an Issue? I can't remember if we drew the line somewhere between Issues/Discussions for this particular project.
I initially thought of making this a Discussion. But then thought that Discussions are kind of ignored by most people and it would seem to get more attention as an issue? We can mention this tomorrow maybe, but I don't want to derail the meeting by rehashing this topic, as there are already a lot of other issues that I think should be discussed instead
The main thing is to get people's attention and then discuss how best to move forward. Maybe for the community meeting after the next one?
But then thought that Discussions are kind of ignored by most people and it would seem to get more attention as an issue?
My thought as well - I'm happy with the norm that we don't care too much about Issue vs Discussion distinction for now. And agreed we have more to discuss this Friday, so I'll make a placeholder Jan community call thread with this on the agenda.
Actually, your proposal was exactly what we had discussed of doing, with the help of @Not-Abram. But it seems even that may be too much to implement right now? @StevenClontz
Unfortunately, we kept ourselves busy enough with some smaller tasks - his senior project is also an honors thesis, so we have to move on now to finishing up a survey on research software engineering in mathematics and then start everyone's favorite part of research: writing.
We can also add this whole topic of Meta-properties as another item of discussion for the Jan zoom.
The problem I see is to what extent we should provide proofs to meta-properties
I think if the meta-property is pretty straightforward, there is no need to provide a justification. If it is more involved, ideal would be a reference to something in the literature or to some mathse post.
Recently the concept of "canonical phrasing" for meta properties appears upon adding them. Should we keep somewhere a list of those phrases? Maybe just in some "redundant" file in the repository?
It would also be helpful to see what meta properties are on the table when trying to finally support them by the "engine". We may group them by difficulty of implementation ("hereditary" seem simpler than "preserved by countable disjoint unions"). I have some ideas on data organisation but the format can get complicated if we aim at tracking more types of meta properties.
@StevenClontz oh, I didn't know it existed. I would also like to document properties independent of ZFC there, if possible
I've already created a small list which I was hoping to enlarge
"Default meta property"
I would call hereditary on clopen subspaces a defeult meta property: it seems more natural for a topological property to behave like that than not. Maybe I am wrong, but in this particular case I suggest that negative examples (when the clopen subspace need not to have the property) are more important than the positive.
LOTS is a negative example, since S198 is clopen in S25 $\sqcup$ S2.
I've prepared an extensive description of my thoughts about handling (describing) meta-properties. Available on Dropbox (v1). I got several ideas and they may be not easy to untangle now. But I guess some core is consistent. After all, you may have very different view on our needs (and possibilities). Decided to post it at the current stage, since writing it for too long seems not the thing I should be doing...
Since I'm not familiar with the details of how $\pi$-base deduction system works (and not really want to study it), I focussed on the data format (i.e. what kind of new information we may want to collect). My occasional remarks regarding deduction system may be misguided.
Not to mention there are possibly some different elements we may want to include in the base (e.g. whether some fact is ZFC-independent).