axiom of infinity




In the foundations of mathematics, the axiom of infinity asserts that infinite sets exist. Infinite sets cannot be constructed from finite sets, so their existence must be posited as an extra axiom. Further axioms in this vein which assert the existence of even larger sets that cannot be constructed from smaller ones are called large cardinal axioms.


One common form of the axiom of infinity says that the particular set NN of natural numbers exists. In material set theory this often takes the form of asserting that the von Neumann ordinal number ω\omega exists, where ω\omega is characterized as the smallest set such that ω\emptyset\in\omega and whenever aωa\in \omega then a{a}ωa\cup \{a\}\in \omega. In structural set theory the usual form of the axiom of infinity is the existence of a natural numbers object.

In the form of an NNO, the axiom of infinity generalises to the existence of inductive types or W-types. These can be constructed from a NNO if power sets exist, but in predicative theories they can be added as additional axioms.


Broadly speaking, finite mathematics is mathematics that does not use or need the axiom of infinity; a finitist is an extreme breed of constructivist that believes that mathematics is better without the axiom of infinity, or even that this axiom is false.

A more extreme case is to deny the axiom of infinity with an axiom of finiteness: every set is finite. There is one of these for every definition of ‘finite’ given on that page; here is the strongest stated directly in terms of set theory as an axiom of induction:

  • Any property of sets that is invariant under isomorphism and holds for the empty set must hold for all sets if, whenever it holds for a set XX, it holds for the disjoint union X{*}X \uplus \{*\}.

In material set theory, this is equivalent given the axiom of foundation (which guarantees that XX and {X}\{X\} are disjoint):

  • Any property of sets that holds for the empty set must hold for all sets if, whenever it holds for a set XX, it holds for the union X{X}X \cup \{X\}.

Last revised on July 9, 2014 at 06:25:03. See the history of this page for a list of all contributions to it.