Rename some numbered axioms in set.mm / iset.mm

[david-a-wheeler]

I think we should rename some of the numbered axioms. "ax-6" doesn't really hint at what it is, and the axioms aren't presented in that order in mmset.raw.html. The risk of renaming is that we miss some link... but once we use /label on .raw.html we can catch many problems automatically. See #698 which would do that.

Norm made a renaming proposal in 2017:
https://groups.google.com/d/msg/metamath/G1xyJb6RjfI/JSNXPIkVAwAJ

He still agrees with it.

[david-a-wheeler]

Norm, I realize that you thought long and hard about numbers vs names. I still think very short names would be better, because they would at least give a hint to what the intent is. Even two letters are a better mnemonic than a number.

[nmegill]

Norm, I realize that you thought long and hard about numbers vs names. I still think very short names would be better, because they would at least give a hint to what the intent is. Even two letters are a better mnemonic than a number.

@david-a-wheeler I am unlikely to change my mind on this. Textbooks describing Hilbert-style systems almost always number the axioms of logic (I can't think of any that doesn't). Tarski's paper on his system S2 uses axiom numbers. So we are conforming to the literature, which is a strong argument. I prefer to see the axiom list in mmset.html displayed as one would find in a book or paper, giving it a more serious and professional appearance instead of looking like computer code. Unlike mnemonics, a fixed sequential axiom numbering (without gaps) conveys a feeling of permanence and authority that can be depended on, which is important at the foundational level (at least in my opinion).

Moreover, with my proposed renumbering, if in text prose we write:

"...Tarksi's axioms (ax-4 through ax-9)..."

this tells us there are 6 axioms, and we know exactly what their names are: ax-4, ax-5, ax-6, ax-7, ax-8, and ax-9. It doesn't matter where or in what order they appear in set.mm.

If we write:

"...Tarski's axioms (ax-qi through ax-re)..."

we have no idea how many axioms there are nor what the missing axioms are named. If the order of ax-qi and ax-di are swapped in the database (for various technical reasons), then this description would become wrong.

If we write:

"...Tarski's axioms (ax-qi, ax-di, ax-ex, ax-eq, ax-le, and ax-re)..."

in addition to being verbose, it's hard to remember and ugly to read.

If I see "ax-8" mentioned somewhere, I'll immediately know that it is a Tarski axiom. If I see "ax-le", I won't know until I've memorized the mnemonics.

As a practical matter, it is relatively uncommon that we reference most axioms directly, which means their names don't really matter for most users (and when they do, we provide an alternate name like hbn1 for the current ax-6).

I will offer you the following compromise, if it is important to you: you can restate the axioms as theorems (with 1-step proofs) with whatever names you want, like we do for theorem hbn1 as an alternate name for ax-6. You can prefix them with "ax" if you want (but not "ax-", which would be confusing; "ax_" might be ok). You can even reference your alternate-name theorems in place of the direct axioms throughout set.mm if you want, putting to rest any concern that the users may be confused by axiom numbers. Then if I get hit by a bus, you will be all set to switch the official axioms to your chosen names immediately. :) But until then I want to be able to say "Tarksi's axioms (ax-4 through ax-9)".

[david-a-wheeler]

Using names instead of numbers is not that important to me. I do agree that being able to refer to a range is useful, and that is something that names don't allow. So I think that is a good argument.

[jkingdon]

I find the desciption at https://groups.google.com/d/msg/metamath/G1xyJb6RjfI/JSNXPIkVAwAJ to be a good statement of the issues.

I'm quite willing to go with Norm's call on set.mm. He's thought about it at length, has stated the reasons, and even if I find the numbers slightly cryptic, that doesn't necessarily outweigh the good arguments on the other side.

As for iset.mm, I'm thinking maybe names is a better idea, because:

• there are more axioms

• I'm not sure numbering is as well established in the constructive literature, although the only one I could find quickly which uses either number or names is https://en.wikipedia.org/wiki/Intuitionistic_logic#Hilbert-style_calculus (which uses, basically, names). Might be a little bit hard to find a lot of precedents, especially if we are looking for literature on Hilbert-style systems (as opposed to natural deduction rules).

• numbers would presumably need to be prefixed with "i" which isn't really a problem, it just might make it slightly more awkward to use the numbers in other theorem names (things similar to the pre-rename a9ev).

• one of the rationales for set.mm was "I think the axioms are going to be stable at this point, so this should be a one-time change". I have no such confidence for iset.mm. The axioms have already changed a few times and that has been with relatively few people working on iset.mm.

In any event, once the set.mm changes are checked in, it would be good to do some kind of rename in iset.mm, just because the worst of both worlds is that iset.mm is all based on the old set.mm numbers. I'm not sure I'll have much time to work on this myself, however. @david-a-wheeler do you have any interest in coming up with a proposed set of new names? And @nmegill are you wanting to weigh in on iset.mm, or just set.mm?

[nmegill]

I'm quite willing to go with Norm's call on set.mm. He's thought about it at length, has stated the reasons, and even if I find the numbers slightly cryptic, that doesn't necessarily outweigh the good arguments on the other side.

