Reduce ax-13 usage by adding dv conditions #3781
Conversation
|
I am not quite convinced of tagging the former versions of theorems as ALT here. Our https://us.metamath.org/mpeuni/conventions.html page wants this suffix for shorter/clearer proofs of the same theorem, at the expense of axiom usage. But here the theorems change considerably by having extra dv conditions. What particularly hurts, is that the usage of the more general ALT version is now discouraged. Why? I am very much in favor of using a *w or *v suffix instead. |
The point is to avoid doing exactly that. The direct usage of these theorems in ax-13-complete shows that it would mean minimizing more than 100 theorems. So instead, with this PR I do basically same thing but faster and with less amount of changes.
I was thinking that instead of keeping original versions as ALT, maybe we could add a different suffix to them, that way we wouldn't be forced to add discouraged tags (the verifiers fail if you don't add them where an ALT suffix is present). Is there an appropriate suffix for the inverse of Then as I mentioned in the description of this PR, perhaps not every theorem in the above list deserves it's own permanent copy, some of the less used original versions could simply be reported as OLD instead. |
|
|
What do you mean by that? I'm not intending to fool any verifier. Perhaps I didn't explain it well.
The thing is, either you add *w versions and minimize hundreds of theorems, or as suggested by @tirix in #3773 (review) you make the weaker versions the default. In that discussion it was originally proposed to keep the original versions as OLD. Then I was asked to keep them as ALT instead #3773 (comment), this is what lead us to the point we are right now. So, to address your concerns my new proposal is to keep the original ones with a different suffix instead of ALT, which would represent the inverse meaning of the *w suffix, and maybe keep bnj1441 and nfiund as OLD, since they are never used anyway. This way I am happy because I avoid a significant minimization activity and you are happy because non-conventional ALT versions are not generated. Does this sound good to you? |
|
Yes |
What suffix would you suggest for "Stronger version of ~ xxx without a dv condition"? |
|
We use the suffix g for more general theorems occasionally. What still nags me a bit is that we do not follow our habits (so far) of providing the general theorem before the specialized one. Is that minimizing process you speak of a one-time shot that once done will not occur further? Or is it a repeating event, that will disturb development again and again? In the latter case we should find a means of circumventing it. Just a few ideas that sprang to my mind. |
|
What is the problem with suffixing a |
|
This isn't a one time occurrence, this happened before when I added an extra DV to cbvabv and cbvrabv |
|
First of all (I didn't mentioned before) this PR drops ax-13 from 106 theorems. Full axiom usage of the changes (last commit included) can be consulted here abc5821. I pushed a new commit renaming *ALT versions as *g versions, the approach I used goes as follows:
Note that *g versions are not needed in principle, they are only used between each other. The only reason I'm keeping them is because I've been asked to do so to show how it looks without additional dvs. For future proofs, the new versions should be preferred. I believe the *g versions could actually have a "new usage is discouraged" tag, because you wouldn't want to repropagate ax-13 in a future ax-13 free database. As I mentioned before, it would take a lot more than one PR to achieve the same result with the *w versions, because we would have to shift hundreds of proofs. Note that adding dv as I did here is not always applicable. In fact, most of the time we have to follow the long approach anyway, because usually dv conditions propagate too much. But when the advantage is clear, such as in this PR, I think we should take the opportunity to get the highest results, while making less changes as possible. |
|
... |
This is reasonable. We can think about it later in a different phase. For now there is still a lot of work to be done. |
|
The goal is accepted, but lofty: Removing ax-13 from theorems on a large scale. It seems that the correct (i.e. according to our established rules) transformation is difficult, either in general, or for @GinoGiotto. So the question is whether we can be generous for the moment, and in a final step rename all affected theorems to our standards again. That way we have some progress, and in the end we get both: the reduced axiom usage, and labels that please the majority of us. Of course, we must not allow the same procedure for any odd small scale improvement, but perhaps this is big enough in size to make an exception. |
Yes. Treating them independently would be fine for me (I would still fear merge conflicts regarding cbvmptv, which is directly used by more than 400 theorems, but at least it's an issue that can be handled without hurry).
Correct. This makes sense for theorems (or to be more precise theorem chains) which are used a lot. Prioritizing these first in a simple manner is not only more practical but also faster in achieving the expected results. |
|
About relabelling: for me it's fine, but it should be documented in changes-set.txt. Example: |
|
Please update changes-set.txt so that the merge conflicts are resolved. If no one objects, I will merge this PR afterwards. |
|
No problem for me to merge, I already approved. My understanding is that this project will ultimately allow to remove ax-13 from the whole of Then from my point of view, the theorems without ax-13 become "the new normal" and their names should not need to be longer than today. I encouraged that direction, sorry I did not also push for an open discussion on the mailing list first! In any case that's a laudable goal and I think one everyone agrees on. I also think Norm would definitely have agreed on. @GinoGiotto you have all my support! |
Actually Norm mentioned in this thread:
My interpretation is that he would be a proponent of replacing the current version of the theorems with the version without ax-13. |
I used a similar approach to #3778 to remove ax-13 dependencies from the theorems mentioned below. Most of these were in the list of proofs that I would have added as *w version, but in this case it's possible (and more convenient) to just add dv conditions directly to them.
I added ALT versions for each item of the list. The main reason is that the variables involved were present in the final statements, but perhaps there are theorems where ALT versions wouldn't be really necessary, for example for bnj1441 and nfiund, which have no current usage.
Since lemma hbsb is part of the ax-13 section, we can't add dv conditions directly to it to reduce that dependency, therefore hbsbw is moved to main from my mathbox. Theorem nfabdw is moved to main to be used by nfiund, but it will be used more later.
Current usage of the edited theorems:
To make things more clear, I provide the chain shapes of these theorems:
nfabdw → nfiund ↑ nfrexd → nfrex → nfiun ↑ * hbsbw → hbab → nfsab → nfab → nfaba1 ↓ ↓ ↓ hblem bnj1441 nfiin * cbviun → cbviunv * cbviin → cbviinvThis PR contains 3 independent chains. The first one has the purpose to drop ax-13 from nfrex and nfab, which are the most used ones in their chain. The other two are meant to drop ax-13 from cbviunv and cbviinv.
The theorems in the chain used directly or indirectly by nfab don't really have high usage. An alternative approach could be to move nfsabw to main with a longer proof, although we would loose the (relavitely small) contributions of hbsbw, hbab, nfsab, hblem for reducing ax-13 usage (their recursive usage is around a few dozens of theorems if we cut off nfab from the chain).