Editing Zermelo–Fraenkel set theory (section)

== 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 {{harvtxt|Quine|1969}}, where the entire construct ''y'' &isin; { ''x'' | F''x'' } is simply defined as F''y''.<ref>{{harvnb|Link|2014}}</ref> 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 {{harvtxt|Bernays|Fraenkel|1958}}.  Virtual classes are also used in {{harvtxt|Levy|2002}}, {{harvtxt|Takeuti|Zaring|1982}}, and in the [[Metamath]] implementation of ZFC.

===Finite axiomatization===
{{Main|Von Neumann–Bernays–Gödel set theory}}

The axiom schemata of replacement and separation each contain infinitely many instances. {{harvtxt|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 [[class (set theory)|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 proof|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{{snd}}ZFC is immune to the classic paradoxes of [[naive set theory]]: [[Russell's paradox]], the [[Burali-Forti paradox]], and [[Cantor's paradox]].

{{harvtxt|Abian|LaMacchia|1978}} studied a [[subtheory]] of ZFC consisting of the axioms of extensionality, union, powerset, replacement, and choice. Using [[model theory|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 cardinal]]s that [[category theory]] requires. Huge sets of this nature are possible if ZF is augmented with [[Tarski–Grothendieck set theory|Tarski's axiom]].{{sfn|Tarski|1939}} Assuming that axiom turns the axioms of [[axiom of infinity|infinity]], [[axiom of power set|power set]], and [[axiom of choice|choice]] (''7''&thinsp;–&thinsp;''9'' above) into theorems.

=== Independence ===
Many important statements are [[Logical independence|independent]] [[list of statements independent of ZFC|of ZFC]]. The independence is usually proved by [[forcing (mathematics)|forcing]], whereby it is shown that every countable transitive [[model theory|model]] of ZFC (sometimes augmented with [[large cardinal axiom]]s) 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 model]]s, 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|Axiom of constructibility (V=L)]] (which is also not a ZFC axiom)
* [[Continuum hypothesis]]
* [[Diamondsuit|Diamond principle]]
* [[Martin's axiom]] (which is not a ZFC axiom)
* [[Suslin's problem|Suslin hypothesis]]

Remarks:

* The consistency of V=L is provable by [[inner model]]s 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|generalized continuum hypothesis]], the diamond principle, Martin's axiom and the Kurepa hypothesis.
* The failure of the [[Kurepa tree|Kurepa hypothesis]] is equiconsistent with the existence of a [[strongly inaccessible cardinal]].

A variation on the method of [[forcing (mathematics)|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".{{sfn|Feferman|1996}} 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 theory)|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.{{sfn|Wolchover|2013}}