Reduce ax-13 usage #3905
Reduce ax-13 usage #3905
Conversation
| brabidgaw.1 $e |- R = { <. x , y >. | ph } $. | ||
| $( Version of ~ brabidga with a disjoint variable condition, which does not | ||
| require ~ ax-13 . (Contributed by Gino Giotto, 2-Apr-2024.) $) | ||
| brabidgaw $p |- ( x R y <-> ph ) $= |
There was a problem hiding this comment.
As mentioned in issue #3879 (which was closed recently), I think it is unfair not to mention the original contributor here, because this theorem will become standard, and the original theorem discouraged. Furthermore, the intention/description of the theorem is missing. Therefore, I would propose to change the comment as follows:
$( The law of concretion for a binary relation. Special case of ~ brabga .
Version of ~ brabidga with a disjoint variable condition, which does not
require ~ ax-13 . (Contributed by Peter Mazsa, 24-Nov-2018.)
(Revised by Gino Giotto, 2-Apr-2024.) $)
This remark applies for all similar cases in the following (and previous PRs).
There was a problem hiding this comment.
Done in e749638. As mentioned in the previous PR I think the general case of this proposal would be better addressed on its own issue (along with the ALTV suggention next to it).
As a quick note I should mention that not all versions without ax-13 have been contributed by me. For example, drex1v and drnf1v have been contributed by @benjub as weaker versions of drex1 and drnf1, which have been contibuted by Norman Megill and Mario Carneiro respectively (now discouraged). Therefore, in the case of drnf1v, the "Contributed by BJ" tag would be changed into "Contributed by Mario Carneiro" and "Revised by BJ" tags. Those technical lemmas used to be in BJ mathbox in a dedicated section that he made with the exact purpose of reducing axiom usage. It's not granted that all people that contributed weaker versions would be ok with this credit change (therefore I believe a separate issue should be opened for this).
There was a problem hiding this comment.
And also there is currently an open PR 3fa74c2 for iset.mm with theorems containing my credit contributions, so even those would have to be edited for consistency.
There was a problem hiding this comment.
Done in e749638. As mentioned in the previous PR I think the general case of this proposal would be better addressed on its own issue (along with the ALTV suggention next to it).
As a quick note I should mention that not all versions without ax-13 have been contributed by me. For example, drex1v and drnf1v have been contributed by @benjub as weaker versions of drex1 and drnf1, which have been contibuted by Norman Megill and Mario Carneiro respectively (now discouraged). Therefore, in the case of drnf1v, the "Contributed by BJ" tag would be changed into "Contributed by Mario Carneiro" and "Revised by BJ" tags. Those technical lemmas used to be in BJ mathbox in a dedicated section that he made with the exact purpose of reducing axiom usage. It's not granted that all people that contributed weaker versions would be ok with this credit change (therefore I believe a separate issue should be opened for this).
I would propose to re-open #3879 for this discussion (because it already contains some suggestions/remarks about this topic), or I want to ask you to create a new issue. Opinions of @benjub and @digama0 are welcome.
There was a problem hiding this comment.
Just a quick comment on these matters:
- When rewriting a theorem to avoid some axiom, that counts as a "Revised by" and you should bring forward the "Contributed by". One way to think about this is that we optimize for the "Contributed by" date to be as early as possible, and try not to lose old dates due to the revise & deprecate cycle.
- We should try to maintain ax-13-free theorems using either "Proof modification discouraged" or the new
usage avoidstag. I'm not sure if we have support for it yet in tooling but we can go ahead with tagging things anyway.
There was a problem hiding this comment.
the "Contributed by BJ" tag would be changed into "Contributed by Mario Carneiro" and "Revised by BJ" tags.
That is fine for me.
There was a problem hiding this comment.
brabidgaw is not exactly the same theorem as brabidga, because it adds a limiting DV condition, allowing for the removal of ax-13. So both "interface" and semantics are different in detail. In the past I sometimes reworked proofs avoiding ax-13 and other axioms, but only the proof -- the theorem stayed the same. In these cases I added a revised tag. Sometimes I invented a new lemma, (like ax13lem1) where a DV condition was added to something else already existing, but then I viewed myself a contributor. If a proof had great similarity to something related I added an appreciative note at the end of the comment paragraph (Based on ideas of ...).
"Revised by" does not only mean "Proof revised by" - minor changes of the theorem/definition itself acan also be reasons for a revision. I think there are three cases:
- a theorem is replace by a new version (the label stays the same): here, it is clear that it is a revision only, the former version is usually marked as OLD and deleted after one year.
- a variant of the theorem is created (with a new label): in this case, both variants will be availabe and can be used without restrictions. Here, the creator of this variant is usually the contributor (unless the creator him-/herself decides that the main work was done by the former contributor and wants to honour this).
- a variant of the theorem is created (with a new label), but the former version becomes discouraged (this is the case under discussion): in my opinion, the change cannot be significant enough to change the contributor in this case, so that it should be a revision.
These are, of course, only rules of thumb, and there will always be border cases. I think, however, the original contributor of a deprecated/discouraged theorem should survive in the theorem which should be used instead.
There was a problem hiding this comment.
a variant of the theorem is created (with a new label), but the former version becomes discouraged
The former version is not discouraged. In fact, you are encouraged to use it when you want to express ideas without distinct variables (as in ax6e). The discouragement technique is a temporary workaround to avoid accidental import of ax-13 in theorems that can do without it. It is a misuse of a method invented for quite a different use case. One should strive for dismissing it again as soon as possible, in my eyes.
I am afraid we already see the first signs of misinterpretations here, because said misuse is not apparent enough.
I do not mean hereby that adding a dv condition to a theorem, where the proof more or less carries over from the origin, is no candidate for keeping the contributor's name in the theorem. It just wasn't done before.
There was a problem hiding this comment.
We should try to maintain ax-13-free theorems using either "Proof modification discouraged" or the new usage avoids tag. I'm not sure if we have support for it yet in tooling but we can go ahead with tagging things anyway.
Over 100 $j usage tags have already been added for the relevant theorems in PR #3886, so this is done (discouraging proof modification is not a ideal because you still want to allow further minimizations).
The discouragement technique is a temporary workaround...
Is it? At the moment we have the discouragement tool and I've not seen plans or approvals to add alternative ones. I'm afraid the current state will be very much permanent unless something like #3879 (comment) will be implemented (adding all $j need tags is more feasible now).
There was a problem hiding this comment.
At the moment we have the discouragement tool and I've not seen plans or approvals to add alternative ones. I'm afraid the current state will be very much permanent...
That's exactly why I was (and am) not in favor of adding these tags. For that you need to convince me you are up to add an adequate solution to metamath-knife or so, in the foreseeable future, replacing the current hack. This piece then issues a warning in rewrap.sh that a use of ax-13 should be checked. As a reaction you either remove its use, or add a 'Noticed' tag to your theorem.
The current state is highly motivated by quickly removing ax-13, and hampering its use, to the point, where I see our established habits been deteriorated.
I can pinpoint the downsides (dirty hack, axc11r), to no avail it seems. Well, it won't hurt my life, but I was installed as a maintainer to watch out for misuses, and voice my concerns -- permanently, if necessary.
|
As I said already before, the changes by this PR should be accepted and merged, if there are no specific objections. The general discussion about comments/credits should be continued elsewhere. |
I also agree. |
Add ~ brabidgaw, a weaker version of ~ brabidga that does not require ax-13.
Add ~ rexlimddvcbvw, a weaker version of ~ rexlimddvcbv that does not require ax-13.
Use the new theorems to reduce axiom usage.
Remove a redundant dv condition.
Add tags and revise comments.
Adjust redundant text of ~ nfiundg.
This PR drops ax-13 from 29 theorems. Full axiom usage here: b6833c3