
This article includes a list of general references, but it lacks sufficient corresponding inline citations.(February 2024) |
In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as Russell's paradox. Today, Zermelo–Fraenkel set theory, with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics. Zermelo–Fraenkel set theory with the axiom of choice included is abbreviated ZFC, where C stands for "choice", and ZF refers to the axioms of Zermelo–Fraenkel set theory with the axiom of choice excluded.
Informally, Zermelo–Fraenkel set theory is intended to formalize a single primitive notion, that of a hereditary well-founded set, so that all entities in the universe of discourse are such sets. Thus the axioms of Zermelo–Fraenkel set theory refer only to pure sets and prevent its models from containing urelements (elements that are not themselves sets). Furthermore, proper classes (collections of mathematical objects defined by a property shared by their members where the collections are too big to be sets) can only be treated indirectly. Specifically, Zermelo–Fraenkel set theory does not allow for the existence of a universal set (a set containing all sets) nor for unrestricted comprehension, thereby avoiding Russell's paradox. Von Neumann–Bernays–Gödel set theory (NBG) is a commonly used conservative extension of Zermelo–Fraenkel set theory that does allow explicit treatment of proper classes.
There are many equivalent formulations of the axioms of Zermelo–Fraenkel set theory. Most of the axioms state the existence of particular sets defined from other sets. For example, the axiom of pairing says that given any two sets and there is a new set containing exactly and . Other axioms describe properties of set membership. A goal of the axioms is that each axiom should be true if interpreted as a statement about the collection of all sets in the von Neumann universe (also known as the cumulative hierarchy).
The metamathematics of Zermelo–Fraenkel set theory has been extensively studied. Landmark results in this area established the logical independence of the axiom of choice from the remaining Zermelo-Fraenkel axioms and of the continuum hypothesis from ZFC. The consistency of a theory such as ZFC cannot be proved within the theory itself, as shown by Gödel's second incompleteness theorem.
History
The modern study of set theory was initiated by Georg Cantor and Richard Dedekind in the 1870s. However, the discovery of paradoxes in naive set theory, such as Russell's paradox, led to the desire for a more rigorous form of set theory that was free of these paradoxes.
In 1908, Ernst Zermelo proposed the first axiomatic set theory, Zermelo set theory. However, as first pointed out by Abraham Fraenkel in a 1921 letter to Zermelo, this theory was incapable of proving the existence of certain sets and cardinal numbers whose existence was taken for granted by most set theorists of the time, notably the cardinal number aleph-omega () and the set
where
is any infinite set and
is the power set operation. Moreover, one of Zermelo's axioms invoked a concept, that of a "definite" property, whose operational meaning was not clear. In 1922, Fraenkel and Thoralf Skolem independently proposed operationalizing a "definite" property as one that could be formulated as a well-formed formula in a first-order logic whose atomic formulas were limited to set membership and identity. They also independently proposed replacing the axiom schema of specification with the axiom schema of replacement. Appending this schema, as well as the axiom of regularity (first proposed by John von Neumann), to Zermelo set theory yields the theory denoted by ZF. Adding to ZF either the axiom of choice (AC) or a statement that is equivalent to it yields ZFC.
Formal language
Formally, ZFC is a one-sorted theory in first-order logic. The equality symbol can be treated as either a primitive logical symbol or a high-level abbreviation for having exactly the same elements. The former approach is the most common. The signature has a single predicate symbol, usually denoted , which is a predicate symbol of arity 2 (a binary relation symbol). This symbol symbolizes a set membership relation. For example, the formula
means that
is an element of the set
(also read as
is a member of
).
There are different ways to formulate the formal language. Some authors may choose a different set of connectives or quantifiers. For example, the logical connective NAND alone can encode the other connectives, a property known as functional completeness. This section attempts to strike a balance between simplicity and intuitiveness.
The language's alphabet consists of:
- A countably infinite amount of variables used for representing sets
- The logical connectives
,
,
- The quantifier symbols
,
- The equality symbol
- The set membership symbol
- Brackets ( )
With this alphabet, the recursive rules for forming well-formed formulae (wff) are as follows:
- Let
and
be metavariables for any variables. These are the two ways to build atomic formulae (the simplest wffs):
- Let
and
be metavariables for any wff, and
be a metavariable for any variable. These are valid wff constructions:
A well-formed formula can be thought as a syntax tree. The leaf nodes are always atomic formulae. Nodes and
have exactly two child nodes, while nodes
,
and
have exactly one. There are countably infinitely many wffs, however, each wff has a finite number of nodes.
Axioms
There are many equivalent formulations of the ZFC axioms. The following particular axiom set is from Kunen (1980). The axioms in order below are expressed in a mixture of first order logic and high-level abbreviations.
Axioms 1–8 form ZF, while the axiom 9 turns ZF into ZFC. Following Kunen (1980), we use the equivalent well-ordering theorem in place of the axiom of choice for axiom 9.
All formulations of ZFC imply that at least one set exists. Kunen includes an axiom that directly asserts the existence of a set, although he notes that he does so only "for emphasis". Its omission here can be justified in two ways. First, in the standard semantics of first-order logic in which ZFC is typically formalized, the domain of discourse must be nonempty. Hence, it is a logical theorem of first-order logic that something exists — usually expressed as the assertion that something is identical to itself, . Consequently, it is a theorem of every first-order theory that something exists. However, as noted above, because in the intended semantics of ZFC, there are only sets, the interpretation of this logical theorem in the context of ZFC is that some set exists. Hence, there is no need for a separate axiom asserting that a set exists. Second, however, even if ZFC is formulated in so-called free logic, in which it is not provable from logic alone that something exists, the axiom of infinity asserts that an infinite set exists. This implies that a set exists, and so, once again, it is superfluous to include an axiom asserting as much.
Axiom of extensionality
Two sets are equal (are the same set) if they have the same elements.
The converse of this axiom follows from the substitution property of equality. ZFC is constructed in first-order logic. Some formulations of first-order logic include identity; others do not. If the variety of first-order logic in which one is constructing set theory does not include equality "",
may be defined as an abbreviation for the following formula:
In this case, the axiom of extensionality can be reformulated as
which says that if and
have the same elements, then they belong to the same sets.
Axiom of regularity (also called the axiom of foundation)
Every non-empty set contains a member
such that
and
are disjoint sets.
or in modern notation:
This (along with the axioms of pairing and union) implies, for example, that no set is an element of itself and that every set has an ordinal rank.
Axiom schema of specification (or of separation, or of restricted comprehension)
Subsets are commonly constructed using set builder notation. For example, the even integers can be constructed as the subset of the integers satisfying the congruence modulo predicate
:
In general, the subset of a set obeying a formula
with one free variable
may be written as:
The axiom schema of specification states that this subset always exists (it is an axiom schema because there is one axiom for each ). Formally, let
be any formula in the language of ZFC with all free variables among
(
is not free in
). Then:
Note that the axiom schema of specification can only construct subsets and does not allow the construction of entities of the more general form:
This restriction is necessary to avoid Russell's paradox (let then
) and its variants that accompany naive set theory with unrestricted comprehension (since under this restriction
only refers to sets within
that don't belong to themselves, and
has not been established, even though
is the case, so
stands in a separate position from which it can't refer to or comprehend itself; therefore, in a certain sense, this axiom schema is saying that in order to build a
on the basis of a formula
, we need to previously restrict the sets
will regard within a set
that leaves
outside so
can't refer to itself; or, in other words, sets shouldn't refer to themselves).
In some other axiomatizations of ZF, this axiom is redundant in that it follows from the axiom schema of replacement and the axiom of the empty set.
On the other hand, the axiom schema of specification can be used to prove the existence of the empty set, denoted , once at least one set is known to exist. One way to do this is to use a property
which no set has. For example, if
is any existing set, the empty set can be constructed as
Thus, the axiom of the empty set is implied by the nine axioms presented here. The axiom of extensionality implies the empty set is unique (does not depend on ). It is common to make a definitional extension that adds the symbol "
" to the language of ZFC.
Axiom of pairing
If and
are sets, then there exists a set which contains
and
as elements, for example if x = {1,2} and y = {2,3} then z will be {{1,2},{2,3}}
The axiom schema of specification must be used to reduce this to a set with exactly these two elements. The axiom of pairing is part of Z, but is redundant in ZF because it follows from the axiom schema of replacement if we are given a set with at least two elements. The existence of a set with at least two elements is assured by either the axiom of infinity, or by the axiom schema of specification[dubious – discuss] and the axiom of the power set applied twice to any set.
Axiom of union
The union over the elements of a set exists. For example, the union over the elements of the set is
The axiom of union states that for any set of sets , there is a set
containing every element that is a member of some member of
:
Although this formula doesn't directly assert the existence of , the set
can be constructed from
in the above using the axiom schema of specification:
Axiom schema of replacement
The axiom schema of replacement asserts that the image of a set under any definable function will also fall inside a set.
Formally, let be any formula in the language of ZFC whose free variables are among
so that in particular
is not free in
. Then:
(The unique existential quantifier denotes the existence of exactly one element such that it follows a given statement.)
In other words, if the relation represents a definable function
,
represents its domain, and
is a set for every
then the range of
is a subset of some set
. The form stated here, in which
may be larger than strictly necessary, is sometimes called the axiom schema of collection.
Axiom of infinity
0 | = | {} | = | ∅ |
---|---|---|---|---|
1 | = | {0} | = | {∅} |
2 | = | {0,1} | = | {∅,{∅}} |
3 | = | {0,1,2} | = | {∅,{∅},{∅,{∅}}} |
4 | = | {0,1,2,3} | = | {∅,{∅},{∅,{∅}},{∅,{∅},{∅,{∅}}}} |
Let abbreviate
where
is some set. (We can see that
is a valid set by applying the axiom of pairing with
so that the set z is
). Then there exists a set X such that the empty set
, defined axiomatically, is a member of X and, whenever a set y is a member of X then
is also a member of X.
or in modern notation:
More colloquially, there exists a set X having infinitely many members. (It must be established, however, that these members are all different because if two elements are the same, the sequence will loop around in a finite cycle of sets. The axiom of regularity prevents this from happening.) The minimal set X satisfying the axiom of infinity is the von Neumann ordinal ω which can also be thought of as the set of natural numbers
Axiom of power set
By definition, a set is a subset of a set
if and only if every element of
is also an element of
:
The Axiom of power set states that for any set , there is a set
that contains every subset of
:
The axiom schema of specification is then used to define the power set as the subset of such a
containing the subsets of
exactly:
Axioms 1–8 define ZF. Alternative forms of these axioms are often encountered, some of which are listed in Jech (2003). Some ZF axiomatizations include an axiom asserting that the empty set exists. The axioms of pairing, union, replacement, and power set are often stated so that the members of the set whose existence is being asserted are just those sets which the axiom asserts
must contain.
The following axiom is added to turn ZF into ZFC:
Axiom of well-ordering (choice)
The last axiom, commonly known as the axiom of choice, is presented here as a property about well-orders, as in Kunen (1980). For any set , there exists a binary relation
which well-orders
. This means
is a linear order on
such that every nonempty subset of
has a least element under the order
.
Given axioms 1 – 8, many statements are provably equivalent to axiom 9. The most common of these goes as follows. Let be a set whose members are all nonempty. Then there exists a function
from
to the union of the members of
, called a "choice function", such that for all
one has
. A third version of the axiom, also equivalent, is Zorn's lemma.
Since the existence of a choice function when is a finite set is easily proved from axioms 1–8, AC only matters for certain infinite sets. AC is characterized as nonconstructive because it asserts the existence of a choice function but says nothing about how this choice function is to be "constructed".
Motivation via the cumulative hierarchy
One motivation for the ZFC axioms is the cumulative hierarchy of sets introduced by John von Neumann. In this viewpoint, the universe of set theory is built up in stages, with one stage for each ordinal number. At stage 0, there are no sets yet. At each following stage, a set is added to the universe if all of its elements have been added at previous stages. Thus the empty set is added at stage 1, and the set containing the empty set is added at stage 2. The collection of all sets that are obtained in this way, over all the stages, is known as V. The sets in V can be arranged into a hierarchy by assigning to each set the first stage at which that set was added to V.
It is provable that a set is in V if and only if the set is pure and well-founded. And V satisfies all the axioms of ZFC if the class of ordinals has appropriate reflection properties. For example, suppose that a set x is added at stage α, which means that every element of x was added at a stage earlier than α. Then, every subset of x is also added at (or before) stage α, because all elements of any subset of x were also added before stage α. This means that any subset of x which the axiom of separation can construct is added at (or before) stage α, and that the powerset of x will be added at the next stage after α.
The picture of the universe of sets stratified into the cumulative hierarchy is characteristic of ZFC and related axiomatic set theories such as Von Neumann–Bernays–Gödel set theory (often called NBG) and Morse–Kelley set theory. The cumulative hierarchy is not compatible with other set theories such as New Foundations.
It is possible to change the definition of V so that at each stage, instead of adding all the subsets of the union of the previous stages, subsets are only added if they are definable in a certain sense. This results in a more "narrow" hierarchy, which gives the constructible universe L, which also satisfies all the axioms of ZFC, including the axiom of choice. It is independent from the ZFC axioms whether V = L. Although the structure of L is more regular and well behaved than that of V, few mathematicians argue that V = L should be added to ZFC as an additional "axiom of constructibility".
Metamathematics
Virtual classes
Proper classes (collections of mathematical objects defined by a property shared by their members which are too big to be sets) can only be treated indirectly in ZF (and thus ZFC). An alternative to proper classes while staying within ZF and ZFC is the virtual class notational construct introduced by Quine (1969), where the entire construct y ∈ { x | Fx } is simply defined as Fy. This provides a simple notation for classes that can contain sets but need not themselves be sets, while not committing to the ontology of classes (because the notation can be syntactically converted to one that only uses sets). Quine's approach built on the earlier approach of Bernays & Fraenkel (1958). Virtual classes are also used in Levy (2002), Takeuti & Zaring (1982), and in the Metamath implementation of ZFC.
Finite axiomatization
The axiom schemata of replacement and separation each contain infinitely many instances. Montague (1961) included a result first proved in his 1957 Ph.D. thesis: if ZFC is consistent, it is impossible to axiomatize ZFC using only finitely many axioms. On the other hand, von Neumann–Bernays–Gödel set theory (NBG) can be finitely axiomatized. The ontology of NBG includes proper classes as well as sets; a set is any class that can be a member of another class. NBG and ZFC are equivalent set theories in the sense that any theorem not mentioning classes and provable in one theory can be proved in the other.
Consistency
Gödel's second incompleteness theorem says that a recursively axiomatizable system that can interpret Robinson arithmetic can prove its own consistency only if it is inconsistent. Moreover, Robinson arithmetic can be interpreted in general set theory, a small fragment of ZFC. Hence the consistency of ZFC cannot be proved within ZFC itself (unless it is actually inconsistent). Thus, to the extent that ZFC is identified with ordinary mathematics, the consistency of ZFC cannot be demonstrated in ordinary mathematics. The consistency of ZFC does follow from the existence of a weakly inaccessible cardinal, which is unprovable in ZFC if ZFC is consistent. Nevertheless, it is deemed unlikely that ZFC harbors an unsuspected contradiction; it is widely believed that if ZFC were inconsistent, that fact would have been uncovered by now. This much is certain — ZFC is immune to the classic paradoxes of naive set theory: Russell's paradox, the Burali-Forti paradox, and Cantor's paradox.
Abian & LaMacchia (1978) studied a subtheory of ZFC consisting of the axioms of extensionality, union, powerset, replacement, and choice. Using models, they proved this subtheory consistent, and proved that each of the axioms of extensionality, replacement, and power set is independent of the four remaining axioms of this subtheory. If this subtheory is augmented with the axiom of infinity, each of the axioms of union, choice, and infinity is independent of the five remaining axioms. Because there are non-well-founded models that satisfy each axiom of ZFC except the axiom of regularity, that axiom is independent of the other ZFC axioms.
If consistent, ZFC cannot prove the existence of the inaccessible cardinals that category theory requires. Huge sets of this nature are possible if ZF is augmented with Tarski's axiom. Assuming that axiom turns the axioms of infinity, power set, and choice (7 – 9 above) into theorems.
Independence
Many important statements are independent of ZFC. The independence is usually proved by forcing, whereby it is shown that every countable transitive model of ZFC (sometimes augmented with large cardinal axioms) can be expanded to satisfy the statement in question. A different expansion is then shown to satisfy the negation of the statement. An independence proof by forcing automatically proves independence from arithmetical statements, other concrete statements, and large cardinal axioms. Some statements independent of ZFC can be proven to hold in particular inner models, such as in the constructible universe. However, some statements that are true about constructible sets are not consistent with hypothesized large cardinal axioms.
Forcing proves that the following statements are independent of ZFC:
- Axiom of constructibility (V=L) (which is also not a ZFC axiom)
- Continuum hypothesis
- Diamond principle
- Martin's axiom (which is not a ZFC axiom)
- Suslin hypothesis
Remarks:
- The consistency of V=L is provable by inner models but not forcing: every model of ZF can be trimmed to become a model of ZFC + V=L.
- The diamond principle implies the continuum hypothesis and the negation of the Suslin hypothesis.
- Martin's axiom plus the negation of the continuum hypothesis implies the Suslin hypothesis.
- The constructible universe satisfies the generalized continuum hypothesis, the diamond principle, Martin's axiom and the Kurepa hypothesis.
- The failure of the Kurepa hypothesis is equiconsistent with the existence of a strongly inaccessible cardinal.
A variation on the method of forcing can also be used to demonstrate the consistency and unprovability of the axiom of choice, i.e., that the axiom of choice is independent of ZF. The consistency of choice can be (relatively) easily verified by proving that the inner model L satisfies choice. (Thus every model of ZF contains a submodel of ZFC, so that Con(ZF) implies Con(ZFC).) Since forcing preserves choice, we cannot directly produce a model contradicting choice from a model satisfying choice. However, we can use forcing to create a model which contains a suitable submodel, namely one satisfying ZF but not C.
Another method of proving independence results, one owing nothing to forcing, is based on Gödel's second incompleteness theorem. This approach employs the statement whose independence is being examined, to prove the existence of a set model of ZFC, in which case Con(ZFC) is true. Since ZFC satisfies the conditions of Gödel's second theorem, the consistency of ZFC is unprovable in ZFC (provided that ZFC is, in fact, consistent). Hence no statement allowing such a proof can be proved in ZFC. This method can prove that the existence of large cardinals is not provable in ZFC, but cannot prove that assuming such cardinals, given ZFC, is free of contradiction.
Proposed additions
The project to unify set theorists behind additional axioms to resolve the continuum hypothesis or other meta-mathematical ambiguities is sometimes known as "Gödel's program". Mathematicians currently debate which axioms are the most plausible or "self-evident", which axioms are the most useful in various domains, and about to what degree usefulness should be traded off with plausibility; some "multiverse" set theorists argue that usefulness should be the sole ultimate criterion in which axioms to customarily adopt. One school of thought leans on expanding the "iterative" concept of a set to produce a set-theoretic universe with an interesting and complex but reasonably tractable structure by adopting forcing axioms; another school advocates for a tidier, less cluttered universe, perhaps focused on a "core" inner model.
Criticisms
ZFC has been criticized both for being excessively strong and for being excessively weak, as well as for its failure to capture objects such as proper classes and the universal set.
Many mathematical theorems can be proven in much weaker systems than ZFC, such as Peano arithmetic and second-order arithmetic (as explored by the program of reverse mathematics). Saunders Mac Lane and Solomon Feferman have both made this point. Some of "mainstream mathematics" (mathematics not directly connected with axiomatic set theory) is beyond Peano arithmetic and second-order arithmetic, but still, all such mathematics can be carried out in ZC (Zermelo set theory with choice), another theory weaker than ZFC. Much of the power of ZFC, including the axiom of regularity and the axiom schema of replacement, is included primarily to facilitate the study of the set theory itself.
On the other hand, among axiomatic set theories, ZFC is comparatively weak. Unlike New Foundations, ZFC does not admit the existence of a universal set. Hence the universe of sets under ZFC is not closed under the elementary operations of the algebra of sets. Unlike von Neumann–Bernays–Gödel set theory (NBG) and Morse–Kelley set theory (MK), ZFC does not admit the existence of proper classes. A further comparative weakness of ZFC is that the axiom of choice included in ZFC is weaker than the axiom of global choice included in NBG and MK.
There are numerous mathematical statements independent of ZFC. These include the continuum hypothesis, the Whitehead problem, and the normal Moore space conjecture. Some of these conjectures are provable with the addition of axioms such as Martin's axiom or large cardinal axioms to ZFC. Some others are decided in ZF+AD where AD is the axiom of determinacy, a strong supposition incompatible with choice. One attraction of large cardinal axioms is that they enable many results from ZF+AD to be established in ZFC adjoined by some large cardinal axiom. The Mizar system and metamath have adopted Tarski–Grothendieck set theory, an extension of ZFC, so that proofs involving Grothendieck universes (encountered in category theory and algebraic geometry) can be formalized.
See also
- Foundations of mathematics
- Inner model
- Large cardinal axiom
Related axiomatic set theories:
- Morse–Kelley set theory
- Von Neumann–Bernays–Gödel set theory
- Tarski–Grothendieck set theory
- Constructive set theory
- Internal set theory
Notes
- Ciesielski 1997, p. 4: "Zermelo-Fraenkel axioms (abbreviated as ZFC where C stands for the axiom of Choice)"
- Kunen 2007, p. 10
- Ebbinghaus 2007, p. 136.
- Halbeisen 2011, pp. 62–63.
- Fraenkel, Bar-Hillel & Lévy 1973
- Kunen 1980, p. 10.
- Hatcher 1982, p. 138, def. 1.
- Fraenkel, Bar-Hillel & Lévy 1973.
- Shoenfield 2001, p. 239.
- Shoenfield 1977, section 2.
- Hinman 2005, p. 467.
- For a complete argument that V satisfies ZFC see Shoenfield (1977).
- Link 2014
- Tarski 1939.
- Feferman 1996.
- Wolchover 2013.
Bibliography
- Abian, Alexander (1965). The Theory of Sets and Transfinite Arithmetic. W B Saunders.
- ———; LaMacchia, Samuel (1978). "On the Consistency and Independence of Some Set-Theoretical Axioms". Notre Dame Journal of Formal Logic. 19: 155–58. doi:10.1305/ndjfl/1093888220.
- Bernays, Paul; Fraenkel, A.A. (1958). Axiomatic Set Theory. Amsterdam: North Holland.
- Ciesielski, Krzysztof (1997). Set Theory for the Working Mathematician. Cambridge University Press. ISBN 0-521-59441-3.
- Devlin, Keith (1996) [First published 1984]. The Joy of Sets. Springer.
- Ebbinghaus, Heinz-Dieter (2007). Ernst Zermelo: An Approach to His Life and Work. Springer. ISBN 978-3-540-49551-2.
- Feferman, Solomon (1996). "Gödel's program for new axioms: why, where, how and what?". In Hájek, Petr (ed.). Gödel '96: Logical foundations of mathematics, computer science and physics–Kurt Gödel's legacy. Springer-Verlag. pp. 3–22. ISBN 3-540-61434-6..
- Fraenkel, Abraham; Bar-Hillel, Yehoshua; Lévy, Azriel (1973) [First published 1958]. Foundations of Set Theory. North-Holland. Fraenkel's final word on ZF and ZFC.
- Halbeisen, Lorenz J. (2011). Combinatorial Set Theory: With a Gentle Introduction to Forcing. Springer. pp. 62–63. ISBN 978-1-4471-2172-5.
- Hatcher, William (1982) [First published 1968]. The Logical Foundations of Mathematics. Pergamon Press.
- van Heijenoort, Jean (1967). From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931. Harvard University Press. Includes annotated English translations of the classic articles by Zermelo, Fraenkel, and Skolem bearing on ZFC.
- Hinman, Peter (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 978-1-56881-262-5.
- Jech, Thomas (2003). Set Theory: The Third Millennium Edition, Revised and Expanded. Springer. ISBN 3-540-44085-2.
- Kunen, Kenneth (1980). Set Theory: An Introduction to Independence Proofs. Elsevier. ISBN 0-444-86839-9.
- Kunen, Kenneth (29 October 2007). The Foundations of Mathematics (PDF). Archived (PDF) from the original on 7 September 2023.
- Levy, Azriel (2002). Basic Set Theory. Dover Publications. ISBN 048642079-5.
- Link, Godehard (2014). Formalism and Beyond: On the Nature of Mathematical Discourse. Walter de Gruyter GmbH & Co KG. ISBN 978-1-61451-829-7.
- Montague, Richard (1961). "Semantical closure and non-finite axiomatizability". Infinistic Methods. London: Pergamon Press. pp. 45–69.
- Quine, Willard van Orman (1969). Set Theory and Its Logic (Revised ed.). Cambridge, Massachusetts and London, England: The Belknap Press of Harvard University Press. ISBN 0-674-80207-1.
- Shoenfield, Joseph R. (1977). "Axioms of set theory". In Barwise, K. J. (ed.). Handbook of Mathematical Logic. North-Holland Publishing Company. ISBN 0-7204-2285-X.
- Shoenfield, Joseph R. (2001) [First published 1967]. Mathematical Logic (2nd ed.). A K Peters. ISBN 978-1-56881-135-2.
- Suppes, Patrick (1972) [First published 1960]. Axiomatic Set Theory. Dover reprint.
- Takeuti, Gaisi; Zaring, W M (1971). Introduction to Axiomatic Set Theory. Springer-Verlag.
- Takeuti, Gaisi; Zaring, W M (1982). Introduction to Axiomatic Set Theory. Springer. ISBN 9780387906836.
- Tarski, Alfred (1939). "On well-ordered subsets of any set". Fundamenta Mathematicae. 32: 176–83. doi:10.4064/fm-32-1-176-783.
- Tiles, Mary (1989). The Philosophy of Set Theory. Dover reprint.
- Tourlakis, George (2003). Lectures in Logic and Set Theory, Vol. 2. Cambridge University Press.
- Wolchover, Natalie (2013). "To Settle Infinity Dispute, a New Law of Logic". Quanta Magazine..
- Zermelo, Ernst (1908). "Untersuchungen über die Grundlagen der Mengenlehre I". Mathematische Annalen. 65 (2): 261–281. doi:10.1007/BF01449999. S2CID 120085563. English translation in Heijenoort, Jean van (1967). "Investigations in the foundations of set theory". From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931. Source Books in the History of the Sciences. Harvard University Press. pp. 199–215. ISBN 978-0-674-32449-7.
- Zermelo, Ernst (1930). "Über Grenzzahlen und Mengenbereiche". Fundamenta Mathematicae. 16: 29–47. doi:10.4064/fm-16-1-29-47. ISSN 0016-2736.
External links
- Axioms of set Theory - Lec 02 - Frederic Schuller on YouTube
- "ZFC", Encyclopedia of Mathematics, EMS Press, 2001 [1994]
- Stanford Encyclopedia of Philosophy articles by Joan Bagaria:
- Bagaria, Joan (31 January 2023). "Set Theory". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
- — (31 January 2023). "Axioms of Zermelo–Fraenkel Set Theory". In — (ed.). Stanford Encyclopedia of Philosophy.
- Metamath version of the ZFC axioms — A concise and nonredundant axiomatization. The background first order logic is defined especially to facilitate machine verification of proofs.
- A derivation in Metamath of a version of the separation schema from a version of the replacement schema.
- Weisstein, Eric W. "Zermelo-Fraenkel Set Theory". MathWorld.
This article includes a list of general references but it lacks sufficient corresponding inline citations Please help to improve this article by introducing more precise citations February 2024 Learn how and when to remove this message In set theory Zermelo Fraenkel set theory named after mathematicians Ernst Zermelo and Abraham Fraenkel is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as Russell s paradox Today Zermelo Fraenkel set theory with the historically controversial axiom of choice AC included is the standard form of axiomatic set theory and as such is the most common foundation of mathematics Zermelo Fraenkel set theory with the axiom of choice included is abbreviated ZFC where C stands for choice and ZF refers to the axioms of Zermelo Fraenkel set theory with the axiom of choice excluded Informally Zermelo Fraenkel set theory is intended to formalize a single primitive notion that of a hereditary well founded set so that all entities in the universe of discourse are such sets Thus the axioms of Zermelo Fraenkel set theory refer only to pure sets and prevent its models from containing urelements elements that are not themselves sets Furthermore proper classes collections of mathematical objects defined by a property shared by their members where the collections are too big to be sets can only be treated indirectly Specifically Zermelo Fraenkel set theory does not allow for the existence of a universal set a set containing all sets nor for unrestricted comprehension thereby avoiding Russell s paradox Von Neumann Bernays Godel set theory NBG is a commonly used conservative extension of Zermelo Fraenkel set theory that does allow explicit treatment of proper classes There are many equivalent formulations of the axioms of Zermelo Fraenkel set theory Most of the axioms state the existence of particular sets defined from other sets For example the axiom of pairing says that given any two sets a displaystyle a and b displaystyle b there is a new set a b displaystyle a b containing exactly a displaystyle a and b displaystyle b Other axioms describe properties of set membership A goal of the axioms is that each axiom should be true if interpreted as a statement about the collection of all sets in the von Neumann universe also known as the cumulative hierarchy The metamathematics of Zermelo Fraenkel set theory has been extensively studied Landmark results in this area established the logical independence of the axiom of choice from the remaining Zermelo Fraenkel axioms and of the continuum hypothesis from ZFC The consistency of a theory such as ZFC cannot be proved within the theory itself as shown by Godel s second incompleteness theorem HistoryThe modern study of set theory was initiated by Georg Cantor and Richard Dedekind in the 1870s However the discovery of paradoxes in naive set theory such as Russell s paradox led to the desire for a more rigorous form of set theory that was free of these paradoxes In 1908 Ernst Zermelo proposed the first axiomatic set theory Zermelo set theory However as first pointed out by Abraham Fraenkel in a 1921 letter to Zermelo this theory was incapable of proving the existence of certain sets and cardinal numbers whose existence was taken for granted by most set theorists of the time notably the cardinal number aleph omega ℵw displaystyle aleph omega and the set Z0 P Z0 P P Z0 P P P Z0 displaystyle Z 0 mathcal P Z 0 mathcal P mathcal P Z 0 mathcal P mathcal P mathcal P Z 0 where Z0 displaystyle Z 0 is any infinite set and P displaystyle mathcal P is the power set operation Moreover one of Zermelo s axioms invoked a concept that of a definite property whose operational meaning was not clear In 1922 Fraenkel and Thoralf Skolem independently proposed operationalizing a definite property as one that could be formulated as a well formed formula in a first order logic whose atomic formulas were limited to set membership and identity They also independently proposed replacing the axiom schema of specification with the axiom schema of replacement Appending this schema as well as the axiom of regularity first proposed by John von Neumann to Zermelo set theory yields the theory denoted by ZF Adding to ZF either the axiom of choice AC or a statement that is equivalent to it yields ZFC Formal languageFormally ZFC is a one sorted theory in first order logic The equality symbol can be treated as either a primitive logical symbol or a high level abbreviation for having exactly the same elements The former approach is the most common The signature has a single predicate symbol usually denoted displaystyle in which is a predicate symbol of arity 2 a binary relation symbol This symbol symbolizes a set membership relation For example the formula a b displaystyle a in b means that a displaystyle a is an element of the set b displaystyle b also read as a displaystyle a is a member of b displaystyle b There are different ways to formulate the formal language Some authors may choose a different set of connectives or quantifiers For example the logical connective NAND alone can encode the other connectives a property known as functional completeness This section attempts to strike a balance between simplicity and intuitiveness The language s alphabet consists of A countably infinite amount of variables used for representing sets The logical connectives displaystyle lnot displaystyle land displaystyle lor The quantifier symbols displaystyle forall displaystyle exists The equality symbol displaystyle The set membership symbol displaystyle in Brackets With this alphabet the recursive rules for forming well formed formulae wff are as follows Let x displaystyle x and y displaystyle y be metavariables for any variables These are the two ways to build atomic formulae the simplest wffs x y displaystyle x y x y displaystyle x in y Let ϕ displaystyle phi and ps displaystyle psi be metavariables for any wff and x displaystyle x be a metavariable for any variable These are valid wff constructions ϕ displaystyle lnot phi ϕ ps displaystyle phi land psi ϕ ps displaystyle phi lor psi xϕ displaystyle forall x phi xϕ displaystyle exists x phi A well formed formula can be thought as a syntax tree The leaf nodes are always atomic formulae Nodes displaystyle land and displaystyle lor have exactly two child nodes while nodes displaystyle lnot x displaystyle forall x and x displaystyle exists x have exactly one There are countably infinitely many wffs however each wff has a finite number of nodes AxiomsThere are many equivalent formulations of the ZFC axioms The following particular axiom set is from Kunen 1980 The axioms in order below are expressed in a mixture of first order logic and high level abbreviations Axioms 1 8 form ZF while the axiom 9 turns ZF into ZFC Following Kunen 1980 we use the equivalent well ordering theorem in place of the axiom of choice for axiom 9 All formulations of ZFC imply that at least one set exists Kunen includes an axiom that directly asserts the existence of a set although he notes that he does so only for emphasis Its omission here can be justified in two ways First in the standard semantics of first order logic in which ZFC is typically formalized the domain of discourse must be nonempty Hence it is a logical theorem of first order logic that something exists usually expressed as the assertion that something is identical to itself x x x displaystyle exists x x x Consequently it is a theorem of every first order theory that something exists However as noted above because in the intended semantics of ZFC there are only sets the interpretation of this logical theorem in the context of ZFC is that some set exists Hence there is no need for a separate axiom asserting that a set exists Second however even if ZFC is formulated in so called free logic in which it is not provable from logic alone that something exists the axiom of infinity asserts that an infinite set exists This implies that a set exists and so once again it is superfluous to include an axiom asserting as much Axiom of extensionality Two sets are equal are the same set if they have the same elements x y z z x z y x y displaystyle forall x forall y forall z z in x Leftrightarrow z in y Rightarrow x y The converse of this axiom follows from the substitution property of equality ZFC is constructed in first order logic Some formulations of first order logic include identity others do not If the variety of first order logic in which one is constructing set theory does not include equality displaystyle x y displaystyle x y may be defined as an abbreviation for the following formula z z x z y w x w y w displaystyle forall z z in x Leftrightarrow z in y land forall w x in w Leftrightarrow y in w In this case the axiom of extensionality can be reformulated as x y z z x z y w x w y w displaystyle forall x forall y forall z z in x Leftrightarrow z in y Rightarrow forall w x in w Leftrightarrow y in w which says that if x displaystyle x and y displaystyle y have the same elements then they belong to the same sets Axiom of regularity also called the axiom of foundation Every non empty set x displaystyle x contains a member y displaystyle y such that x displaystyle x and y displaystyle y are disjoint sets x a a x y y x z z y z x displaystyle forall x exists a a in x Rightarrow exists y y in x land lnot exists z z in y land z in x or in modern notation x x y y x y x displaystyle forall x x neq varnothing Rightarrow exists y y in x land y cap x varnothing This along with the axioms of pairing and union implies for example that no set is an element of itself and that every set has an ordinal rank Axiom schema of specification or of separation or of restricted comprehension Subsets are commonly constructed using set builder notation For example the even integers can be constructed as the subset of the integers Z displaystyle mathbb Z satisfying the congruence modulo predicate x 0 mod2 displaystyle x equiv 0 pmod 2 x Z x 0 mod2 displaystyle x in mathbb Z x equiv 0 pmod 2 In general the subset of a set z displaystyle z obeying a formula f x displaystyle varphi x with one free variable x displaystyle x may be written as x z f x displaystyle x in z varphi x The axiom schema of specification states that this subset always exists it is an axiom schema because there is one axiom for each f displaystyle varphi Formally let f displaystyle varphi be any formula in the language of ZFC with all free variables among x z w1 wn displaystyle x z w 1 ldots w n y displaystyle y is not free in f displaystyle varphi Then z w1 w2 wn y x x y x z f x w1 w2 wn z displaystyle forall z forall w 1 forall w 2 ldots forall w n exists y forall x x in y Leftrightarrow x in z land varphi x w 1 w 2 w n z Note that the axiom schema of specification can only construct subsets and does not allow the construction of entities of the more general form x f x displaystyle x varphi x This restriction is necessary to avoid Russell s paradox let y x x x displaystyle y x x notin x then y y y y displaystyle y in y Leftrightarrow y notin y and its variants that accompany naive set theory with unrestricted comprehension since under this restriction y displaystyle y only refers to sets within z displaystyle z that don t belong to themselves and y z displaystyle y in z has not been established even though y z displaystyle y subseteq z is the case so y displaystyle y stands in a separate position from which it can t refer to or comprehend itself therefore in a certain sense this axiom schema is saying that in order to build a y displaystyle y on the basis of a formula f x displaystyle varphi x we need to previously restrict the sets y displaystyle y will regard within a set z displaystyle z that leaves y displaystyle y outside so y displaystyle y can t refer to itself or in other words sets shouldn t refer to themselves In some other axiomatizations of ZF this axiom is redundant in that it follows from the axiom schema of replacement and the axiom of the empty set On the other hand the axiom schema of specification can be used to prove the existence of the empty set denoted displaystyle varnothing once at least one set is known to exist One way to do this is to use a property f displaystyle varphi which no set has For example if w displaystyle w is any existing set the empty set can be constructed as u w u u u u displaystyle varnothing u in w mid u in u land lnot u in u Thus the axiom of the empty set is implied by the nine axioms presented here The axiom of extensionality implies the empty set is unique does not depend on w displaystyle w It is common to make a definitional extension that adds the symbol displaystyle varnothing to the language of ZFC Axiom of pairing If x displaystyle x and y displaystyle y are sets then there exists a set which contains x displaystyle x and y displaystyle y as elements for example if x 1 2 and y 2 3 then z will be 1 2 2 3 x y z x z y z displaystyle forall x forall y exists z x in z land y in z The axiom schema of specification must be used to reduce this to a set with exactly these two elements The axiom of pairing is part of Z but is redundant in ZF because it follows from the axiom schema of replacement if we are given a set with at least two elements The existence of a set with at least two elements is assured by either the axiom of infinity or by the axiom schema of specification dubious discuss and the axiom of the power set applied twice to any set Axiom of union The union over the elements of a set exists For example the union over the elements of the set 1 2 2 3 displaystyle 1 2 2 3 is 1 2 3 displaystyle 1 2 3 The axiom of union states that for any set of sets F displaystyle mathcal F there is a set A displaystyle A containing every element that is a member of some member of F displaystyle mathcal F F A Y x x Y Y F x A displaystyle forall mathcal F exists A forall Y forall x x in Y land Y in mathcal F Rightarrow x in A Although this formula doesn t directly assert the existence of F displaystyle cup mathcal F the set F displaystyle cup mathcal F can be constructed from A displaystyle A in the above using the axiom schema of specification F x A Y x Y Y F displaystyle cup mathcal F x in A exists Y x in Y land Y in mathcal F Axiom schema of replacement The axiom schema of replacement asserts that the image of a set under any definable function will also fall inside a set Formally let f displaystyle varphi be any formula in the language of ZFC whose free variables are among x y A w1 wn displaystyle x y A w 1 dotsc w n so that in particular B displaystyle B is not free in f displaystyle varphi Then A w1 w2 wn x x A yf B x x A y y B f displaystyle forall A forall w 1 forall w 2 ldots forall w n bigl forall x x in A Rightarrow exists y varphi Rightarrow exists B forall x bigl x in A Rightarrow exists y y in B land varphi bigr bigr The unique existential quantifier displaystyle exists denotes the existence of exactly one element such that it follows a given statement In other words if the relation f displaystyle varphi represents a definable function f displaystyle f A displaystyle A represents its domain and f x displaystyle f x is a set for every x A displaystyle x in A then the range of f displaystyle f is a subset of some set B displaystyle B The form stated here in which B displaystyle B may be larger than strictly necessary is sometimes called the axiom schema of collection Axiom of infinity First several von Neumann ordinals 0 1 0 2 0 1 3 0 1 2 4 0 1 2 3 Let S w displaystyle S w abbreviate w w displaystyle w cup w where w displaystyle w is some set We can see that w displaystyle w is a valid set by applying the axiom of pairing with x y w displaystyle x y w so that the set z is w displaystyle w Then there exists a set X such that the empty set displaystyle varnothing defined axiomatically is a member of X and whenever a set y is a member of X then S y displaystyle S y is also a member of X X e z z e e X y y X S y X displaystyle exists X left exists e forall z neg z in e land e in X land forall y y in X Rightarrow S y in X right or in modern notation X X y y X S y X displaystyle exists X left varnothing in X land forall y y in X Rightarrow S y in X right More colloquially there exists a set X having infinitely many members It must be established however that these members are all different because if two elements are the same the sequence will loop around in a finite cycle of sets The axiom of regularity prevents this from happening The minimal set X satisfying the axiom of infinity is the von Neumann ordinal w which can also be thought of as the set of natural numbers N displaystyle mathbb N Axiom of power set By definition a set z displaystyle z is a subset of a set x displaystyle x if and only if every element of z displaystyle z is also an element of x displaystyle x z x q q z q x displaystyle z subseteq x Leftrightarrow forall q q in z Rightarrow q in x The Axiom of power set states that for any set x displaystyle x there is a set y displaystyle y that contains every subset of x displaystyle x x y z z x z y displaystyle forall x exists y forall z z subseteq x Rightarrow z in y The axiom schema of specification is then used to define the power set P x displaystyle mathcal P x as the subset of such a y displaystyle y containing the subsets of x displaystyle x exactly P x z y z x displaystyle mathcal P x z in y z subseteq x Axioms 1 8 define ZF Alternative forms of these axioms are often encountered some of which are listed in Jech 2003 Some ZF axiomatizations include an axiom asserting that the empty set exists The axioms of pairing union replacement and power set are often stated so that the members of the set x displaystyle x whose existence is being asserted are just those sets which the axiom asserts x displaystyle x must contain The following axiom is added to turn ZF into ZFC Axiom of well ordering choice The last axiom commonly known as the axiom of choice is presented here as a property about well orders as in Kunen 1980 For any set X displaystyle X there exists a binary relation R displaystyle R which well orders X displaystyle X This means R displaystyle R is a linear order on X displaystyle X such that every nonempty subset of X displaystyle X has a least element under the order R displaystyle R X R Rwell ordersX displaystyle forall X exists R R mbox well orders X Given axioms 1 8 many statements are provably equivalent to axiom 9 The most common of these goes as follows Let X displaystyle X be a set whose members are all nonempty Then there exists a function f displaystyle f from X displaystyle X to the union of the members of X displaystyle X called a choice function such that for all Y X displaystyle Y in X one has f Y Y displaystyle f Y in Y A third version of the axiom also equivalent is Zorn s lemma Since the existence of a choice function when X displaystyle X is a finite set is easily proved from axioms 1 8 AC only matters for certain infinite sets AC is characterized as nonconstructive because it asserts the existence of a choice function but says nothing about how this choice function is to be constructed Motivation via the cumulative hierarchyOne motivation for the ZFC axioms is the cumulative hierarchy of sets introduced by John von Neumann In this viewpoint the universe of set theory is built up in stages with one stage for each ordinal number At stage 0 there are no sets yet At each following stage a set is added to the universe if all of its elements have been added at previous stages Thus the empty set is added at stage 1 and the set containing the empty set is added at stage 2 The collection of all sets that are obtained in this way over all the stages is known as V The sets in V can be arranged into a hierarchy by assigning to each set the first stage at which that set was added to V It is provable that a set is in V if and only if the set is pure and well founded And V satisfies all the axioms of ZFC if the class of ordinals has appropriate reflection properties For example suppose that a set x is added at stage a which means that every element of x was added at a stage earlier than a Then every subset of x is also added at or before stage a because all elements of any subset of x were also added before stage a This means that any subset of x which the axiom of separation can construct is added at or before stage a and that the powerset of x will be added at the next stage after a The picture of the universe of sets stratified into the cumulative hierarchy is characteristic of ZFC and related axiomatic set theories such as Von Neumann Bernays Godel set theory often called NBG and Morse Kelley set theory The cumulative hierarchy is not compatible with other set theories such as New Foundations It is possible to change the definition of V so that at each stage instead of adding all the subsets of the union of the previous stages subsets are only added if they are definable in a certain sense This results in a more narrow hierarchy which gives the constructible universe L which also satisfies all the axioms of ZFC including the axiom of choice It is independent from the ZFC axioms whether V L Although the structure of L is more regular and well behaved than that of V few mathematicians argue that V L should be added to ZFC as an additional axiom of constructibility MetamathematicsVirtual classes Proper classes collections of mathematical objects defined by a property shared by their members which are too big to be sets can only be treated indirectly in ZF and thus ZFC An alternative to proper classes while staying within ZF and ZFC is the virtual class notational construct introduced by Quine 1969 where the entire construct y x Fx is simply defined as Fy This provides a simple notation for classes that can contain sets but need not themselves be sets while not committing to the ontology of classes because the notation can be syntactically converted to one that only uses sets Quine s approach built on the earlier approach of Bernays amp Fraenkel 1958 Virtual classes are also used in Levy 2002 Takeuti amp Zaring 1982 and in the Metamath implementation of ZFC Finite axiomatization The axiom schemata of replacement and separation each contain infinitely many instances Montague 1961 included a result first proved in his 1957 Ph D thesis if ZFC is consistent it is impossible to axiomatize ZFC using only finitely many axioms On the other hand von Neumann Bernays Godel set theory NBG can be finitely axiomatized The ontology of NBG includes proper classes as well as sets a set is any class that can be a member of another class NBG and ZFC are equivalent set theories in the sense that any theorem not mentioning classes and provable in one theory can be proved in the other Consistency Godel s second incompleteness theorem says that a recursively axiomatizable system that can interpret Robinson arithmetic can prove its own consistency only if it is inconsistent Moreover Robinson arithmetic can be interpreted in general set theory a small fragment of ZFC Hence the consistency of ZFC cannot be proved within ZFC itself unless it is actually inconsistent Thus to the extent that ZFC is identified with ordinary mathematics the consistency of ZFC cannot be demonstrated in ordinary mathematics The consistency of ZFC does follow from the existence of a weakly inaccessible cardinal which is unprovable in ZFC if ZFC is consistent Nevertheless it is deemed unlikely that ZFC harbors an unsuspected contradiction it is widely believed that if ZFC were inconsistent that fact would have been uncovered by now This much is certain ZFC is immune to the classic paradoxes of naive set theory Russell s paradox the Burali Forti paradox and Cantor s paradox Abian amp LaMacchia 1978 studied a subtheory of ZFC consisting of the axioms of extensionality union powerset replacement and choice Using models they proved this subtheory consistent and proved that each of the axioms of extensionality replacement and power set is independent of the four remaining axioms of this subtheory If this subtheory is augmented with the axiom of infinity each of the axioms of union choice and infinity is independent of the five remaining axioms Because there are non well founded models that satisfy each axiom of ZFC except the axiom of regularity that axiom is independent of the other ZFC axioms If consistent ZFC cannot prove the existence of the inaccessible cardinals that category theory requires Huge sets of this nature are possible if ZF is augmented with Tarski s axiom Assuming that axiom turns the axioms of infinity power set and choice 7 9 above into theorems Independence Many important statements are independent of ZFC The independence is usually proved by forcing whereby it is shown that every countable transitive model of ZFC sometimes augmented with large cardinal axioms can be expanded to satisfy the statement in question A different expansion is then shown to satisfy the negation of the statement An independence proof by forcing automatically proves independence from arithmetical statements other concrete statements and large cardinal axioms Some statements independent of ZFC can be proven to hold in particular inner models such as in the constructible universe However some statements that are true about constructible sets are not consistent with hypothesized large cardinal axioms Forcing proves that the following statements are independent of ZFC Axiom of constructibility V L which is also not a ZFC axiom Continuum hypothesis Diamond principle Martin s axiom which is not a ZFC axiom Suslin hypothesis Remarks The consistency of V L is provable by inner models but not forcing every model of ZF can be trimmed to become a model of ZFC V L The diamond principle implies the continuum hypothesis and the negation of the Suslin hypothesis Martin s axiom plus the negation of the continuum hypothesis implies the Suslin hypothesis The constructible universe satisfies the generalized continuum hypothesis the diamond principle Martin s axiom and the Kurepa hypothesis The failure of the Kurepa hypothesis is equiconsistent with the existence of a strongly inaccessible cardinal A variation on the method of forcing can also be used to demonstrate the consistency and unprovability of the axiom of choice i e that the axiom of choice is independent of ZF The consistency of choice can be relatively easily verified by proving that the inner model L satisfies choice Thus every model of ZF contains a submodel of ZFC so that Con ZF implies Con ZFC Since forcing preserves choice we cannot directly produce a model contradicting choice from a model satisfying choice However we can use forcing to create a model which contains a suitable submodel namely one satisfying ZF but not C Another method of proving independence results one owing nothing to forcing is based on Godel s second incompleteness theorem This approach employs the statement whose independence is being examined to prove the existence of a set model of ZFC in which case Con ZFC is true Since ZFC satisfies the conditions of Godel s second theorem the consistency of ZFC is unprovable in ZFC provided that ZFC is in fact consistent Hence no statement allowing such a proof can be proved in ZFC This method can prove that the existence of large cardinals is not provable in ZFC but cannot prove that assuming such cardinals given ZFC is free of contradiction Proposed additions The project to unify set theorists behind additional axioms to resolve the continuum hypothesis or other meta mathematical ambiguities is sometimes known as Godel s program Mathematicians currently debate which axioms are the most plausible or self evident which axioms are the most useful in various domains and about to what degree usefulness should be traded off with plausibility some multiverse set theorists argue that usefulness should be the sole ultimate criterion in which axioms to customarily adopt One school of thought leans on expanding the iterative concept of a set to produce a set theoretic universe with an interesting and complex but reasonably tractable structure by adopting forcing axioms another school advocates for a tidier less cluttered universe perhaps focused on a core inner model CriticismsZFC has been criticized both for being excessively strong and for being excessively weak as well as for its failure to capture objects such as proper classes and the universal set Many mathematical theorems can be proven in much weaker systems than ZFC such as Peano arithmetic and second order arithmetic as explored by the program of reverse mathematics Saunders Mac Lane and Solomon Feferman have both made this point Some of mainstream mathematics mathematics not directly connected with axiomatic set theory is beyond Peano arithmetic and second order arithmetic but still all such mathematics can be carried out in ZC Zermelo set theory with choice another theory weaker than ZFC Much of the power of ZFC including the axiom of regularity and the axiom schema of replacement is included primarily to facilitate the study of the set theory itself On the other hand among axiomatic set theories ZFC is comparatively weak Unlike New Foundations ZFC does not admit the existence of a universal set Hence the universe of sets under ZFC is not closed under the elementary operations of the algebra of sets Unlike von Neumann Bernays Godel set theory NBG and Morse Kelley set theory MK ZFC does not admit the existence of proper classes A further comparative weakness of ZFC is that the axiom of choice included in ZFC is weaker than the axiom of global choice included in NBG and MK There are numerous mathematical statements independent of ZFC These include the continuum hypothesis the Whitehead problem and the normal Moore space conjecture Some of these conjectures are provable with the addition of axioms such as Martin s axiom or large cardinal axioms to ZFC Some others are decided in ZF AD where AD is the axiom of determinacy a strong supposition incompatible with choice One attraction of large cardinal axioms is that they enable many results from ZF AD to be established in ZFC adjoined by some large cardinal axiom The Mizar system and metamath have adopted Tarski Grothendieck set theory an extension of ZFC so that proofs involving Grothendieck universes encountered in category theory and algebraic geometry can be formalized See alsoFoundations of mathematics Inner model Large cardinal axiom Related axiomatic set theories Morse Kelley set theory Von Neumann Bernays Godel set theory Tarski Grothendieck set theory Constructive set theory Internal set theoryNotesCiesielski 1997 p 4 Zermelo Fraenkel axioms abbreviated as ZFC where C stands for the axiom of Choice Kunen 2007 p 10 Ebbinghaus 2007 p 136 Halbeisen 2011 pp 62 63 Fraenkel Bar Hillel amp Levy 1973 Kunen 1980 p 10 Hatcher 1982 p 138 def 1 Fraenkel Bar Hillel amp Levy 1973 Shoenfield 2001 p 239 Shoenfield 1977 section 2 Hinman 2005 p 467 For a complete argument that V satisfies ZFC see Shoenfield 1977 Link 2014 Tarski 1939 Feferman 1996 Wolchover 2013 BibliographyAbian Alexander 1965 The Theory of Sets and Transfinite Arithmetic W B Saunders LaMacchia Samuel 1978 On the Consistency and Independence of Some Set Theoretical Axioms Notre Dame Journal of Formal Logic 19 155 58 doi 10 1305 ndjfl 1093888220 Bernays Paul Fraenkel A A 1958 Axiomatic Set Theory Amsterdam North Holland Ciesielski Krzysztof 1997 Set Theory for the Working Mathematician Cambridge University Press ISBN 0 521 59441 3 Devlin Keith 1996 First published 1984 The Joy of Sets Springer Ebbinghaus Heinz Dieter 2007 Ernst Zermelo An Approach to His Life and Work Springer ISBN 978 3 540 49551 2 Feferman Solomon 1996 Godel s program for new axioms why where how and what In Hajek Petr ed Godel 96 Logical foundations of mathematics computer science and physics Kurt Godel s legacy Springer Verlag pp 3 22 ISBN 3 540 61434 6 Fraenkel Abraham Bar Hillel Yehoshua Levy Azriel 1973 First published 1958 Foundations of Set Theory North Holland Fraenkel s final word on ZF and ZFC Halbeisen Lorenz J 2011 Combinatorial Set Theory With a Gentle Introduction to Forcing Springer pp 62 63 ISBN 978 1 4471 2172 5 Hatcher William 1982 First published 1968 The Logical Foundations of Mathematics Pergamon Press van Heijenoort Jean 1967 From Frege to Godel A Source Book in Mathematical Logic 1879 1931 Harvard University Press Includes annotated English translations of the classic articles by Zermelo Fraenkel and Skolem bearing on ZFC Hinman Peter 2005 Fundamentals of Mathematical Logic A K Peters ISBN 978 1 56881 262 5 Jech Thomas 2003 Set Theory The Third Millennium Edition Revised and Expanded Springer ISBN 3 540 44085 2 Kunen Kenneth 1980 Set Theory An Introduction to Independence Proofs Elsevier ISBN 0 444 86839 9 Kunen Kenneth 29 October 2007 The Foundations of Mathematics PDF Archived PDF from the original on 7 September 2023 Levy Azriel 2002 Basic Set Theory Dover Publications ISBN 048642079 5 Link Godehard 2014 Formalism and Beyond On the Nature of Mathematical Discourse Walter de Gruyter GmbH amp Co KG ISBN 978 1 61451 829 7 Montague Richard 1961 Semantical closure and non finite axiomatizability Infinistic Methods London Pergamon Press pp 45 69 Quine Willard van Orman 1969 Set Theory and Its Logic Revised ed Cambridge Massachusetts and London England The Belknap Press of Harvard University Press ISBN 0 674 80207 1 Shoenfield Joseph R 1977 Axioms of set theory In Barwise K J ed Handbook of Mathematical Logic North Holland Publishing Company ISBN 0 7204 2285 X Shoenfield Joseph R 2001 First published 1967 Mathematical Logic 2nd ed A K Peters ISBN 978 1 56881 135 2 Suppes Patrick 1972 First published 1960 Axiomatic Set Theory Dover reprint Takeuti Gaisi Zaring W M 1971 Introduction to Axiomatic Set Theory Springer Verlag Takeuti Gaisi Zaring W M 1982 Introduction to Axiomatic Set Theory Springer ISBN 9780387906836 Tarski Alfred 1939 On well ordered subsets of any set Fundamenta Mathematicae 32 176 83 doi 10 4064 fm 32 1 176 783 Tiles Mary 1989 The Philosophy of Set Theory Dover reprint Tourlakis George 2003 Lectures in Logic and Set Theory Vol 2 Cambridge University Press Wolchover Natalie 2013 To Settle Infinity Dispute a New Law of Logic Quanta Magazine Zermelo Ernst 1908 Untersuchungen uber die Grundlagen der Mengenlehre I Mathematische Annalen 65 2 261 281 doi 10 1007 BF01449999 S2CID 120085563 English translation in Heijenoort Jean van 1967 Investigations in the foundations of set theory From Frege to Godel A Source Book in Mathematical Logic 1879 1931 Source Books in the History of the Sciences Harvard University Press pp 199 215 ISBN 978 0 674 32449 7 Zermelo Ernst 1930 Uber Grenzzahlen und Mengenbereiche Fundamenta Mathematicae 16 29 47 doi 10 4064 fm 16 1 29 47 ISSN 0016 2736 External linksAxioms of set Theory Lec 02 Frederic Schuller on YouTube ZFC Encyclopedia of Mathematics EMS Press 2001 1994 Stanford Encyclopedia of Philosophy articles by Joan Bagaria Bagaria Joan 31 January 2023 Set Theory In Zalta Edward N ed Stanford Encyclopedia of Philosophy 31 January 2023 Axioms of Zermelo Fraenkel Set Theory In ed Stanford Encyclopedia of Philosophy Metamath version of the ZFC axioms A concise and nonredundant axiomatization The background first order logic is defined especially to facilitate machine verification of proofs A derivation in Metamath of a version of the separation schema from a version of the replacement schema Weisstein Eric W Zermelo Fraenkel Set Theory MathWorld