梦游ZFA仙境，遥想当年苦读

2017年10月11日夜间，我梦入ZFC公理集合论仙境，四处都是集合、集合的集合以及集合的集合的集合，……意境虚幻，仿若仙境，不忍离去。

10月12日中午，部分南京大学数学天文系57级老同学相约聚会南京大学（共计20人），遥想当年苦读情景。

现将ZFC公理集合论公理体系附在下面，供读者参考，有困难者，不必阅读。

袁萌  10月12日

ZFC公理体系（共计8条）：

1.Axiom of extensionality

∀ x ∀ y [ ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ x = y ] .

2.Axiom of regularity (also called the Axiom of foundation) 

∀ x [ ∃ a ( a ∈ x ) ⇒ ∃ y ( y ∈ x ∧ ¬ ∃ z ( z ∈ y ∧ z ∈ x ) ) ]

3.Axiom schema of specification (also called the axiom schema of separation or of restricted comprehension)  

{ x ∈ Z : x ≡ 0 ( mod 2 ) } .

4.Axiom of pairing 

∀ x ∀ y ∃ z ( x ∈ z ∧ y ∈ z ) .

5.Axiom of union

∀ F ∃ A ∀ Y ∀ x [ ( x ∈ Y ∧ Y ∈ F ) ⇒ x ∈ A ] .

6.Axiom schema of replacement

∀ A ∀ w 1 ∀ w 2 … ∀ w n [ ∀ x ( x ∈ A ⇒ ∃ ! y ϕ ) ⇒ ∃ B   ∀ x ( x ∈ A ⇒ ∃ y ( y ∈ B ∧ ϕ ) ) ] .

7. Axiom of infinity[edit]

∃ X [ ∅ ∈ X ∧ ∀ y ( y ∈ X ⇒ S ( y ) ∈ X ) ] .

8. Axiom of power set

( z ⊆ x ) ⇔ ( ∀ q ( q ∈ z ⇒ q ∈ x ) ) .

9. Well-ordering theorem  

∀ X ∃ R ( R well-orders X ) .

（全文完）

附：ZFC公理体系：

There are many equivalent formulations of the ZFC axioms; for a discussion of this see Fraenkel, Bar-Hillel & Lévy 1973. The following par Kunen ticular axiom set is from  (1980)

articular

axiom set is from Kunen (1980). The axioms per se are expressed in the symbolism of first order logic. The associated English prose is only intended to aid the intuition.

All formulations of ZFC imply that at least one set exists. Kunen includes an axiom that directly asserts the existence of a set, in addition to the axioms given below (although he notes that he does so only “for emphasis”).^[3] 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 identica

                  axiom that directly asserts the existence of a set, in addition to the axioms given below (although he notes that he does so only “for emphasis”).^[3] 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). 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 (below) 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.

1. Axiom of extensionality[edit]

Main article: 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. If the background logic does not include equality "=", x=y may be defined as an abbreviation for the following formula:^[4]

∀ 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 and y have the same elements, then they belong to the same sets.^[5]

2. Axiom of regularity (also called the Axiom of foundation)[edit]

Main article: Axiom of regularity

Every non-empty set x contains a member y such that x and 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))].} ^[6]

This implies, for example, that no set is an element of itself and that every set has an ordinal rank.

3. Axiom schema of specification (also called the axiom schema of separation or of restricted comprehension)[edit]

Main article: Axiom schema of specification

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 ( mod 2 ) {\displaystyle x\equiv 0{\pmod {2}}} :

{ x ∈ Z : x ≡ 0 ( mod 2 ) } .

 

{\displaystyle \{x\in \mathbb {Z} :x\equiv 0{\pmod {2}}\}.}

In general, the subset of a set z obeying a formula ϕ {\displaystyle \phi } (x) with one free variable x may be written as:

{ x ∈ z : ϕ ( x ) } . {\displaystyle \{x\in z:\phi (x)\}.}

The axiom schema of specification states that this subset always exists (it is an axiom schema because there is one axiom for each ϕ {\displaystyle \phi } ). Formally, let ϕ{\displaystyle \phi } be any formula in the language of ZFC with all free variables among x , z , w 1 , … , w n {\displaystyle x,z,w_{1},\ldots ,w_{n}} (y is not free in ϕ {\displaystyle \phi } ). Then:

∀ z ∀ w 1 ∀ w 2 … ∀ w n ∃ y ∀ x [ x ∈ y ⇔ ( x ∈ 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 \phi )].}

