The Axiom of Choice: A Century of Debate
This paper delves into the century-long debate surrounding the Axiom of Choice in mathematics. From Cantor's well-ordering principle to Zermelo's proof and introduction of the Axiom of Choice, the mathematical community engaged in heated discussions. The article deeply analyzes different forms of the Axiom of Choice, including the constructive and extensional versions, highlighting the issue with the extensional version: it violates the principle of 'you cannot get something from nothing'. Through proofs in constructive type theory, the paper reveals the relationship between the extensional Axiom of Choice, Zermelo's Axiom of Choice, and the topos-theoretic Axiom of Choice, concluding that the extensional Axiom of Choice is the correct rendering of Zermelo's Axiom in constructive type theory.