# Infinity, axiom of

An axiom of a formal theory or of a theory with an interpretation (thematic theory) which ensures the presence of infinite objects in the theory. Thus, the axiom of infinity in some system of axiomatic set theory ensures the existence of an infinite set. For instance, in the language of the axiomatic Zermelo–Fraenkel system, the axiom of infinity is usually written as follows:

$$\exists X(\emptyset\in X\&\forall Z(Z\in X\supset Z\cup\{Z\}\in X))$$

(i.e. there exists a set $X$ such that $\emptyset\in X$ and for any $Z$ which belongs to $X$, the set $Z\cup\{Z\}$ also belongs to $X$).

In the simple theory of types (cf. Types, theory of), another formulation of the axiom of infinity is accepted, in view of the specific limitations on the language of the theory: There exists a relation which defines a total order without a last element on the set of individuals. In many theories it is convenient to use the so-called Dedekind axiom of infinity: There exists a set which can be mapped one-to-one into one of its proper subsets. With the aid of the axiom of choice it is easily shown that Dedekind's axiom of infinity is equivalent to the other above-mentioned forms of the axiom of infinity. It is known, however, that this equivalence cannot be proved by usual set-theoretic means without the use of the axiom of choice.

In set theory the so-called axioms of higher infinity, which postulate the existence of sets of high cardinality, are employed as well: The axiom on the existence of an inaccessible cardinal, the axiom on the existence of a measurable cardinal, etc.

In predicate logic, formulas which are only valid in an infinite model are called axioms of infinity. From the point of view of proof theory such formulas usually state less than the axiom of infinity in axiomatic set theory: They ensure that there are infinitely many objects, but may not ensure the existence of an infinite object of study. It has been shown that there exists an infinite number of pairwise non-equivalent axioms of infinity of predicate logic.