nLab unsorted set theory

Unsorted set theory




The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

Unsorted set theory


There are a number of ways to present a set theory; one of the most basic decisions when it comes to presenting a set theory is whether the probable sets and probable elements should be regarded as the same kind of objects, as in unsorted set theory, or as fundamentally different objects, as in two-sorted set theory or three-sorted set theory. In the former, there is a global membership relation \in which is defined on the entire domain of discourse. In the latter, there are two domains of discourse, one representing the probable sets and the other representing the probable elements or atoms, and for the membership relation aba \in b, aa is required to be a probable element and bb is required to be a probable set.

Furthermore, in an unsorted set theory, there is also a global equality predicate, whereby it is meaningful to ask, given any two objects, whether those two objects are equal. Additionally, a set’s identity here is determined by its elements, in other words the axiom of weak extensionality holds for the global membership relation with respect to the equality relation.

Unsorted set theories come in both material set theory and structural set theory flavors. For example, ZFC, ZFA, and New Foundations are unsorted material set theories, while fully formal ETCS is an unsorted structural set theory.

Notions of sets and elements

First of all, in order to give a definition pertaining to all unsorted set theories, we need to know: what is a set theory? Probably no theory can intrinsically be called a set theory; it is only given that distinction by our intent to regard some of its objects of study as “sets” and others as their “elements.” Thus we make the following definition.


A notion of set and element in a unsorted first-order theory consists of:

  • A binary predicate ()=()(-)=(-) called equality

  • A unary predicate set()\mathrm{set}(-) called being a set

  • A unary predicate element()\mathrm{element}(-) called being an element

  • A binary predicate ()()(-)\in(-) called membership

such that

  • if aba \in b, then aa is an element and bb is a set
a.b.(ab)element(a)set(b)\forall a.\forall b.(a \in b) \to \mathrm{element}(a) \wedge \mathrm{set}(b)
  • weak extensionality for sets and elements: for all aa and for all bb, if a and b are sets, then a=ba = b if and only if, for all cc, if cc is an element, then cac \in a if and only if cbc \in b
a.b.(set(a)set(b))((a=b)c.(element(c)((ca)(cb))))\forall a.\forall b.(\mathrm{set}(a) \wedge \mathrm{set}(b)) \implies ((a = b) \iff \forall c.(\mathrm{element}(c) \implies ((c \in a) \iff (c \in b))))


Pure set theories

In pure set theories, such as ZFC and New Foundations, set(a)\mathrm{set}(a) and element(a)\mathrm{element}(a) is \top for all objects aa, \in is the primitive membership relation and == is defined through the axiom of extensionality.

Set theories with urelements

In set theories with urelements, such as ZFA, only element(a)\mathrm{element}(a) is \top for all objects aa, \in is the primitive membership relation, set\mathrm{set} is the primitive sethood predicate, and == is defined through the axiom of extensionality.

Categorical set theories

In an unsorted categorical set theory, such as Todd Trimble‘s fully formal ETCS, == is a primitive, and there is a specified symbol 11 representing the identity morphism of the terminal object and a specified symbol 00 representing the identity morphism of the initial object, as well as ss and tt representing the identity morphisms of the source and target. The elements are functions with domain 11, element(a)(dom(a)=1)\mathrm{element}(a) \coloneqq (\mathrm{dom}(a) = 1) There are many possible notions of sets, three of which include:

  • sets as identity functions set(a)dom(a)=a\mathrm{set}(a) \coloneqq \mathrm{dom}(a) = a or set(a)codom(a)=a\mathrm{set}(a) \coloneqq \mathrm{codom}(a) = a

  • sets as functions into the singleton set(a)(codom(a)=1)\mathrm{set}(a) \coloneqq (\mathrm{codom}(a) = 1)

  • sets as functions out of the empty set (set(a)(dom(a)=0)\mathrm{set}(a) \coloneqq (\mathrm{dom}(a) = 0)).

Thus, there are many different definitions of the membership relation \in, which for the above notions of set are:

  • for sets as identity functions, the membership relation is defined as

    abelement(a)set(b)codom(a)=ba \in b \coloneqq \mathrm{element}(a) \wedge \mathrm{set}(b) \wedge \mathrm{codom}(a) = b
  • for sets as functions into the singleton, the membership relation is defined as

    abelement(a)set(b)codom(a)=dom(b)a \in b \coloneqq \mathrm{element}(a) \wedge \mathrm{set}(b) \wedge \mathrm{codom}(a) = \mathrm{dom}(b)
  • for sets as functions out of the empty set, the membership relation is defined as

    abelement(a)set(b)codom(a)=codom(b)a \in b \coloneqq \mathrm{element}(a) \wedge \mathrm{set}(b) \wedge \mathrm{codom}(a) = \mathrm{codom}(b)

For the first two membership relations \in, the singleton 11 is a Quine atom, and any set in bijection with 11 is a Quine atom. For the third membership relation, there are no Quine atoms. While all the membership relations defined above are weakly extensional relations, all three membership relations defined above could be proven not to be strongly extensional relations, which means that the axiom of foundation fails in any of the three unsorted presentations of categorical set theory.

Allegorical set theories

See also

Last revised on November 17, 2022 at 15:15:35. See the history of this page for a list of all contributions to it.