Inmathematics, and particularly inset theory,category theory,type theory, and thefoundations of mathematics, auniverse is a collection that contains all the entities one wishes to consider in a given situation.
In set theory, universes are oftenclasses that contain (aselements) all sets for which one hopes toprove a particulartheorem. These classes can serve asinner models for various axiomatic systems such asZFC orMorse–Kelley set theory. Universes are of critical importance to formalizing concepts incategory theory inside set-theoretical foundations. For instance, thecanonical motivating example of a category isSet, the category of all sets, which cannot be formalized in a set theory without some notion of a universe.
In type theory, a universe is a type whose elements are types.
Perhaps the simplest version is thatany set can be a universe, so long as the object of study is confined to that particular set. If the object of study is formed by thereal numbers, then thereal lineR, which is the real number set, could be the universe under consideration. Implicitly, this is the universe thatGeorg Cantor was using when he first developed modernnaive set theory andcardinality in the 1870s and 1880s in applications toreal analysis. The only sets that Cantor was originally interested in weresubsets ofR.
This concept of a universe is reflected in the use ofVenn diagrams. In a Venn diagram, the action traditionally takes place inside a large rectangle that represents the universeU. One generally says that sets are represented by circles; but these sets can only be subsets ofU. Thecomplement of a setA is then given by that portion of the rectangle outside ofA's circle. Strictly speaking, this is therelative complementU \A ofA relative toU; but in a context whereU is the universe, it can be regarded as theabsolute complementAC ofA. Similarly, there is a notion of thenullary intersection, that is theintersection ofzero sets (meaning no sets, notnull sets).
Without a universe, the nullary intersection would be the set of absolutely everything, which is generally regarded as impossible; but with the universe in mind, the nullary intersection can be treated as the set of everything under consideration, which is simplyU. These conventions are quite useful in the algebraic approach to basic set theory, based onBoolean lattices. Except in some non-standard forms ofaxiomatic set theory (such asNew Foundations), theclass of all sets is not a Boolean lattice (it is only arelatively complemented lattice).
In contrast, the class of all subsets ofU, called thepower set ofU, is a Boolean lattice. The absolute complement described above is the complement operation in the Boolean lattice; andU, as the nullary intersection, serves as thetop element (or nullarymeet) in the Boolean lattice. ThenDe Morgan's laws, which deal with complements of meets andjoins (which areunions in set theory) apply, and apply even to the nullary meet and the nullary join (which is theempty set).
However, once subsets of a given setX (in Cantor's case,X =R) are considered, the universe may need to be a set of subsets ofX. (For example, atopology onX is a set of subsets ofX.) The various sets of subsets ofX will not themselves be subsets ofX but will instead be subsets ofPX, thepower set ofX. This may be continued; the object of study may next consist of such sets of subsets ofX, and so on, in which case the universe will beP(PX). In another direction, thebinary relations onX (subsets of theCartesian productX ×X) may be considered, orfunctions fromX to itself, requiring universes likeP(X ×X) orXX.
Thus, even if the primary interest isX, the universe may need to be considerably larger thanX. Following the above ideas, one may want thesuperstructure overX as the universe. This can be defined bystructural recursion as follows:
Then the superstructure overX, writtenSX, is the union ofS0X,S1X,S2X, and so on; or
No matter what setX is the starting point, theempty set {} will belong toS1X. The empty set is thevon Neumann ordinal [0].Then {[0]}, the set whose only element is the empty set, will belong toS2X; this is the von Neumann ordinal [1]. Similarly, {[1]} will belong toS3X, and thus so will {[0],[1]}, as the union of {[0]} and {[1]}; this is the von Neumann ordinal [2]. Continuing this process, everynatural number is represented in the superstructure by its von Neumann ordinal. Next, ifx andy belong to the superstructure, then so does {{x},{x,y}}, which represents theordered pair (x,y). Thus the superstructure will contain the various desired Cartesian products. Then the superstructure also containsfunctions andrelations, since these may be represented as subsets of Cartesian products. The process also gives orderedn-tuples, represented as functions whose domain is the von Neumann ordinal [n], and so on.
So if the starting point is justX = {}, a great deal of the sets needed for mathematics appear as elements of the superstructure over {}. But each of the elements ofS{} will be afinite set. Each of the natural numbers belongs to it, but the setN ofall natural numbers does not (although it is asubset ofS{}). In fact, the superstructure over {} consists of all of thehereditarily finite sets. As such, it can be considered theuniverse offinitist mathematics. Speaking anachronistically, one could suggest that the 19th-century finitistLeopold Kronecker was working in this universe; he believed that each natural number existed but that the setN (a "completed infinity") did not.
However,S{} is unsatisfactory for ordinary mathematicians (who are not finitists), because even thoughN may be available as a subset ofS{}, still the power set ofN is not. In particular, arbitrary sets of real numbers are not available. So it may be necessary to start the process all over again and formS(S{}). However, to keep things simple, one can take the setN of natural numbers as given and formSN, the superstructure overN. This is often considered theuniverse ofordinary mathematics. The idea is that all of the mathematics that is ordinarily studied refers to elements of this universe. For example, any of the usualconstructions of the real numbers (say byDedekind cuts) belongs toSN. Evennon-standard analysis can be done in the superstructure over anon-standard model of the natural numbers.
There is a slight shift in philosophy from the previous section, where the universe was any setU of interest. There, the sets being studied weresubsets of the universe; now, they aremembers of the universe. Thus althoughP(SX) is a Boolean lattice, what is relevant is thatSX itself is not. Consequently, it is rare to apply the notions of Boolean lattices and Venn diagrams directly to the superstructure universe as they were to the power-set universes of the previous section. Instead, one can work with the individual Boolean latticesPA, whereA is any relevant set belonging toSX; thenPA is a subset ofSX (and in fact belongs toSX). In Cantor's caseX =R in particular, arbitrary sets of real numbers are not available, so there it may indeed be necessary to start the process all over again.
It is possible to give a precise meaning to the claim thatSN is the universe of ordinary mathematics; it is amodel ofZermelo set theory, theaxiomatic set theory originally developed byErnst Zermelo in 1908. Zermelo set theory was successful precisely because it was capable of axiomatising "ordinary" mathematics, fulfilling the programme begun by Cantor over 30 years earlier. But Zermelo set theory proved insufficient for the further development of axiomatic set theory and other work in thefoundations of mathematics, especiallymodel theory.
For a dramatic example, the description of the superstructure process above cannot itself be carried out in Zermelo set theory. The final step, formingS as an infinitary union, requires theaxiom of replacement, which was added to Zermelo set theory in 1922 to formZermelo–Fraenkel set theory, the set of axioms most widely accepted today. So while ordinary mathematics may be doneinSN, discussionofSN goes beyond the "ordinary", intometamathematics.
But if high-powered set theory is brought in, the superstructure process above reveals itself to be merely the beginning of atransfinite recursion.Going back toX = {}, the empty set, and introducing the (standard) notationVi forSi{},V0 = {},V1 =P{}, and so on as before. But what used to be called "superstructure" is now just the next item on the list:Vω, where ω is the firstinfiniteordinal number. This can be extended to arbitraryordinal numbers:
definesVi forany ordinal numberi.The union of all of theVi is thevon Neumann universeV:
Every individualVi is a set, but their unionV is aproper class. Theaxiom of foundation, which was added toZF set theory at around the same time as the axiom of replacement, says thatevery set belongs toV.
In aninterpretation offirst-order logic, the universe (or domain of discourse) is the set of individuals (individual constants) over which thequantifiers range. A proposition such as∀x (x2 ≠ 2) is ambiguous, if no domain of discourse has been identified. In one interpretation, the domain of discourse could be the set ofreal numbers; in another interpretation, it could be the set ofnatural numbers. If the domain of discourse is the set of real numbers, the proposition is false, withx =√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.
There is another approach to universes which is historically connected withcategory theory. This is the idea of aGrothendieck 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]
The most common use of a Grothendieck universeU is to takeU as a replacement for the category of all sets. One says that a setS isU-small ifS ∈U, andU-large otherwise. The categoryU-Set of allU-small sets has as objects allU-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 allU-small categories is the category of all categories whose object set and whose morphism set are inU. 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 theAxiom of Universes: "For any setx, there exists a universeU such thatx ∈U." The point of this axiom is that any set one encounters is thenU-small for someU, so any argument done in a general Grothendieck universe can be applied.[2] This axiom is closely related to the existence ofstrongly inaccessible cardinals.
In some type theories, especially in systems withdependent types, types themselves can be regarded asterms. There is a type called the universe (often denoted) which has types as its elements. To avoid paradoxes such asGirard's paradox (an analogue ofRussell's paradox for type theory), type theories are often equipped with acountably 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 afterBertrand Russell) andTarski-style universes (named afterAlfred 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 ofMartin-Löf type theory is particularly manifest in the introduction of so-called universes. Type universes encapsulate the informal notion of reflection whose role may be explained as follows. During the course of developing a particular formalization of type theory, the type theorist may look back over the rules for types, say C, which have been introduced hitherto and perform the step of recognizing that they are valid according toMartin-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 UC mirroring C.