nLab
universe

This entry is about the notion in mathematics/logic/type theory. For the notion of the same name in physics see at observable universe.


Context

Universes

Foundations

Contents

Idea

A universe is a realm within which (some conceived part, naively and virtually all, of) mathematics may be thought of as taking place. Universes can be purely metamathematical, but we can also reflect upon them and bring them into mathematics. There are several different kinds of ‘universes’. For a physical notion of universe see observable universe.

Categories as universes

Much of ordinary mathematics can be thought of as taking place inside “the archetypical category SET of sets”. Typically, the properties of SETSET are formulated in first-order logic using a set theory such as ZFC or (more directly) ETCS.

We can generalise this from SETSET to any other category CC. Without further assumptions on the category, there is in general very little mathematics that can be formulated inside it, but a few extra properties and structures are usually sufficient to provide something interesting. This is the general topic of internalisation. The attitude to take is that any specific category is merely one model, while a general class of categories is a theory (really a doctrine, or 2-theory?).

We can also use higher categories instead of mere categories here. Even for ordinary mathematics, this means starting with \infty-GRPD instead of SETSET.

Universes of pure sets

The idea of the large category SETSET as the universe of mathematics has an analogue in pre-category-theoretic material set theory. The von Neumann universe VV is the proper class of all well-founded pure sets.

More explicitly: for every ordinal number α\alpha, we have a set V αV_\alpha (the von Neumann universe of rank α\alpha), defined recursively using the operations of power set and (material) union as

V α β<α𝒫V β. V_\alpha \coloneqq \bigcup_{\beta \lt \alpha} \mathcal{P}V_\beta .

Then VV itself is the union of all of the V αV_\alpha.

A similar but more complicated definition allows us to define the universe LL of constructible sets, called the constructible universe.

See also a Wikipedia article written largely by Toby Bartels in another lifetime.

Universes inside SETSET

If set theory is the foundation of mathematics, then the universes above are part of metamathematics rather than mathematics itself. However, we can also look for small categories or sets that exist within set theory and have the properties of a universe.

There is already a hint of this in the hierarchy V αV_\alpha out of which the von Neumann universe is built. For some values of α\alpha, V αV_\alpha might be a sufficiently large and complete collection of sets in which to do ordinary mathematics. From the nPOV, we can instead look at the category Set αSet_\alpha of these sets and the functions between them, although it's more common to think about Set κSet_\kappa for some cardinal number κ\kappa.

An infinite set is a simple example, as finite mathematics can be done inside it. Going beyond this, a Grothendieck universe is a set within which other infinite sets exist but which is complete under the operations of material set theory that are needed for ordinary mathematics. The structural analogue is a universe in the topos SETSET.

In general, we need some axioms to state the existence of such universes; we can think of these as large cardinal axioms. (The existence of an infinite set is the axiom of infinity; the existence of a Grothendieck universe is the existence of an inaccessible cardinal.)

The use of such universes is convenient when we want to work with large categories “as if they were small.” That is, if we redefine “small” to mean “element of some fixed universe,” then the categories of all small structures of some sort will still be sets (rather than proper classes) in the bigger ambient universe, and thus we can for instance form functor categories between them freely. We do sometimes then need a way to “move a category” from one universe to another; see universe enlargement.

Reflection

In logic, we use reflection principle?s (see Wikipedia) to systematically identify features of our meta-universe and see what is needed to prove the existence of an internal universe with these features.

This follows the following outline:

  1. We assume that we understand a priori what it means to use first-order logic (or some other finitary base logic).

  2. Using this base logic, we can formulate a foundational set theory that describes a meta-universe such as SETSET.

  3. Of course, SETSET cannot be described from inside itself. But there may be objects in SETSET (internal categories) that look like SETSET itself.

  4. We add an additional axiom to our set theory stating that such objects, the internal universes, exist. These are then models of our original set theory.

  5. Now we are using a new, stronger set theory; repeat.

Universes in type theory

Set theory is not the only foundation of mathematics. For example, there are also various foundational type theories?, closely related to structural set theory. Then we have a meta-universe of all types, and we can also add axioms for the existence of internal universes.

References

General

(…)

In type theory

Revised on April 14, 2014 06:32:34 by Urs Schreiber (88.128.80.70)