Was there ever an axiom rendered a theorem?

The most famous example I know is that of Hilbert's axiom II.4 for the linear ordering of points on a line, for Euclidean geometry, proven to be superfluous by E.H. Moore. See this wikipedia article, especially "Hilbert's discarded axiom". https://en.wikipedia.org/wiki/Hilbert%27s_axioms

In the article of Moore linked there, it is stated that also axiom I.4 is superfluous.

http://www.ams.org/journals/tran/1902-003-01/S0002-9947-1902-1500592-8/S0002-9947-1902-1500592-8.pdf


Fraenkel introduced the axiom schema of replacement to set theory. This implied the axiom schema of comprehension, and allowed the empty set and unordered pair axioms to follow from the axiom of infinity. (Note Zermelo set theory includes the axiom of choice whereas ZF does not, so Zermelo+replacement is ZFC.) The "deleted" axioms are typically listed when describing ZF(C), partly so people realise they're in Zermelo set theory, partly for easier comparisons with other set theories of interest.


Yes, everywhere. What is an axiom from one theory can be a theorem in another.

Euclid's fifth postulate can be replaced by the statement that the angles on the inside of each triangle add up to $\pi$ radians.

Another notable example is the axiom of choice, which is equivalent in some axiomatic systems to Zorn's Lemma.

Also, watch this Feynman clip.