search

metamath / set.mm

Metamath source file for logic and set theory
Other
243 stars 88 forks source link

rmv ax-12 from ssel (ax-mulcom pr 7) #4020

Closed icecream17 closed 3 months ago

icecream17 commented 3 months ago

remove reference in remulid2 now that being a real number is not necessary to avoid ax-mulcom

(removing ax-12 from ssel at minimum removes ax-12 from elpwg: https://github.com/metamath/set.mm/pull/4015)

wlammen commented 3 months ago

While mulid2 involves ax-mulcom, sn-mulid2 needs ax-mulrcl. What is so special about ax-mulcom, that it is better exchanged for another axiom?

icecream17 commented 3 months ago

in my mathbox I am investigating whether ax-mulcom is independent, meaning all other axioms may be used.

ax-mulcom "pr 1" is arbitrarily defined as https://github.com/metamath/set.mm/pull/3713