Skip to content

Clarify ax-mulf comment #4796

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

Clarify ax-mulf comment #4796

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -127694,13 +127694,13 @@ this axiom (with the defined operation in place of ` + ` ) follows as a
$( $j restatement 'ax-addf' of 'axaddf'; $)

$( Multiplication is an operation on the complex numbers. This deprecated
axiom is provided for historical compatibility but is not a bona fide
axiom for complex numbers (independent of set theory) since it cannot be
interpreted as a first-order or second-order statement (see
~ https://us.metamath.org/downloads/schmidt-cnaxioms.pdf ). It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific ~ ax-mulcl should be used. Note that uses of ~ ax-mulf
can be eliminated by using the defined operation
axiom is provided for historical compatibility. However, while Metamath
can handle it, it cannot be interpreted as a first-order or second-order
statement. We generally prefer simpler statements (see
~ https://us.metamath.org/downloads/schmidt-cnaxioms.pdf ). This
deprecated axiom may be deleted in the future and should be avoided for
new theorems. Instead, the less specific ~ ax-mulcl should be used. Note
Copy link
Contributor

@avekens avekens May 1, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

that uses of ~ ax-mulf can be eliminated by using the defined operation
` ( x e. CC , y e. CC |-> ( x x. y ) ) ` in place of ` x. ` , from which
this axiom (with the defined operation in place of ` x. ` ) follows as a
theorem.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

@avekens avekens May 1, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

@icecream17 icecream17 May 2, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Expand Down