Table of Contents - 21.31.5. Independence of ax-mulcom
This section mainly concerns the independence of ax-mulcom, which is the
only real and complex number axiom whose independence is open (
https://us.metamath.org/mpeuni/mmcomplex.html). In particular, this is a
combination of attempts to prove more and more properties of real and complex
numbers without ax-mulcom. Completing this direction would show that
ax-mulcom is not independent.
Alternatively, one could search for a model satisfying all axioms except
ax-mulcom, thus showing it is independent. A few models satisfying
non-commutativity which only violate one other axiom are provided at
https://gist.github.com/icecream17/933f95d820e0b8f1cab0d4293b68eaf9. I
conjecture that if it is possible to prove ax-mulcom from the other axioms,
then all the other axioms are needed.
In abstract terms, the symbol would have to correspond to an infinite
non-commutative left-near-field with a Dedekind-complete order compatible
with its ring operations.
Needless to say, this is a very undeveloped area of math. In addition, such
a structure for would have to, together with the structure for the
symbol , satisfy ax-resscn, ax-icn, ax-i2m1, and most
crucially ax-cnre.
None of the theorems in this section should be moved to main. If there is a
naming conflict, feel free to add the prefix "sn-".