Conversation
|
For example, P114 is now entirely resolved except for two spaces (by adding T1000). Previously, this was the most unknown trait (for 114 spaces) |
| required(trait, 'property', error) | ||
| required(trait, 'value', error) | ||
| required(trait, 'description', error) | ||
| // description is optional for traits |
There was a problem hiding this comment.
so this fixes the issue if I understand correctly?
There was a problem hiding this comment.
What I means is, currently the CI/CD of pi-base already has other errors.
(Because currently pi-base/data is at a invalid state, but CI/CD still builds)
There was a problem hiding this comment.
Relatedly, the fact that CI/CD builds at all for the undecidable-data branch is amazing, considering it has values that the current pi base compiler considers invalid. So if you go to the pi base website and load unprovable-data, it just ignores Felix's changes that it considers invalid, but otherwise works normally.
There was a problem hiding this comment.
One possible reason is that pi-base CI/CD use a docker that is not up to date.
There was a problem hiding this comment.
For example, I can confirm that the change of #171 is not applied at all, because description in pi-base now is not trimmed.
| @@ -1,5 +1,5 @@ | |||
| <script lang="ts"> | |||
| export let value: boolean | undefined | |||
| export let value: boolean | 'undecidable' | undefined | |||
There was a problem hiding this comment.
Probably should be TruthValue | undefined
There was a problem hiding this comment.
This component is used as two functionalities, so if we want to match the semantic, one should even write boolean | TruthValue | undefined (for whether manual and whether truth)
| <Icons.User /> | ||
| {:else if value === false} | ||
| <Icons.Robot /> | ||
| {:else if value === 'undecidable'} |
There was a problem hiding this comment.
This should never happen and should be an error
| {:else if value === false} | ||
| <Icons.X /> | ||
| {:else if value === 'undecidable'} | ||
| <span title="Undecidable">—</span> |
There was a problem hiding this comment.
Again, this should not produce a span. There needs to be an icon,
Undecidable, in the icons folder, and then we need to write <Icons.Undecidable />.
There was a problem hiding this comment.
yes i left that out intentionally. Maybe the the "not prove" icon from logic is appropriate
| { when, then }: { when: Formula<Property>; then: Formula<Property> }, | ||
| space: Space, | ||
| ): boolean { | ||
| if (F.hasUndecidable(when) || F.hasUndecidable(then)) { |
There was a problem hiding this comment.
Someone should confirm that this means undecidable implications do not ever have counterexamples (that's fine).
| const map = new Map( | ||
| assertedTraits.map(([p, t]) => { | ||
| if (p === property) { | ||
| if (p === property && t.value !== 'undecidable') { |
There was a problem hiding this comment.
I have to look at this more closely
|
Am I mildly annoyed that AI wrote this instantly? Absolutely. But does it work? Yeah...probably, or close enough. But we need to review it extra carefully because we're touching the deduction engine. @felixpernegger This will probably cause horrible messes if you use "undecidable" in the antecedent of a condition. My list of suggested things to try:
|
|
This PR also needs to add code for internal links to support undecidable statements, an icon for the undecidable truth value, and code so that the title of the page displays properly for undecidable theorems. I have most of this written here [DON'T use any of my deduction engine stuff, just my "cosmetic" stuff—the deduction engine stuff is broken] I used a different name, "unprovable", which is less correct. Just change it to undecidable. |
Took at least 2 tries, but yeah. :)
I added this and converse shows no counterexamples found. Undecidable (hopefully) has a lower priority implemented than true/false. Lusin sets are working as they are supposed to. (bc cardinalities are added manually there) |
Does it show an auto derivation of undecidable or not for Luzin? It should not. |
|
wait i make ss |
|
I just edited my previous comment with my own fork that includes some of the missing stuff. It can be mostly copy/pasted over, changing "unprovable" to "undecidable" |
|
What is our AI policy? |
|
|
|
Besides testing the daylight out of Explore and checking that the code does what it should for that, we also should check if the Question Box does what it's supposed to—known undecidable statements are excluded. |
|
I checked this and they are excluded |
Well, good thing we're editing this, then. |
|
Can you send a picture of /spaces/S000147/properties/P000114 ? That sort of thing is what I'm concerned about. |
as I said, "undecidable" most likely has a lower priority implemented
|
|
@felixpernegger No; this is very special. It completely overrides the "undecidable" theorem and so we don't even see a derivation of that undecidability. This is good. A bad implementation could have overridden this but only half way. When I get to testing this (or you can do it)—I will go back to your deleted integer topology, which was automatically derived to have "cardinality aleph 1" as undecidable. Then I will manually add a "cardinality aleph 1 is undecidable" trait to this space. In this case, pi base probably should and will provide a derivation in addition to the manual trait being displayed. |
|
@felixpernegger can I have push access to your fork so i can add some of those missing pieces that I have |
|
The symbol ⊬ may not be the most appropriate in this context; see here. Manually writing it out may be easier, e.g. "Euclidean reals R is Cardinality = aleph1" is logically independent I have code for this |
|
@mathmaster13 did you get invite? |
|
compile time also still suffers a bit i think |
|
Eventually I'm going to remove the "converse" section from any undecidability theorems. They shouldn't have one at this time. |
| if (formula.value === 'undecidable') { | ||
| return | ||
| } | ||
| return this.contradiction(theorem, [...support, property]) |
| switch (formula.kind) { | ||
| case 'atom': | ||
| if (formula.value === 'undecidable') { | ||
| throw new Error('Cannot negate an undecidable atom') |
There was a problem hiding this comment.
I don't think anything else in the deduction engine throws errors...changing this may be a good idea? then again there are things that should never happen and this is one of them.
|
The "may not compile" commit is to remind us and/or actually implement the idea that these things should not have converses. They're actually very delicate. They should be interpreted as "if X is provably true then Y is indepndent", rather than "if X is true then Y is independent". So it's not that a space having cardinality aleph 1 implies cardinality = c is independent—it's the fact that we KNOW it has cardinality aleph 1 that makes the independence logically follow. So using implication is a little imprecise but that is possible to change with a minor tweak. Independence can wreak a lot of havoc: if you're working with a space that's not in ZFC, you may end up with a scenario where X is provably true, but Y is not independent of the theory you're in (e.g. the two Luzin sets). In the worst case (which we don't have as a problem now but which could very conceivably become one), Y is not known to be independent of the theory in question, but we also don't know its truth value. Then we need "unknown" to override "independent!". A possible, though not ideal, solution is to just have a flag for spaces not in ZFC which disables any derived independence results from appearing. That way we can manually add them later, rather than having to manually check whether all those independence results are correct. It's tedious either way, and maybe we could disable certain theorems but not others—but I'd rather be certainly correct and less complete than have a vector for incorrect information. I'm sure everyone agrees there. Also, I think with the explore page we can, in the future, entertain an option to negate "undecidable". I don't think the Formula.ts currently allows ~Uhausdorff (where U is the weird undecidable symbol that we need to change), which is good. That means we can't write "not undecidable" in explore and cause core to throw an error. |
|
What is the difference between "provably true" and "true"? In dependent type rhepry and I think also first order logic this ought to be the same thing (see Gödel completeness theorem). |
|
You make a lot of good point, but in general I think "Perfect is the enemy of the good" can be applied here: See my comment above, but what is the difference between "true" and "provably true"? Yes adding an undecidable value could potentially mark spaces where the value of certain traits is decidable, but how often does this actually occur? Whenever adding a theorem with undecidable, its not hard to check to just check those two spaces, especially since there are mostly completed anyways. Yes, when adding additonal spaces with extra axioms this could become a bigger problem, but is this really happening? I doubt we'd have many theorems except (versions of) CH for undecidable. A more simpler solution to flagging theorems (which may complicate the entire website quite a bit) would be to just write a warning in the wiki and/or in every space with additional axioms that "undecidable" values may not hold. Converse of a theorem with undecidable is actually not a vig problem I think. Say PA + PB => U(ndeciable) PC The negation of undecidable would be decidable, so either true or false. But are there actually cases (besides computational stuff) in math where we know something is decidable but not if its true or false? Personally, I'd be fine with just excluding undecidavle from explore at all. I doubt anyone would seriously use this. |
|
In any case, if you are okay with it, I think it might be a good idea to schedule a "community call" (those existed in the past, before I contributed so idk) to discuss this, since adding "undecidable" is undoubtebly a big (but good) change. If yes, I write a message on zulip |
@prabau I think you participated in those in the past, would this be something appropriate? |
|
This is definitely a good topic to discuss. We used to have zoom meetings. @StevenClontz should be probably be involved here. |
|
Did not read the long comments above. But some background info regarding Luzin spaces: In the past, we decided that we would allow set theoretic assumptions beyond ZFC when defining spaces. But we would not allow such assumptions in theorems, as it would create too many problems (theorems are supposed to apply uniformly to all spaces). Just FYI for background. What is this theorem 1000 that you used? |
I am also fine with excluding undecidable from explore. I think we basically want a "minimum viable product" right now, and all that is would be allowing us to mark things as undecidable and ideally allowing us to automate stuff like CH. I agree the perfect is the enemy of the good. However, I don't think writing "undecidable values may not hold" is great. We should not write anything that will automatically populate a database entry if that automatically filled data is possibly wrong. Yes, only two spaces use non-ZFC axioms. But maybe we add more—what do I know? I've certainly seen issues for spaces on the first measurable cardinal. In any case, it is better to have some missing information when everything in the database is correct, rather than have even a small risk that some extra information in that isn't really true gets put in by an automation. Also, I wasn't thinking of flagging theorems so much as flagging spaces—saying "hey, this is not a ZFC construction, don't apply any undecidability stuff here because it could just be wrong". I'd have to see what performance hit it'd take, but I get your point now. Given Patrick's comment on "theorems should be universally applicable", I think this warrants further discussion. The difference between true and provably true: every statement is either true or false, but it may not be possible for us to know which one. The negation of undecidable would be "true or false". The point I'm making is that this negation means provably true or provably false—because every statement is either true or false, even the undecidable ones. So "X is true or false" would not be a tautology in our system, but equivalent to "X is decidable", which is a subtle thing. Because I also don't want the perfect to be the enemy of the good, I was trying to avoid thinking about these subtleties entirely. I'm not a logician :) |
Well said |
|
@prabau T1000 is a very temporary ID for one side of the continuum hypothesis: cardinality = c "implies" cardinality = aleph1 is undecidable where "implies" has quotes because I am not a logician. This is half of saying "CH is undecidable". The other half would be "cardinality = aleph1 -> cardinality = c undecidable" |
I dont this this is really the case. Law of excluded middle says (p or not p) but both p and not p can be consistent with your language (see CH or for something more advanced Stone Cech conpactification of integers) |
|
P and not P can both be consistent but (obviously) you can't have P and not P as axioms at the same time and have a consistent system. I don't know what you were referring to when you said "I don't think this is really the case". Sorry about that. |
Not that it matters at all here, but I think this is not possible to properly state in first order logic (what people usually think about) but very much so in higher order logic |
|
Also, T1000 is in the |
@prabau Having undecidability not break this rule (though it would break it in a very controlled manner) is going to be interesting. Ex: CH. We want to not have to manually put in the following fact: if we know that a space has cardinality c, then it is undecidable if it has cardinality aleph1 or not. We would be manually doing that on basically every space. Let's assume we are using a theorem for that, like Felix's T1000. The two Luzin sets, then, would break this rule. In the current pi base, we have their cardinality as both c and aleph1, because you need CH to construct them in the first place. If we were to say that it was "undecidable in ZFC" if the Luzin sets had cardinality aleph 1 or not, we'd be at best saying something useless, because we used cardinality aleph 1 to even construct them. Hence I suggested we should allow spaces with extra axioms besides ZFC to opt out of automated undecidability results, or at least allow for us to override those automated undecidability results. That way, the two Luzin sets can still affirmatively have cardinality c and aleph1 at the same time. But that means that some theorems (i.e. these automated undecidability results) would not be applied uniformly to all spaces. But it's very predictable how that works and arguably needed for correctness. But instead of flagging non-ZFC spaces, we could just have an actual database property (say P999) "Object can be shown to exist in ZFC alone" and have all the undecidability theorems use that as an assumption. This keeps the theorems nice and uniform and keeps correctness intact, because we're encoding whether a space is in pure ZFC or not using a property rather than a flag. There are issues here: the property is not exactly a property of the space "object can be shown to exist in ZFC", but rather a property of the database entry "this pi-base entry assumes only ZFC". And a property has its own drawbacks: properties have to be set manually or derived, and this property likely couldn't be derived. I have to admit the property approach would probably simplify the implementation, if we can formalize it correctly. But none of this matters until we decide what our goals are here. |
4 participants
Disclaimer: This PR was entirely made by Claude code!!! (I checked the output but not the code)
This is a rudimentary attempt at adding a third truth value "undecidable" to pibase.
This was discussed many times: There are traits which cannot be (dis-)proven in ZFC, most notably traits related to the Continuum hypothesis.
To test this, in the branch "undecidable-data" of pibase data repo, I added T1000 (essentially the CH) and S147|P64 (just to test). The system appears to be working.
"undecidable" (hopefully) has a lower priority than true/false which is important for spaces assuming additonal axioms (S147 and S148).
Right now "undecidable" (again hopefully) does not deal with contraposes. One would have to think about what is the right approach. (Since there are not so many theorems about undecidability, adding all versions might just be ok in my opnion).