As for iset.mm, I'm thinking maybe names is a better idea, because:

• there are more axioms
• I'm not sure numbering is as well established in the constructive literature, although the only one I could find quickly which uses either number or names is https://en.wikipedia.org/wiki/Intuitionistic_logic#Hilbert-style_calculus (which uses, basically, names). Especially if we are looking for literature on Hilbert-style systems (as opposed to how natural deduction rules are named).
• numbers would presumably need to be prefixed with "i" which isn't really a problem, it just might make it slightly more awkward to use the numbers in other theorem names (things similar to the pre-rename a9ev).
• one of the rationales for set.mm was "I think the axioms are going to be stable at this point, so this should be a one-time change". I have no such confidence for iset.mm. The axioms have already changed a few times and that has been with relatively few people working on iset.mm.

I agree with all of this. Using numeric axiom names for all iset.mm axioms would probably be premature and not necessarily helpful. It can always be revisited later.

In the case of set.mm, it is truly a once-in-a-generation thing: the axioms still use the original numbers from 25 years ago, and I don't expect them to change again after this.

I will also mention another issue with descriptive names: they can be misleading for the set.mm axioms. The purpose of the auxiliary axioms (the current ax-6,7,11,12) is much more subtle than the descriptive names displayed on the MPE page suggest. First, all of them are logically redundant as axiom schemes and are included for "metalogical completeness" (in essence being able to prove all cases of bundling), which makes a short description of their logical purpose meaningless from the very start. So what we do is describe some feature based on their superficial appearance. To me their descriptive names are somewhat misleading, but it appeases people and is a cheap compromise. But I don't think their true purpose can be easily described with simple names.

Take for example the current ax-7, "quantifier commutation". For any object language theorem, quantifier commutation can already be proved from Tarski's axioms. So what is it providing? Among other things, it assists us in proving bundled versions of various theorem schemes; it itself bundles x and y. But it does not do this in isolation. All 4 auxiliary axioms ultimately work together intimately to achieve this; they are inseparable. It is much different from ZFC set theory where each axiom has an easily described purpose. (Since ax-7 is available, we do often use it for quantifier commutation in place of a longer proof from Tarski's axioms, but that is secondary to its true purpose.)

For iset.mm, bundling and "metalogical completeness" is an advanced issue that isn't too important to be concerned with at this point, where the main goal is just getting basic stuff proved.

In any event, once the set.mm changes are checked in, it would be good to do some kind of rename in iset.mm, just because the worst of both worlds is that iset.mm is all based on the old set.mm numbers. I'm not sure I'll have much time to work on this myself, however. @david-a-wheeler do you have any interest in coming up with a proposed set of new names? And @nmegill are you wanting to weigh in on iset.mm, or just set.mm?

Eventually you may want to do a rename of the axioms that were taken from set.mm, if only to make it easier to reuse some of its proofs. However, for pred calc you are probably mostly done, and beyond that the new names don't affect much. I will be keeping a permanent cross-reference table between the old and new for the benefit of external papers etc. that reference the old names, so there isn't any urgency. The list of changed theorem names will be at the top of set.mm with today's date to apply at your convenience.

Norm

[jkingdon]

Good point about bundling and "metalogical completeness" - unless/until this gets a lot more attention, we don't really know where iset.mm stands on any of it (my guess would be "noticeably different from set.mm" but that's speculation as much as anything else).

And Norm's statement about "isn't any urgency" is oddly calming. Oddly in the sense that the perfectionist in me wants to rush in and make everything right. But calming in the sense that, well, it'll happen if/when it happens and I also want other things like constructive real numbers and whatever other things would take my iset.mm time.

[david-a-wheeler]

@nmegill - Once you're done renaming the set.mm axioms (including maybe swapping 12/13), I hope you'll update the metamath book to match. Newcomers will find things a lot easier to follow if the book and actual set.mm file match :-).

[nmegill]

I've added a to-do list item to update the book.

[david-a-wheeler]

Nit: mmset.raw.html has the following text that I think should be deleted: "The above axioms evolved over time as redundancies and simplifications were discovered. As a result, the axiom numbering isn't sequential. We may rename them in the future."

[nmegill]

Nit: mmset.raw.html has the following text that I think should be deleted: "The above axioms evolved over time as redundancies and simplifications were discovered. As a result, the axiom numbering isn't sequential. We may rename them in the future."

It has already been removed on us2. although not on github yet.

[david-a-wheeler]

I believe this has been completely resolved in set.mm (and with the matching book), and there's already agreement to let iset.mm grow in whatever form it naturally takes.

So I'm closing this as resolved. If that's in error, please reopen!

[jkingdon]

I believe this has been completely resolved in set.mm (and with the matching book), and there's already agreement to let iset.mm grow in whatever form it naturally takes.

So I'm closing this as resolved. If that's in error, please reopen!

I've moved the iset.mm question to #756 . There seems to be some level of agreement as to what might make sense, but on the other hand maybe doing nothing (for now at least) is also an option.