Boolean space machine

[StevenClontz]

Ported from issue #269

http://at.yorku.ca/i/a/a/c/94.htm

It'd be a nice service to the community to make Murray Bell's work accessible again by importing his work into the pi-Base. There's some stuff we cannot model yet (e.g. he has "structure" theorems modeling when properties are retained in e.g. products).

Direct link to ZIP: http://at.yorku.ca/i/a/a/c/94.dir/bell.zip Includes plaintext dat files, HTML, and Perl cgi scripts.

I've created a backup at https://github.com/pi-base/bell-boolean-spaces-machine

[GeoffreySangston]

There's some stuff we cannot model yet (e.g. he has "structure" theorems modeling when properties are retained in e.g. products).

Since you said 'yet', I was wondering if there is a plan to eventually include "structure" theorems? It sounds like a potentially large but exciting change to pi-base, and I've already felt the urge to include "meta-properties". E.g., while working on Contractible it seemed natural to deduce that certain of the product topologies known to pi-base are contractible because the Euclidean line is and because products of contractible spaces are contractible. Also, while writing up the proof of "Closed long ray is simply connected", it seemed natural to want to internally link to the fact that images preserve connected, or compact, or second countable; i.e., in addition to perhaps increasing the scope of the logical deduction engine, "structure theorems" become a third database / community reference within pi-base, adjacent to the databases of spaces and properties.

Not to press the matter, since I assume it would be a foundational change, and therefore take a lot of work. I don't think the idea is in conflict with the normative questions/clarifications you and @prabau have made in the threads I've participated in, but I'm also not sure if it's not. One potential conflict is it could be likely to lead to "redundant theorems", since perhaps a space is a product of connected spaces and is therefore connected, but is also connected for some previously deduced reason (though that depends on your perspective on what "redundant" means).

(I imagine this kind of thing has been thought about about by you all for a while, but I didn't see anything on the ideas page about it other than this.)

[StevenClontz]

I want to support this, but it's just a matter of the lack of time to (a) figure out how to model this, and (b) implement it with the pi-Base software. Hopefully someday!

[prabau]

We had discussed baby steps to start displaying "meta-properties" of properties, for information purpose without associated automated deductions. But even that would take more development resources than currently available. And it's maybe not the highest priority.