Knowlpedia

ZFC axioms

Standard axioms of set theory: Zermelo-Fraenkel axioms plus the Axiom of Choice.

ZFC is the classical first-order theory of with equality and membership ∈\in, governed by the following axioms and axiom schemas. Variables range over sets. The logical connectives and quantifiers use .

Axioms
  1. Extensionality: ∀x∀y[∀z(z∈x⇔z∈y)⇒x=y]\forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow x=y].
  2. Empty set: ∃e∀z (z∉e)\exists e\forall z\,(z\notin e). Extensionality makes this object unique; write it as ∅\varnothing.
  3. Pairing: ∀a∀b∃c∀z[z∈c⇔(z=a∨z=b)]\forall a\forall b\exists c\forall z[z\in c\Leftrightarrow(z=a\lor z=b)]. Write this set as {a,b}\{a,b\}, with {a}={a,a}\{a\}=\{a,a\}.
  4. Union: ∀a∃u∀z[z∈u⇔∃x(x∈a∧z∈x)]\forall a\exists u\forall z[z\in u\Leftrightarrow\exists x(x\in a\land z\in x)].
  5. Power set: ∀a∃p∀z[z∈p⇔∀w(w∈z⇒w∈a)]\forall a\exists p\forall z[z\in p\Leftrightarrow\forall w(w\in z\Rightarrow w\in a)].
  6. Infinity: there is a set II with ∅∈I\varnothing\in I such that x∈Ix\in I implies x∪{x}∈Ix\cup\{x\}\in I. Here x∪{x}x\cup\{x\} abbreviates the set whose elements are the elements of xx, together with xx itself; pairing and union provide it.
  7. Separation schema: for each first-order formula ϕ(z,p)\phi(z,\mathbf p), with the new variable bb not free in ϕ\phi, every set aa and every choice of parameter sets p\mathbf p satisfy
∃b∀z[z∈b⇔(z∈a∧ϕ(z,p))].\exists b\forall z[z\in b\Leftrightarrow(z\in a\land\phi(z,\mathbf p))].
  1. Replacement schema: for each formula ϕ(x,y,p)\phi(x,y,\mathbf p), if for every x∈ax\in a exactly one yy satisfies ϕ(x,y,p)\phi(x,y,\mathbf p), then there is a set bb with
∀y[y∈b⇔∃x(x∈a∧ϕ(x,y,p))].\forall y[y\in b\Leftrightarrow\exists x(x\in a\land\phi(x,y,\mathbf p))].

All parameter choices are quantified; bound variables are chosen to avoid capture.

  1. Foundation: every nonempty set aa has an element xx sharing no element with aa:
∀a[∃y(y∈a)⇒∃x(x∈a∧¬∃z(z∈x∧z∈a))].\forall a[\exists y(y\in a)\Rightarrow \exists x(x\in a\land\neg\exists z(z\in x\land z\in a))].
  1. Choice: for every set AA of pairwise disjoint nonempty sets, there is a set CC meeting each member of AA in exactly one element. In membership notation the conclusion is
∀x∈A ∃u [u∈x∧u∈C∧∀v((v∈x∧v∈C)⇒v=u)].\forall x\in A\ \exists u\,[u\in x\land u\in C\land \forall v((v\in x\land v\in C)\Rightarrow v=u)].

This choice-set form is equivalent, over the other axioms, to the usual choice-function form of the . Bounded quantifiers such as ∀x∈A\forall x\in A are abbreviations using implication and membership.

Scope

Separation permits selecting elements from an existing set; it is not unrestricted comprehension. Replacement asserts that a definable single-valued image of a set is a set. The axioms allow constructions such as natural numbers and ordered pairs; those constructions are consequences and explanations, not prerequisites of the axiom statements themselves.

References