nLab empty set

Redirected from "axiom of the empty set".
Contents

Contents

Definition

The empty set \emptyset is the set with no elements.

The empty set is unique in most membership-based foundations, but in any case we can say ‘the’ empty set, since any two empty sets are isomorphic by a unique isomorphism (the generalized the).

Indeed, in any foundations (whether membership-based or structural), the empty set is characterized by a universal property: it is the initial object in the category Set of all sets: for every set SS, there is a unique function

!S. \emptyset \stackrel{\exists !}{\to} S \,.

Properties

The empty set can be confusing, because it is a degenerate case. Indeed, it is defined as an exception: every set is inhabited, except the empty set. Nothing belongs to the empty set, but the empty set itself is something. Mathematics students are confused that there is a function from the empty set to itself, and even grown mathematicians will misstate definitions because they forget about the empty set.

In terms of the empty set one can give sense to the natural number expression 0 00^0, the exponentiation of zero with itself, by defining the exponential m nm^n to be the cardinality of the hom-set hom Set([n],[m])\hom_{Set}([n], [m]) where [m][m] is an mm-element set. Then 0 0=10^0 = 1 because \emptyset is an initial object.

Remark

Endless debates (as seen for example at sci.math) about the meaning of 0 00^0 are most easily resolved by paying attention to how exponentiation (in a ring or rig that admits exponentiation) is defined. We have just observed how 0 0=10^0 = 1 makes good sense in the rig of natural numbers. But exponentiation for the real number field (x yx^y for x>0x \gt 0) is standardly defined by continuity considerations, and cannot be continuously extended to cover 0 00^0. Of course, that has nothing to do with the empty set!

Foundational status

Material set theory

In set theory as a foundation of mathematics, the existence of the empty set is often taken as an axiom, the axiom of the null set. Actually, this axiom can be written in such a simple way that the name seems unmotivated:

Axiom (null set)

There exists a set.

However, one can then use the axiom of separation (bounded separation is enough) to prove that there exists an empty set, and then use the axiom of extensionality to prove that this empty set is unique.

In some axiomatic frameworks, even this is unnecessary; while it makes little sense from the standpoint of categorial logic, it was once traditional to take x,P[x]x,P[x]\forall x,\; P[x] \;\Rightarrow\; \exists x,\; P[x] as an axiom (or theorem) of first-order logic. It is then automatic that something exists, and if one uses a material set theory of pure sets, then this something must be a set.

Alternatively, since the axiom of infinity states the existence of a set (and is often phrased to state explicitly the existence of an empty set), then the axiom of the null set becomes unnecessary for another reason.

 Dependent type theory

In dependent type theory, it is possible to define a Tarski universe (V,)(V, \in) of pure sets which behaves as a material set theory. The universal type family of the Tarski universe is given by the type family x:V y:Vyxx:V \vdash \sum_{y:V} y \in x. The axiom of the null set is given by the following inference rule:

ΓctxΓnullset V: :V x:V¬(x)\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{nullset}_V:\sum_{\emptyset:V} \prod_{x:V} \neg (x \in \emptyset)}

Last revised on February 28, 2024 at 03:33:18. See the history of this page for a list of all contributions to it.