Note that the axiom schema of specification can only construct subsets, and does not allow the construction of sets of the more general form:

{ x : ϕ ( x ) } . {\displaystyle \{x:\phi (x)\}.}

This restriction is necessary to avoid Russell's paradox and its variants that accompany naive set theory with unrestricted comprehension.

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 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 (see above). One way to do this is to use a property ϕ{\displaystyle \phi } which no set has. For example, if 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). It is common to make a definitional extension that adds the symbol ∅ {\displaystyle \varnothing } to the language of ZFC.

4. Axiom of pairing[edit]

Main article: Axiom of pairing

If x and y are sets, then there exists a set which contains x and y as elements.

∀ 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 and the axiom of the power set applied twice to any set.

5. Axiom of union[edit]

Main article: 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\}} .

Formally, 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].}

While this doesn't directly assert the existence of ∪ F {\displaystyle \cup {\mathcal {F}}} , it 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 image of the domain set A under the definable function f (i.e. the range of f) falls inside a set B.

6. Axiom schema of replacement[edit]

Main article: 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 ϕ {\displaystyle \phi } be any formula in the language of ZFC whose free variables are among x , y , A , w 1 , … , w n {\displaystyle x,y,A,w_{1},\dotsc ,w_{n}} , so that in particular B {\displaystyle B} is not free in ϕ{\displaystyle \phi } . Then:

∀ A ∀ w 1 ∀ w 2 … ∀ w n [ ∀ x ( x ∈ A ⇒ ∃ ! y ϕ ) ⇒ ∃ B   ∀ x ( x ∈ A ⇒ ∃ y ( y ∈ B ∧ ϕ ) ) ] .

 

{\displaystyle \forall A\forall w_{1}\forall w_{2}\ldots \forall w_{n}{\bigl [}\forall x(x\in A\Rightarrow \exists !y\,\phi )\Rightarrow \exists B\ \forall x{\bigl (}x\in A\Rightarrow \exists y(y\in B\land \phi ){\bigr )}{\bigr ]}.}

In other words, if the relation ϕ {\displaystyle \phi } 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.

7. Axiom of infinity[edit]

Main article: Axiom of infinity

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 {\displaystyle z} is { w } {\displaystyle \{w\}} ). Then there exists a set X such that the empty set ∅ {\displaystyle \varnothing } 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 [ ∅ ∈ 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 ω, which can also be thought of as the set of natural numbers N {\displaystyle \mathbb {N} } .

8. Axiom of power set[edit]

Main article: Axiom of power set

By definition a set z is a subset of a set x if and only if every element of z is also an element of 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, there is a set y that contains every subset of 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) as the subset of such a y containing the subsets of x exactly:

P ( x ) = { z ∈ y : z ⊆ x } {\displaystyle 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 whose existence is being asserted are just those sets which the axiom asserts x must contain.

The following axiom is added to turn ZF into ZFC:

9. Well-ordering theorem[edit]

Main article: Well-ordering theorem

For any set X, there is a binary relation R which well-orders X. This means R is a linear order on X such that every nonempty subset of X has a member which is minimal under R.

∀ X ∃ R ( R well-orders X ) .

 

{\displaystyle \forall X\exists R(R\;{\mbox{well-orders}}\;X).}

Given axioms 1–8, there are many statements provably equivalent to axiom 9, the best known of which is the axiom of choice (AC), which goes as follows. Let X be a set whose members are all non-empty. Then there exists a function f from X to the union of the members of X, called a "choice function", such that for all Y ∈ X one has f(Y) ∈ Y. Since the existence of a choice function when 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 set but says nothing about how the choice set is to be "constructed." Much research has sought to characterize the definability (or lack thereof) of certain sets whose existence AC asserts.

Motivation via the cumulative hierarchy[edit]

One motivation for the ZFC axioms is the cumulative hierarchy of sets introduced by John von Neumann.^[7] 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.^[8] 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 provable that 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 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 stage α, and that the powerset of x will be added at the next stage after α. For a complete argument that V satisfies ZFC see Shoenfield (1977).

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.

Metamathematics[edit]

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.

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.^[9] Assuming that axiom turns the axioms of infinity, power set, and choice (7 − 9 above) into theorems.

Independence[edit]

Many important statements are independent of ZFC (see list of statements undecidable in 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:

• Continuum hypothesis
• Diamond principle
• Suslin hypothesis
• Martin's axiom (which is not a ZFC axiom)
• Axiom of Constructibility (V=L) (which is also not a ZFC axiom).

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.