The modern study of set theory was initiated by Georg Cantor and Richard Dedekind in the 1870s.
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 (
[3] 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.
Adding to ZF either the axiom of choice (AC) or a statement that is equivalent to it yields ZFC.
Kunen includes an axiom that directly asserts the existence of a set, although he notes that he does so only "for emphasis".
First, in the standard semantics of first-order logic in which ZFC is typically formalized, the domain of discourse must be nonempty.
If the variety of first-order logic in which one is constructing set theory does not include equality "
) and its variants that accompany naive set theory with unrestricted comprehension (since under this restriction
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 other hand, the axiom schema of specification can be used to prove the existence of the empty set, denoted
(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.
Some ZF axiomatizations include an axiom asserting that the empty set exists.
One motivation for the ZFC axioms is the cumulative hierarchy of sets introduced by John von Neumann.
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.
Virtual classes are also used in Levy (2002), Takeuti & Zaring (1982), and in the Metamath implementation of ZFC.
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.
Abian & LaMacchia (1978) studied a subtheory of ZFC consisting of the axioms of extensionality, union, powerset, replacement, and choice.
If consistent, ZFC cannot prove the existence of the inaccessible cardinals that category theory requires.
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.
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: Remarks: 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.
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.
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".
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.
These include the continuum hypothesis, the Whitehead problem, and the normal Moore space conjecture.
Some others are decided in ZF+AD where AD is the axiom of determinacy, a strong supposition incompatible with choice.