Predicate calculus axiom renumbering

[Norman Megill]

On July 18, 2017, I proposed a change to the axiom numbering:
https://groups.google.com/d/msg/metamath/G1xyJb6RjfI/JSNXPIkVAwAJ

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.

Norm

[Jim Kingdon]

Thanks for the heads-up on the list. I've given my thoughts on iset.mm here: https://github.com/metamath/set.mm/issues/703#issuecomment-448806468 (I assume you are just going to push a change for set.mm tomorrow?)

--
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.

[fl]

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.

What a joy to be able to make the changes you want without having to justify yourself. I remember trying to get my proofs in category theory   formalized without ever having any answers but loopholes from Megill. All the proofs were of course made at his request. They were eventually replaced by those of Carneiro, still without explanation. Not a very nice thing to do.

-- 

FL

[David A. Wheeler]

On Thu, 20 Dec 2018 04:27:10 -0800 (PST), "'fl' via Metamath" <meta...@googlegroups.com> wrote:
> What a joy to be able to make the changes you want without having to
> justify yourself.

Not true. There was a long justification here:

https://groups.google.com/d/msg/metamath/G1xyJb6RjfI/JSNXPIkVAwAJ

Further discussion here:

https://github.com/metamath/set.mm/issues/703

--- David A. Wheeler

[Thomas Brendan Leahy]

Is there a reason 13 still comes before 12?

[Norman Megill]

Gérard brought this up also.  I assume that "comes before" you mean in set.mm.

I chose the ax-12 and ax-13 naming order in the 2017 proposal for essentially superficial aesthetic reasons:  ax-12 seemed to belong with the two other "quantifier introduction" axioms above it, and ax-13 seemed the "most complicated" (the only axiom with both wff and individual variables) so I put it last.

The order of introduction in set.mm can easily be changed to introduce ax-12 first, but after looking at it last night I'm not sure it should.  Often we like to introduce an axiom then prove as many new things as we can with it.  There are over 200 theorems using ax-13 but not ax-12, whereas there are only 2 theorems (ax12v and ax12lem2) using ax-12 but not ax-13.  In other words ax-12 is almost completely useless without ax-13 to assist it.

So, maybe I made a mistake, and the ax-12/ax-13 labels should be swapped.  If we are going to do so, this is certainly the time to do it.  Let me hear some opinions.

Norm

[Michael Wu]

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

--

[Norman Megill]

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.

Norm

On Saturday, December 22, 2018 at 3:28:06 PM UTC-5, Michael Wu wrote:

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

[Norman Megill]

The axiom names ax-12 and ax-13 are now been swapped everywhere:
http://us2.metamath.org:88/mpeuni/mmset.html#pcaxioms
http://us2.metamath.org:88/mpeuni/mmtheorems.html#dtl:1.5

The post with the cross-reference list was edited:
https://groups.google.com/forum/#!msg/metamath/G1xyJb6RjfI/JSNXPIkVAwAJ

In response to someone's question, the reason the obsolete axioms have been renamed ax-c* is to match the ones in my 1995 paper; for example ax-c4 is axiom C4' there.  This is also explained here:
http://us2.metamath.org:88/mpeuni/mmset.html#subsys

Thanks to David for scripts that make editing the mm*.html files (in the form of mm*.raw.html), and keeping them up to date, much easier.  The new 'markup' command in metamath.exe converts mm*.raw.html to mm*.html; see 'help markup'.

Norm

On Saturday, December 22, 2018 at 4:55:45 PM UTC-5, Norman Megill wrote:

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.

Norm

On Saturday, December 22, 2018 at 3:28:06 PM UTC-5, Michael Wu wrote:

...

[Norman Megill]

I added Appendix 8 to the MPE Home Page, which is intended to provide a permanent cross reference between new and old axiom numbers.
http://us2.metamath.org:88/mpeuni/mmset.html#oldaxioms

Norm