Editing Axiom of choice (section)

==Independence==
{{See also|List of statements independent of ZFC}}
It has been known since as early as 1922 that the axiom of choice may fail in a variant of ZF with [[urelement]]s, through the technique of [[permutation model]]s introduced by [[Abraham Fraenkel]]{{sfn|Fraenkel|1922}} and developed further by [[Andrzej Mostowski]].{{sfn|Mostowski|1938}} The basic technique can be illustrated as follows: Let ''x''<sub>''n''</sub> and ''y''<sub>''n''</sub> be distinct urelements for {{nowrap|1=''n''=1, 2, 3...}}, and build a model where each set is symmetric under the interchange ''x''<sub>''n''</sub> ↔ ''y''<sub>''n''</sub> for all but a finite number of ''n''. Then the set {{nowrap|1=''X'' = {<!-- -->{''x''<sub>1</sub>, ''y''<sub>1</sub>}, {''x''<sub>2</sub>, ''y''<sub>2</sub>}, {''x''<sub>3</sub>, ''y''<sub>3</sub>}, ...} }} can be in the model but sets such as {{nowrap|{''x''<sub>1</sub>, ''x''<sub>2</sub>, ''x''<sub>3</sub>, ...} }} cannot, and thus ''X'' cannot have a choice function.

In 1938,<ref>{{Cite journal|title=The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis|journal = Proceedings of the National Academy of Sciences of the United States of America|volume = 24|issue = 12|pages = 556–557|last=Gödel|first=Kurt|date=9 November 1938|pmc = 1077160|pmid = 16577857|bibcode = 1938PNAS...24..556G|doi = 10.1073/pnas.24.12.556|doi-access = free}}</ref> [[Kurt Gödel]] showed that the ''negation'' of the axiom of choice is not a theorem of ZF by constructing an [[inner model]] (the [[constructible universe]]) that satisfies ZFC, thus showing that ZFC is consistent if ZF itself is consistent. In 1963, [[Paul Cohen (mathematician)|Paul Cohen]] employed the technique of [[forcing (mathematics)|forcing]], developed for this purpose, to show that, assuming ZF is consistent, the axiom of choice itself is not a theorem of ZF. He did this by constructing a much more complex model that satisfies ZF¬C (ZF with the negation of AC added as axiom) and thus showing that ZF¬C is consistent. Cohen's model is a [[symmetric model]], which is similar to permutation models, but uses "generic" subsets of the natural numbers (justified by forcing) in place of urelements.<ref>{{Cite web|url=https://stacks.stanford.edu/file/druid:pd104gy5838/SCM0405.pdf |archive-url=https://ghostarchive.org/archive/20221009/https://stacks.stanford.edu/file/druid:pd104gy5838/SCM0405.pdf |archive-date=2022-10-09 |url-status=live|title=The Independence of the Axiom of Choice|last=Cohen|first=Paul|date=2019|website=Stanford University Libraries|access-date=2019-03-22}}</ref>

Together these results establish that the axiom of choice is [[Independence (mathematical logic)|logically independent]] of ZF. The assumption that ZF is consistent is harmless because adding another axiom to an already inconsistent system cannot make the situation worse. Because of independence, the decision whether to use the axiom of choice (or its negation) in a proof cannot be made by appeal to other axioms of set theory. It must be made on other grounds.

One argument in favor of using the axiom of choice is that it is convenient because it allows one to prove some simplifying propositions that otherwise could not be proved. Many theorems provable using choice are of an elegant general character: the cardinalities of any two sets are comparable, every nontrivial [[Ring (mathematics)|ring]] with unity has a [[maximal ideal]], every [[vector space]] has a [[Basis (linear algebra)|basis]], every [[connected graph]] has a [[spanning tree]], and every [[Product topology|product]] of [[compact space]]s is compact, among many others. Frequently, the axiom of choice allows generalizing a theorem to "larger" objects. For example, it is provable without the axiom of choice that every vector space of finite dimension has a basis, but the generalization to all vector spaces requires the axiom of choice. Likewise, a finite product of compact spaces can be proven to be compact without the axiom of choice, but the generalization to infinite products ([[Tychonoff's theorem]]) requires the axiom of choice.

The proof of the independence result also shows that a wide class of mathematical statements, including all statements that can be phrased in the language of [[Peano arithmetic]], are provable in ZF if and only if they are provable in ZFC.<ref>This is because arithmetical statements are [[absoluteness (mathematical logic)|absolute]] to the [[constructible universe]] ''L''. [[Shoenfield's absoluteness theorem]] gives a more general result.</ref> Statements in this class include the statement that [[P = NP]], the [[Riemann hypothesis]], and many other unsolved mathematical problems. When attempting to solve problems in this class, it makes no difference whether ZF or ZFC is employed if the only question is the existence of a proof. It is possible, however, that there is a shorter proof of a theorem from ZFC than from ZF.

The axiom of choice is not the only significant statement that is independent of ZF. For example, the [[Continuum hypothesis#The generalized continuum hypothesis|generalized continuum hypothesis]] (GCH) is not only independent of ZF, but also independent of ZFC. However, ZF plus GCH implies AC, making GCH a strictly stronger claim than AC, even though they are both independent of ZF.