Universe (mathematics)

${\displaystyle V_{i}:=\bigcup _{j<i}\mathbf {P} V_{j}\!}$

defines V_i for any ordinal number i. The union of all of the V_i is the von Neumann universe V:

${\displaystyle V:=\bigcup _{i}V_{i}\!}$.

Every individual V_i is a set, but their union V is a

Kurt Gödel's constructible universe L and the axiom of constructibility

Inaccessible cardinals yield models of ZF and sometimes additional axioms, and are equivalent to the existence of the Grothendieck universe set

In predicate calculus

In an interpretation of first-order logic, the universe (or domain of discourse) is the set of individuals (individual constants) over which the quantifiers range. A proposition such as ∀x (x² ≠ 2) is ambiguous, if no domain of discourse has been identified. In one interpretation, the domain of discourse could be the set of real numbers; in another interpretation, it could be the set of natural numbers. If the domain of discourse is the set of real numbers, the proposition is false, with x = √2 as counterexample; if the domain is the set of naturals, the proposition is true, since 2 is not the square of any natural number.

In category theory

There is another approach to universes which is historically connected with category theory. This is the idea of a Grothendieck universe. Roughly speaking, a Grothendieck universe is a set inside which all the usual operations of set theory can be performed. This version of a universe is defined to be any set for which the following axioms hold:^[1]

1. ${\displaystyle x\in u\in U}$ implies ${\displaystyle x\in U}$
2. ${\displaystyle u\in U}$ and ${\displaystyle v\in U}$ imply {u,v}, (u,v), and ${\displaystyle u\times v\in U}$.
3. ${\displaystyle x\in U}$ implies ${\displaystyle {\mathcal {P}}x\in U}$ and ${\displaystyle \cup x\in U}$
4. ${\displaystyle \omega \in U}$ (here ${\displaystyle \omega =\{0,1,2,...\}}$ is the set of all finite ordinals.)
5. if ${\displaystyle f:a\to b}$ is a surjective function with ${\displaystyle a\in U}$ and ${\displaystyle b\subset U}$, then ${\displaystyle b\in U}$.

The most common use of a Grothendieck universe U is to take U as a replacement for the category of all sets. One says that a set S is U-small if S ∈U, and U-large otherwise. The category U-Set of all U-small sets has as objects all U-small sets and as morphisms all functions between these sets. Both the object set and the morphism set are sets, so it becomes possible to discuss the category of "all" sets without invoking proper classes. Then it becomes possible to define other categories in terms of this new category. For example, the category of all U-small categories is the category of all categories whose object set and whose morphism set are in U. Then the usual arguments of set theory are applicable to the category of all categories, and one does not have to worry about accidentally talking about proper classes. Because Grothendieck universes are extremely large, this suffices in almost all applications.

Often when working with Grothendieck universes, mathematicians assume the Axiom of Universes: "For any set x, there exists a universe U such that x ∈U." The point of this axiom is that any set one encounters is then U-small for some U, so any argument done in a general Grothendieck universe can be applied.^[2] This axiom is closely related to the existence of strongly inaccessible cardinals.

In type theory

In some type theories, especially in systems with dependent types, types themselves can be regarded as terms. There is a type called the universe (often denoted ${\displaystyle {\mathcal {U}}}$) which has types as its elements. To avoid paradoxes such as Girard's paradox (an analogue of Russell's paradox for type theory), type theories are often equipped with a countably infinite hierarchy of such universes, with each universe being a term of the next one.

There are at least two kinds of universes that one can consider in type theory: Russell-style universes (named after Bertrand Russell) and Tarski-style universes (named after Alfred Tarski).^[3][4][5] A Russell-style universe is a type whose terms are types.^[3] A Tarski-style universe is a type together with an interpretation operation allowing us to regard its terms as types.^[3]

For example:^[6]

The openendedness of

Martin-Löf’s informal semantics of meaning explanation. This act of ‘introspection’ is an attempt to become aware of the conceptions which have governed our constructions in the past. It gives rise to a “reflection principle

which roughly speaking says whatever we are used to doing with types can be done inside a universe” (Martin-Löf 1975, 83). On the formal level, this leads to an extension of the existing formalization of type theory in that the type forming capacities of C become enshrined in a type universe U_C mirroring C.

• Domain of discourse
• Grothendieck universe
• Herbrand universe
• Free object
• Open formula
• Space (mathematics)

Notes