Thanks for the heads-up on the list. I've given my thoughts on
(I assume you are just going to push a change for set.mm
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.
I plan to push this change to github tomorrow. In addition to the axiom number changes, theorems whose names reference axiom numbers (e.g. a17d) will also be changed to reflect the new numbering (a5d).
Most ongoing mathbox work shouldn't be affected significantly since they are typically far removed from the predicate calculus axioms. But if there are concerns or conflicts let me know.
Hi guys.First time posting here.Just my two cents: the labels should be swapped. A few reasons:- If the current labeling stays, then there will need to be a justification (most likely within set.mm itself) for why the labels are not in order (especially because all the other ones are). If the labels are swapped, no justification is needed.- I don't really agree with the "aesthetic reason". To whom will it be more aesthetic to?- For active users of set.mm, if they actually care about the predicate calculus axioms, they probably care more about the dependency relations anyway, in which case it makes much more sense for the labels to be ordered as with the dependencies (a topologically sorted order).- For random netizens who stumble across the metamath homepage (like I did), I really don't think they care. Unless they understand logic to some degree, the axioms will look kind of random to them anyway. The only thing here is aesthetically, it's nice to have the word "quantified" appear in three consecutive axioms, but I think this is a silly reason to make the labels out of order.- For members of academia, I think the only real benefit of the current scheme is perhaps making it seem prettier at the outset -- if any of them actually look into it, they'll also probably be confused as to why these two axioms are "out of order."Please let me know any thoughts you might have.Sincerely,Michael
You make good points. Since you are the third person to notice this, and TBH the present order isn't completely satisfying to me either, I will go back to the original order and swap the ax-12 and ax-13 names.
On Saturday, December 22, 2018 at 3:28:06 PM UTC-5, Michael Wu wrote: