Logical Independence

[mathmaster13]

Update: A draft PR is slowly piecing itself together. We have a "starter" generated by some AI that works fairly well, and we need to
edit it (which also means understanding exactly what it does and correcting its errors) and add any missing features we want. It won't become a ready PR until all of it is understood and corrected by a human. If a person who is experienced with core helps finish the draft, it'll get done much faster. We are making some changes in viewer to support this—those are super simple—but also changes to core and compile to 1) allow independence results in deduction and data 2) limit how they can be used by contributors to data and/or the deduction engine to ensure correctness.

Also, anybody else see pi base not displaying any names for anything? No space names or property names ever. Thanks @felixpernegger

I know in the super long term there's been at least a remark on Zulip about possibly overhauling to Lean. So maybe this isn't necessary/helpful.

But I've been thinking that it should not be that hard to implement a third logical value besides true or false. This can be the "provably independent" value (the "unknown" value would still exist, of course). Currently I got the compiler to recognize a third value and am working on getting deduction to work properly. I probably will try and implement it just for fun, though if there is significant optimization that's needed I might struggle to do that. I can't make promises, but it seems fun.

Is there any desire for/recommendations when playing around with this? My primary motivation is to stop the continuum hypothesis from raiding the question box, though it's also just a good feature in my opinion.

The hard part is that the engine seems to prove everything by negating it and getting a contradiction (is that right?). So what may be easiest is to have the independence deductions separate from the regular deduction engine in some way, where independence can be influenced by logical deductions but cannot be used for any further deductions. So pi-base can deduce a statement is independent but cannot deduce anything else from that fact. For simplicity (for now) it cannot even affect the explore page, only occurring if you ask for a specific trait on a specific space.

A related feature, which would be somewhat necessary, would be the ability to override independence values. For example, pi base has Luzin sets which require CH to construct. Thus pi base correctly has their cardinality as both c and aleph1. If we had a theorem "cardinality c implies cardinality aleph1 is independent", then we'd need to basically turn that theorem off for the Luzin sets, which live in ZFC+CH. This is easy if independence checking is somewhat separate from deduction: we just say "whatever deduction (including manual input) says goes; we won't even check for independence unless deduction gives us nothing".

To check independence, we have a few theorems A -> (B is independent) and we just try and prove A. If nothing pops up, we say we don't have enough information.

[felixpernegger]

Also, anybody else see pi base not displaying any names for anything? No space names or property names ever.

No, I recommend you clear browser cookies.

[felixpernegger]

@mathmaster13 #235

[mathmaster13]

We should note that there are subtleties to the meaning of a statement like "X implies Y is independent". Really I don't know if it's an actual "implication" in the sense of logic, but it says that if we can prove X is true (in ZFC) then Y is independent (of ZFC). Note that the "contrapositive" of this (if that even makes sense) would be "if Y is not logically independent of ZFC, then X cannot be proven true in ZFC" which is not the same as saying that X is false.

I think the move right now is to try and make these logical details matter as little as humanly possible, and banning the use of "undecidable" on the left side of an implication would hopefully do that. Hence also separating the "undecidable" system from the deduction system proper—that way we (hopefully) don't need to think about it unless we're working with it specifically.

[mathmaster13]

Stuff gets even weirder when you consider stuff like this StackExchange post. That surely won't bite us someday, right?

[mathmaster13]

The most important things from the Zulip note we should add:

P114 implies P58 independent
P114 implies P65 independent
P65 implies P114 independent

and others

Note that P58 (i.e. being able to prove P58) does not necessarily imply that P114 is independent. In fact, the only way you can get a proof of P58, for any space X, is if X is countable!

Besides that, there are a few cases where P72 is potentially independent. Those probably will be added manually.

[mathmaster13]

I mentioned this in a comment, but correctness is very important to pi-base, and so we want to make it hard to screw that up. I think instead of manually overriding individual independence results, we should just have a flag axioms-beyond-zfc in the markdown file format (which is false by default and does not need to be specified if it's false) that tells the viewer to just turn off all independence results for this space and force them to be either added manually or overridden. This ensures that whenever we have extra axioms, we never will accidentally assert the independence of a statement that may not actually be independent in the theory we are working with. Side note: I named the flag the way I did to make it clear that it is, as of the current pi-base, impossible to not assume the ZFC axioms. For example, a space or trait that exists in ZF+negation of choice, but doesn't exist in ZFC, is impossible to talk about in pi-base, and this feature will not change that.

This shouldn't be too bad, given what we have now. But if you use AI to help you implement it, review your own code—we already have a bit to review. (Note that I don't mean "review" in the PR approval sense—we are drafting a PR using AI-generated code that we are checking for correctness and making changes to. It won't be marked as a ready-for-review PR until all the code is edited and understood by humans. This likely will take a while.)