Axiom of Choice

In classical logic, an optional axiom of set theory. It asserts that out of an arbitrary (even non-enumerable) family (internal set) of non-empty sets, you can find a function that (simultaneously) picks for each set in the family an element of said set. The axiom of choice is equivalent to Zorn's Lemma or Zermelo's theorem. A weaker version often used in classical logic is the Theorem of Compacity.

The axiom was long controversial, because it allows reasoning about objects that are non-constructible, and beyond imagination (like unreachable ordinals). It was finally proven that the axiom is independent from the other usual axioms of Set Theory: you can as well admit it or reject it, and end up with as consistent logic models.

In a way, it can be argued that classical logic is verily built upon some kind of use of the axiom of choice at the meta-level: simultaneous coherent choice of a truth value for every proposition. Utter rejection of the Axiom of Choice and of the things that it entails has led to the discovery of Intuitionnistic Logic and Constructive Logic, and the development of Proof Theory.