From cd9e89be2e3b433bb53d62ee0f1fe4416d71e67c Mon Sep 17 00:00:00 2001 From: "David A. Wheeler" Date: Wed, 30 Apr 2025 18:44:28 -0400 Subject: [PATCH 1/2] Clarify ax-mulf comment 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. Signed-off-by: David A. Wheeler --- set.mm | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/set.mm b/set.mm index d39cccbe83..322f5caf74 100644 --- a/set.mm +++ b/set.mm @@ -128362,13 +128362,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 + 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. From 429a496362966d710462f079f71dd48ad574475e Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 2 Oct 2025 08:06:19 -0700 Subject: [PATCH 2/2] Revise wording of ax-mulf and axmulf This is in response to discussion on github and includes: - focus on the consequences of using it or not, with less language about which we prefer (because there doesn't seem to be a consensus about that). - compare with other operations - refer to mulcl rather than ax-mulcl directly - mention mpomulf --- iset.mm | 27 ++++++++++++--------------- set.mm | 27 ++++++++++++--------------- 2 files changed, 24 insertions(+), 30 deletions(-) diff --git a/iset.mm b/iset.mm index 3d166d510e..38c1123076 100644 --- a/iset.mm +++ b/iset.mm @@ -84297,10 +84297,10 @@ involve to natural numbers (notably, ~ axcaucvg ). (Contributed by VAWPABGJJVBVCVRWDVDSABHIJKILZJNHLXFNHRSHXFVEVFWEWBSVTWAVGZVFWCKVHSXEKVIVP VJVKVLKVRVMVNWBABJXGVOABJJJKVQVN $. - $( Multiplication is an operation on the complex numbers. This theorem can - be used as an alternate axiom for complex numbers in place of the less - specific ~ axmulcl . This construction-dependent theorem should not be - referenced directly; instead, use ~ ax-mulf . (Contributed by NM, + $( Multiplication is an operation on the complex numbers. 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 . (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) $) axmulf $p |- x. : ( CC X. CC ) --> CC $= ( vx vy vw vv vu vf vz vb va cc cmul cv co wcel wceq wa cop cmr wex wtru @@ -85486,17 +85486,14 @@ this axiom (with the defined operation in place of ` + ` ) follows as a ax-addf $a |- + : ( CC X. CC ) --> CC $. $( $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- 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 - ` ( 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. + $( Multiplication is an operation on the complex numbers. This axiom tells + us that ` x. ` is defined only on complex numbers which is analogous to + the way that other operations are defined, for example see ~ subf or + ~ eff . However, while Metamath can handle this axiom, if we wish to work + with weaker complex number axioms, we can avoid it by using the less + specific ~ mulcl . Note 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. ` , as seen in ~ mpomulf . This axiom is justified by Theorem ~ axmulf . (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) $) diff --git a/set.mm b/set.mm index 322f5caf74..2272fd643d 100644 --- a/set.mm +++ b/set.mm @@ -127715,10 +127715,10 @@ the converse membership relation (which is not an equivalence relation) YCXLMXQXSXRXTYFXQXSTYDXRXTTYEWQWLVHWKWNVHVIVNYBWRSSVJVOVKVLVEVMZVPVQJWBVR VSWGABHHYGVTABHHHJWAVS $. - $( Multiplication is an operation on the complex numbers. This theorem can - be used as an alternate axiom for complex numbers in place of the less - specific ~ axmulcl . This construction-dependent theorem should not be - referenced directly; instead, use ~ ax-mulf . (Contributed by NM, + $( Multiplication is an operation on the complex numbers. 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 . (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) $) axmulf $p |- x. : ( CC X. CC ) --> CC $= ( vx vy vw vv vu vf vz cc cmul cv co wcel wceq wa cop cmr wex cnr mulclsr @@ -128361,17 +128361,14 @@ this axiom (with the defined operation in place of ` + ` ) follows as a ax-addf $a |- + : ( CC X. CC ) --> CC $. $( $j restatement 'ax-addf' of 'axaddf'; $) - $( Multiplication is an operation on the complex numbers. This deprecated - 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 - 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. + $( Multiplication is an operation on the complex numbers. This axiom tells + us that ` x. ` is defined only on complex numbers which is analogous to + the way that other operations are defined, for example see ~ subf or + ~ eff . However, while Metamath can handle this axiom, if we wish to work + with weaker complex number axioms, we can avoid it by using the less + specific ~ mulcl . Note 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. ` , as seen in ~ mpomulf . This axiom is justified by Theorem ~ axmulf . (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) $)