nLab
size issues
Context
Foundations
foundations

The basis of it all
mathematical logic

deduction system , natural deduction , sequent calculus , lambda-calculus , judgment

type theory , simple type theory , dependent type theory

collection , object , type , term , set , element

equality , judgmental equality , typal equality

universe , size issues

higher-order logic

Set theory
Foundational axioms
Removing axioms
Contents
Overview
There are various ways to deal with size issues in the foundations of mathematics . All of them involve the notion of universe in one way or another.

In set theory , one usually either uses Grothendieck universes , or some internal model of set theory or class theory , whether well-pointed Heyting categories , well-pointed division allegories , sets with extensional well-founded transitive relations, categories with class structure , et cetera.

In class theory , the notion of universe is already in the theory via the universal class , which is by definition a class universe .

In dependent type theory , one uses univalent Russell universes or Tarski universes , which are basically internal models of dependent type theory .

In any case, given a universe $U$ , we say that a collection is $U$ -small if it is in $U$ , a collection is $U$ -large if it is not in $U$ , any subcollection of $U$ is a class , and a subcollection of $U$ is a proper class if it is not a singleton subcollection of $U$ .

See also
Last revised on November 19, 2022 at 17:04:00.
See the history of this page for a list of all contributions to it.