Clarify ax-mulf comment

[david-a-wheeler]

The ax-mulf comment is confusing.
Its text "is not a bona fide axiom for complex numbers" makes it sound like this statement can't be an axiom or that Metamath can't handle such axioms, which is obviously untrue. Also, the cited paper doesn't justify this axiom.

This commit attempts to clarify the comment for ax-mulf in the hopes of making it clearer.

[avekens]

"Instead, the less specific ~ ax-mulcl should be used." Is this (still) true? The usage of ~ax-mulcl is also discouraged, and ~mulcl should be used instead. ~ax-mulcl is currently used in the proof for ~mulcl only.

[GinoGiotto]

Yes, ~ax-mulcl should not be used directly, it should be used only through ~mulcl. As of today, all theorems obey this rule.

[avekens]

We have this theorem already: it is ~mpomulf. This should be mentioned here.

[avekens]

I like these clarifications/improvements of comments very much.
Besides my inlne comments: What about the comment for ~axmulf? It contains "instead, use ~ ax-mulf", which is certainly not valid anymore.

[avekens]

I would like to hear @GinoGiotto `s opinon before this PR is merged. He put a lot of effort into the removal of ~ax-mulf from proofs.

[GinoGiotto]

What about the comment for ~axmulf? It contains "instead, use ~ ax-mulf", which is certainly not valid anymore.

Indeed. The comment could be revised to reference both, for example: "This is the construction-dependent version of ~ax-mulf and it should not be referenced outside the construction. We generally prefer to develop our theory using the less specific ~mulcl."

I would like to hear @GinoGiotto `s opinon before this PR is merged. He put a lot of effort into the removal of ~ax-mulf from proofs.

In a recent discussion with @jkingdon, it was brought to light that the reference to the Schmidt paper is not very clear. When the author mentions that one of the axioms cannot be interpreted as a first-order or second-order statement, the description of such axiom appears to match ~ax-cnex rather than ~ax-mulf. In fact, it seems ~ax-mulf is never mentioned at all (not even as ~ax-mulopr). This left me puzzled. Did the author of the comment implicitly state that the argument given for ~ax-cnex could also be applied to ~ax-mulf? (The revision of this PR seems to indirectly solve this issue already, though.)

[icecream17]

The paper doesn't mention ax-addf or ax-mulf so I don't think the author was implying anything about them.

Edit: It might be covered by page 2 note 1:

There are other, minor differences between our presentation and Megill’s; these need not detain us.

[GinoGiotto]

Edit: It might be covered by page 2 note 1:

There are other, minor differences between our presentation and Megill’s; these need not detain us.

This note doesn't justify the claim made in the ax-mulf comment (which I assume was written by Norm, since he's the contributor). It's way too vague to be considered a valid source for anything related to ax-addf or ax-mulf.

In my opinion, the most natural solution would be to cite the Schmidt paper in a more appropriate context, possibly alongside ~ax-cnex or on the webpages, and remove it entirely from the ax-addf/mulf comments, where it's not pertinent.

[metakunt]

I would like to know why the fact that + is a function on CC X CC is so problematic? Is it because it's construction dependent. Or is it because it's untyped? I've looked a bit into it and it appears that we build lots of theory on this conclusion anyways. Getting rid of it would also make https://us.metamath.org/mpeuni/cnfldadd.html way more complicated. I don't know if the trade-off is worth it?

[icecream17]

I think the comment of ax-addf regarding not being a first or second order statement is wrong.

The axiom, along with addcl is equivalent to:

dom + = ( CC X. CC )

A. x A. y ( x + y <-> ( x e. CC /\ y e. CC ) )

which is a first order statement.

So I think the best argument is that it's construction dependent. + could be a more general operator, for example.

Though I think ax-addf is still useful to show that if 2 + 3 = 5, it isn't because ⟨2, 3⟩ happens to be out of range and (/) = 5

[GinoGiotto]

I've looked a bit into it and it appears that we build lots of theory on this conclusion anyways

The axiom ax-addf is currently used by 3506 theorems, about the same as ax-mulf one month ago. Currently, however, ax-mulf is used by 1629 theorems, which less than half that amount. The propagation of ax-mulf does not make its removal particularly difficult, and the same story is applicable to ax-addf as well. The edit of a few dozen theorems was enough to accomplish a 50%+ reduction.

Getting rid of it would also make https://us.metamath.org/mpeuni/cnfldadd.html way more complicated.

