From 4655db6d603255c64e2c98983bd39ed3c06bc3f7 Mon Sep 17 00:00:00 2001 From: "David A. Wheeler" Date: Wed, 30 Apr 2025 18:44:28 -0400 Subject: [PATCH] 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 cba01bb92..1d3e86d27 100644 --- a/set.mm +++ b/set.mm @@ -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 + 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.