Buggy ?property formula

[StevenClontz]

https://topology.pi-base.org/spaces?q=LOTS%2BPerfectly+normal%2B%3FFirst+Countable

See converation at pi-base/data#1041

[prabau]

This is a case where a search with a formula containing "?P" returns "... is impossible" and displays a single theorem.

Every time I have seen this happen, if one replaces "?P" with either "P" or "~P", it gives a sequence of theorems proving that one of the situations is impossible. In this case, "~P" is impossible. And therefore any space satisfying the other conditions will automatically satisfy "P". And so the P trait can never be "unknown".

But I agree that the output is confusing and could be changed.

Furthermore, compare:

(1) π-Base, Search for LOTS + Perfectly normal + ?First Countable

displays the single theorem T183.

(2) π-Base, Search for LOTS + Perfectly normal + ~First Countable

displays a series of theorems to prove impossibility, but not T183 among them.

My guess is that it's because there may be multiple ways to show some combination is impossible. And as it happens, the deduction of impossibility for

(3) π-Base, Search for LOTS+Perfectly normal+~Fréchet Urysohn

is just 7 theorems. In combination with T183, that would give a total of 8 theorems, shorter than the non-optimal derivation for (2). So internally, when pi-base figured out the impossibility of (1), it found a proof of it using T183 and returned that.

[yhx-12243]

This is because of the buggy logic that don't check null in theorem deduction, it will be fixed by #206.

web/packages/core/src/Formula.ts

Line 146 in e3004a6

return traits.get(f.property) === f.value

traits.get(f.property) can be null.

[prabau]

This is not resolved at all. It is now worse than before.

See #206 (comment).