I'm not sure what this means. The proof of cnfldadd has already been revised recently and it doesn't need to be touched further, unless someone finds shortenings or other usual maintainance stuff. To avoid ax-addf in proofs, you can use mpocnfldadd instead, which isn't particularly demanding.

If you're not satisfied with the ongoing proof modifications, an alternative strategy would be to add variations of 'is a ring', 'is a group' kind of theorems, formulated with maps-to notation in the hypotheses.

Let's take the example of a 'is a commutative ring' theorem, which is iscrngd:

$d x .1. $.  $d x y z B $.  $d ph x y z $.  $d x R y z $.
isringd.b $e |- ( ph -> B = ( Base ` R ) ) $.
isringd.p $e |- ( ph -> .+ = ( +g ` R ) ) $.
isringd.t $e |- ( ph -> .x. = ( .r ` R ) ) $.
isringd.g $e |- ( ph -> R e. Grp ) $.
isringd.c $e |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) e. B ) $.
isringd.a $e |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) $.
isringd.d $e |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) ) $.
isringd.e $e |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) $.
isringd.u $e |- ( ph -> .1. e. B ) $.
isringd.i $e |- ( ( ph /\ x e. B ) -> ( .1. .x. x ) = x ) $.
isringd.h $e |- ( ( ph /\ x e. B ) -> ( x .x. .1. ) = x ) $.
iscrngd.c $e |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) = ( y .x. x ) ) $.
iscrngd $p |- ( ph -> R e. CRing ) $= ... $.

There is only one theorem that uses iscrngd, and that theorem is cncrng, therefore I opted for revising the proof of cncrng directly, however one could add a mpoisringd instead:

$d x .1. u v $.  $d x y z u v B $.  $d ph x y z u v $.  $d x R y z u v $.
mpoisringd.b $e |- ( ph -> B = ( Base ` R ) ) $.
mpoisringd.p $e |- ( ph -> ( u e. B , v e. B |-> ( u .+ v ) ) = ( +g ` R ) ) $.
mpoisringd.t $e |- ( ph -> ( u e. B , v e. B |-> ( u .x. v ) ) = ( .r ` R ) ) $.
mpoisringd.g $e |- ( ph -> R e. Grp ) $.
mpoisringd.c $e |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) e. B ) $.
mpoisringd.a $e |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) $.
mpoisringd.d $e |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) ) $.
mpoisringd.e $e |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) ) $.
mpoisringd.u $e |- ( ph -> .1. e. B ) $.
mpoisringd.i $e |- ( ( ph /\ x e. B ) -> ( .1. .x. x ) = x ) $.
mpoisringd.h $e |- ( ( ph /\ x e. B ) -> ( x .x. .1. ) = x ) $.
mpoiscrngd.c $e |- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) = ( y .x. x ) ) $.
mpoiscrngd $p |- ( ph -> R e. CRing ) $= ... $.

If mpoiscrngd is used instead of iscrngd in cncrng, the revised proof of cncrng would be nearly identical to the original, so much so that a revision tag and OLD proof probably wouldn't be necessary.

However, the fact that iscrngd is used only once doesn't make the addition of mpoiscrngd particularly convenient. Realistically, these mpois* additions would be used only by theorems about the CCfld structure, so you're not really generalizing, you are just shifting the revision somewhere else. I'd say such additions might be worth it when used a couple of times or more.

Unfortunately, iscrngd is not the exception. It seems that many of these new theorems would be used just once. If we apply this approach without discrimination we would need to add many of them. A partial list of those that I checked includes: ~iscrngd, ~isringid, ~isdrngd, ~issrngd, ~issubrg2, ~isabvd, ~issubg2, ~ismhm, ~issrg, ~issubm, ~isghm, ~isghmd and more.

[metakunt]

That's not what I meant. I thought that cnfldadd couldn't be proved in its current form if you didn't have ax-addf and you would have a slightly more complicated operation. In any case, I don't particularly care about the axiom reduction, I just want stuff to work ;)

[GinoGiotto]

I thought that cnfldadd couldn't be proved in its current form if you didn't have ax-addf and you would have a slightly more complicated operation.

Yes, cnfldadd is not provable if ax-addf gets deleted. You would use mpocnfldadd in all cases. However, deletion is a different story from axiom usage reduction, and since it's not yet clear how low the usage can go, it's premature to make such decision.

[digama0]

FWIW, I don't think it is worthwhile to eliminate ax-addf and ax-mulf. It is quite useful to know that these operators are proper functions, and it is trivial to reconstruct a function from it even if we don't have the axiom, so it seems like just an annoyance to hide this fact.