Rename numbered predicate logic axioms in iset.mm

[jkingdon]

Currently the predicate logic axioms in iset.mm have names which are based on the old axiom numbering in set.mm.

The reasons that set.mm uses numbers, rather than names, are described at #703 and in particular https://groups.google.com/d/msg/metamath/G1xyJb6RjfI/JSNXPIkVAwAJ

As for iset.mm, there is some level of agreement that names may be better than numbers here, 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.

Since this is a question of aesthetics and clarity, there isn't a huge cost to worrying about it later. But especially if we see names rather than numbers as being the likely end state, there also isn't much cost to doing this "prematurely", while the axioms still might be evolving.

[jkingdon]

I'd be OK with closing this issue as I'm not sure there is a large degree of consensus that anything needs to done soon (or interest in working on it), and if someone does pick it up they can look at a closed issue just as easily as an open one. For what it is worth, I haven't really thought much about axioms in a while; I've been busy with real number construction and other things which are several steps removed from the axioms themselves.

I guess I'll close this in a few days if no one has any further comments.

[digama0]

I think names are generally better than numbers because the numbers are fragile to reordering. I guess they were inherited from set.mm and things have since changed on the set.mm side? In that case either renumbering to match or just giving them names would make sense to me.

[jkingdon]

I think names are generally better than numbers because the numbers are fragile to reordering. I guess they were inherited from set.mm and things have since changed on the set.mm side? In that case either renumbering to match or just giving them names would make sense to me.

Yeah, they were inherited and switched around a bit and then set.mm renumbered.

I would prefer names as well.

[benjub]

At least for the propositional calculus part, I think there is a clear winner with many advantages, namely T. Thacher Robinson's system. I advocated it ad nauseam a few years ago on the discussion group, but let me recall:

• it is an independent set of axioms;
• its axioms are simple and short;
• all basic connectives are introduced axiomatically rather than defined;
• a subsystem of it gives minimal calculus;
• it has the separation property;
• add Peirce's axiom and obtain classical calculus (the resulting system is still independent, still has the separation property, and a susbsystem of it gives classical refutability calculus).

The separation property (a statement is provable from the axioms containing at most the connectives occurring in it and implication) has pratical advantages:

• ease of proof (given the statement to be proved, you need only concentrate on those axioms/sections of the database);
• better sectionning of the database (a crucial advantage for ease of searching; for a counterexampe, look at Subsection 1.2.6 of set.mm).

As for the names (you can deduce the axioms from the names, without being a metamather: great advantage): ax-mp ax-k ax-s ax-iffelim1/ax-iffelim2/ax-iffintro ax-andelim1/ax-andelim2/ax-andintro ax-orintro1/ax-orintro2/ax-orelim ax-contrap ax-notelim ax-falseelim (aka ax-exfalso)

If the names are too long, one can use aliases, i.e. ax-orintro1 is discouraged and referenced by a single result, ax-ori1 (then, in the "axioms used" list on the webpages, you see "ax-orintro1" which is self-explanatory).

One could group ax-k and ax-s into a single axiom ax-minimp for minimal implicational calculus (since it's a bloc in itself, and we do not worry about what is provable without ax-k or without ax-s), discourage its usage, and prove axs and axk from it (see my mathbox in set.mm).

Note that Robinson does not introduce the "iff" group. Also, he uses either negation or falsehood, and defines one in terms of the other the usual way, but I think it's clearer that both be introduced axiomatically as above, and the interdefinability be proved.

This system is so superior, that after a few years, set.mm will probably adopt it and simply add ax-peirce. This will halve efforts of development in the propositional calculus part.

As for the predicate calculus part, I have some ideas for the names (like probably all of you), that @nmegill and @digama0 know of, but this can come in a second phase.

[jkingdon]

I've changed the title to include "predicate logic" since that was always the scope of this issue.

Another consideration which makes me even less sure than before is that there are various theorems named after numbered axioms (the one which came up recently is ax6evr from #2624 ), and although a certain degree of difference from set.mm is inevitable when it comes to predicate logic, I'd prefer to keep it down because we do move proofs between iset.mm and set.mm a fair bit (including in #2624 ). So I'm inclined to switch to the set.mm numbering for those axioms which the two have in common and do something else (names not based on numbers, perhaps) for the axioms which are only in iset.mm.

[benjub]

In reply to @jkingdon's latest: I think any modifications towards the rule

if two labeled statements ($f $e $a $p) are identical in set.mm and iset.mm, then they should have the same label (edit: and conversely)

are good, so if you have the energy to renumber, go for it. The additional axioms can be labeled "ax-i#" following your current naming scheme, where # is either the number of the closest set.mm-equivalent, or the next available number.

As for the naming ideas I mentioned in my previous post, they are now public at https://arxiv.org/abs/2202.10383 (summary on the last page) and https://arxiv.org/abs/2109.14745. Note that these are not prescriptions or recommendations, but only ideas or proposals if one is willing to go that way.

[benjub]

Side note: I ran into a discussion on the FOM mailing list about the role of "ex falso (quodlibet)", or EFQ, or "explosion" (in which @digama0 took part), in May and June: https://cs.nyu.edu/pipermail/fom/2022-May/thread.html and https://cs.nyu.edu/pipermail/fom/2022-June/thread.html

If using the axiom system I proposed above, which contains ex-falso (ax-falseelim) as an independent axiom, Metamath could have been linked for some basic, but formalized, results, from which to go (even if the system used there was sequent calculus).