nLab two-sorted set theory

Redirected from "element reflection".
Two-sorted set theory

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Two-sorted set theory

Overview

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. 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.

In contrast to unsorted set theory, there is no global equality predicate in a two-sorted set theory. Instead, there are separate equality predicates for sets and elements, whereby it is meaningful to ask, given any two elements, whether those two elements are equal, and likewise, given any two set, whether those two sets are equal. Additionally, a set’s identity here is determined by its elements, in other words the axiom of weak extensionality holds for the membership relation with respect to the equality relation of sets.

Two-sorted set theories come in both material set theory and structural set theory flavors. For example, ZFC, ZFA, and New Foundations are could all be presented as two-sorted material set theories, while ETCS can be presented as a two-sorted structural set theory.

Notions of sets and elements

We work in a two-sorted first order theory, where SS represents the type of probable sets, and EE represents the type of probable elements. Then,

Definition

A notion of set and element in a two-sorted first-order theory with sorts SS and EE consists of:

  • A binary predicate in SS, ()= S()(-)=_S(-), called equality of sets

  • A binary predicate in EE, ()= E()(-)=_E(-), called equality of elements

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

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

  • A binary predicate in EE on the left and SS on the right, ()()(-)\in(-), called membership

such that

  • ()= E()(-)=_E(-) is an equivalence relation

  • if aba \in b, then aa is an element and bb is a set

a:E.b:S.(ab)element(a)set(b)\forall a:E.\forall b:S.(a \in b) \to \mathrm{element}(a) \wedge \mathrm{set}(b)
  • weak extensionality for sets and elements: for all a:Sa:S and for all b:Sb:S, if a and b are sets, then a= Sba =_S b if and only if, for all c:Ec:E, if cc is an element, then cac \in a if and only if cbc \in b
a:S.b:S.(set(a)set(b))((a= Sb)c:E.(element(c)((ca)(cb))))\forall a:S.\forall b:S.(\mathrm{set}(a) \wedge \mathrm{set}(b)) \implies ((a =_S b) \iff \forall c:E.(\mathrm{element}(c) \implies ((c \in a) \iff (c \in b))))

Element reflection and set reflection

In two-sorted set theories, sets are not literally elements. Instead, to represent that sets are elements and vice versa, one could add reflection rules and axioms to the set theory, which say that for every set, there is a corresponding element, and vice versa.

In two-sorted set theory, element reflection is the statement that for all sets AA, there is an element asElem(A)\mathrm{asElem}(A), or equivalently, that there is a function asElem:SE\mathrm{asElem}:S \to E in the set theory. Similarly, set reflection is the statement that for all elements aa, there is a set asSet(A)\mathrm{asSet}(A), or equivalently, that there is a function asSet:ES\mathrm{asSet}:E \to S in the set theory.

For any two-sorted set theory with element reflection, it is possible to define a membership relation on the elements alone which behaves like a global membership relation in unsorted set theory, as follows

a EAA:S.A= EasElem(A)aAa \in_E A \coloneqq \exists A':S.A =_E \mathrm{asElem}(A') \wedge a \in A'

Similarly, for any two-sorted set theory with set reflection, it is possible to define a membership relation on the sets alone which behaves like a global membership relation in unsorted set theory, as follows

a SAa:E.a= SasSet(a)aAa \in_S A \coloneqq \exists a':E.a =_S \mathrm{asSet}(a') \wedge a' \in A

Examples

Pure set theories

A two-sorted set theory with element reflection and set reflection is a pure set theory if set(A)\mathrm{set}(A) and element(a)\mathrm{element}(a) are both \top for all A:SA:S and a:Ea:E, and set and element reflection are inverses of each other: asElem(asSet(A))= SA\mathrm{asElem}(\mathrm{asSet}(A)) =_S A and asElem(asSet(a))= Ea\mathrm{asElem}(\mathrm{asSet}(a)) =_E a. The induced membership relations E\in_E and S\in_S both behave as the global membership relation in an unsorted set theory, so one could work entirely in EE or in SS.

Set theories with urelements

A two-sorted set theory with element reflection is a material set theory with urelements if set(A)\mathrm{set}(A) and element(a)\mathrm{element}(a) are both \top for all A:SA:S and a:Ea:E, and element reflection is an injection, A= SBA =_S B only if asElem(A)= EasElem(B)\mathrm{asElem}(A) =_E \mathrm{asElem}(B). The atoms or urelements are the elements which are not contained in the image of asElem\mathrm{asElem}. The induced membership relation E\in_E behaves as the global membership relation in an unsorted set theory, so one could work entirely in EE.

Categorical set theories

There are also two-sorted categorical set theories, such as the presentation of ETCS. In ETCS, there are two types, a set SetSet and a set FuncFunc representing sets and functions respectively, with functions dom:FuncSet\mathrm{dom}:Func \to Set and codom:FuncSet\mathrm{codom}:Func \to Set representing the domain and codomain of the function. (there might be a fiberwise set-truncation necessary in this definition) There is a set 1:Set1:Set representing the singleton, the terminal object in SetSet. set(A)\mathrm{set}(A) is true for all A:SetA:Set, but element(a)\mathrm{element}(a) is only true for those functions whose source is the singleton terminal object dom(a)= Set1\mathrm{dom}(a) =_{Set} 1. We define the membership relation aAa \in A to be

aAelement(a)set(A)codom(a)=Aa \in A \coloneqq \mathrm{element}(a) \wedge \mathrm{set}(A) \wedge \mathrm{codom}(a) = A

Furthermore, there are multiple possible functions which could act as element reflections in categorical set theories, three of which are

  • the identity functions of sets AA, asElem(A)id(A)\mathrm{asElem}(A) \coloneqq \mathrm{id}(A)

  • the unique function into the singleton and out of AA, due to the universal property of the singleton, asElem(A)u(A)\mathrm{asElem}(A) \coloneqq u(A), where codom(u(A))=1\mathrm{codom}(u(A)) = 1 and dom(u(A))=A\mathrm{dom}(u(A)) = A

  • the unique function out of the empty set into AA, due to the universal property of the empty set, asElem(A)v(A)\mathrm{asElem}(A) \coloneqq v(A), where dom(v(A))=\mathrm{dom}(v(A)) = \emptyset and codom(v(A))=A\mathrm{codom}(v(A)) = A

This in turn induces the following definitions of sets in FuncFunc itself:

  • 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)).

and the following definitions of membership relations on FuncFunc itself:

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

    a Funcbelement(a)set(b)codom(a)=ba \in_{Func} 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

    a Funcbelement(a)set(b)codom(a)=dom(b)a \in_{Func} 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

    a Funcbelement(a)set(b)codom(a)=codom(b)a \in_{Func} b \coloneqq \mathrm{element}(a) \wedge \mathrm{set}'(b) \wedge \mathrm{codom}(a) = \mathrm{codom}(b)

For the first two membership relations Func\in_{Func}, the identity morphism of the singleton 11 is a Quine atom, and any identity morphism of 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 14:45:36. See the history of this page for a list of all contributions to it.