Edit credits, add comments #3923
Conversation
|
The way the credits are handled, is not convincing to me, to be honest. As far as my person is concerned, I do not care much. But in principle is adding DV conditions and finding a proof for such a specialized theorem an act of ingeniosity in its own right in most cases. The proofs do not generally carry over (see https://us.metamath.org/mpeuni/spei.html /https://us.metamath.org/mpeuni/speiv.html for example). This is similar to specializing a group to a symmetric group, for example. Extra conditions are added, allowing for a different theory, in the end with its own rules and proof techniques. Why should one specializing a general rule about groups to symmetric ones not appear as contributor of that theorem, but as a reviser of the one in the more general context? Why are DV conditions handled differently to adding/modifying a hypothesis line? I don't think this comment should block this PR. But it can serve as a starting point for a discussion after which we adapt our conventions accordingly, and corrections in set.mm can be made. In case it is supported by some, I will open an issue regarding this topic. |
This PR applies @avekens request #3905 (comment) of adding comments and credits to theorems avoiding ax-13. The criteria goes as follows: scan through the discouraged theorems using ax-13 and check out whether they have a newer weaker version; if they have one then replace the credit of the weaker version with the contributor of the original one. As default I only added the original contributor and not the following revisers, as it's not always clear to me whether they play a role on the new version (specifically it's not always stated whether the revison concerned the old proof only and not the statement itself). This may change with the review process.
Additional changes:
Replace usages of ralcom2 and ralcom2w with ralcom, which uses less axioms (and delete my version ralcom2w since it's just redundant and never used).
Delete my version cbvrabcsfw since it was only added to avoid ax-13, but it's never used.
Delete my mathbox. The information it contains it's not relevant anymore and I'm not planning to add other stuff into it. So, to avoid waste of space, it can be removed.