New website to find remaining unknown A => B implications

[felixpernegger]

https://felixpernegger.github.io/pibase-data/

It would be cool to find the remaining pairs of properties A,B (or negations) where one can deduce A => B. This site is made to help with that.

Note it is a bit whacky right now but potentially useful?

Most "unknown" implications are false; for those ideally just give a rough sketch of counterexample (see the log to what I mean) if you wanna contribute

[L-Lord-of-Lore]

Should there be a button/procedure for "not provable in/independent of ZFC" and other middle-y things?
Ie, pi base already explains in theorem 67 that the converse (item 260 in the attachment) cannot be proven true or proven false.

[felixpernegger]

Yes I noticed that as well. Sincenwe are more interested in proving implications, one may even just mark these false (ime. we cant prove them in ZFC) but there should be a distinction, yeah

[prabau]

This is nice. But just to set expectations, I am not sure we necessarily want to add to pi-base all possible such implications. The ones we should focus on are the ones deemed "interesting" in some sense, useful for proving non-trivial results or for simplifying other results, or allowing to automatically derive existing explicit traits.
(@StevenClontz may have an opinion here)

[yhx-12243]

Maybe one can add it to the “Advance” panel, next to “@‍danflapjax Pi-Base Tools”, i.e., serve as a auxiliary tool.

Also change the subtitle “@‍danflapjax Pi-Base Tools” to a general one, e.g., “Third-party π-base auxiliary tools”, etc.

[StevenClontz]

I like the idea of sharing links to community tools in the advanced tab

[prabau]

What do you think of the statement I made in #1815 (comment) that we want to be selective about which results we want to add to pi-base?

[Moniker1998]

I've added some contributions. Not sure how many entries you would ideally want per submission so I kept it to around 10 at one time.
I concur with @L-Lord-of-Lore that it'd be nice to have a buttons for "provable from ZFC" and "not provable from ZFC" (assuming ZFC is consistent).
Also, note pi-base has spaces which axioms depend on more than just ZFC. Such implications we would ideally want to get rid of, I think.

[felixpernegger]

I concur with @L-Lord-of-Lore that it'd be nice to have a buttons for "provable from ZFC" and "not provable from ZFC".
Also, note pi-base has spaces which axioms depend on more than just ZFC. Such implications we would ideally want to get rid of, I think.

Thanks, I forgot about that

[felixpernegger]

sorry i edited your comment accidentally