basic constructions:
strong axioms
further
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 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 , is required to be a probable element and 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.
We work in a two-sorted first order theory, where represents the type of probable sets, and represents the type of probable elements. Then,
A notion of set and element in a two-sorted first-order theory with sorts and consists of:
A binary predicate in , , called equality of sets
A binary predicate in , , called equality of elements
A unary predicate in , , called being a set
A unary predicate in , , called being an element
A binary predicate in on the left and on the right, , called membership
such that
is an equivalence relation
if , then is an element and is a set
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 , there is an element , or equivalently, that there is a function in the set theory. Similarly, set reflection is the statement that for all elements , there is a set , or equivalently, that there is a function 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
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 two-sorted set theory with element reflection and set reflection is a pure set theory if and are both for all and , and set and element reflection are inverses of each other: and . The induced membership relations and both behave as the global membership relation in an unsorted set theory, so one could work entirely in or in .
A two-sorted set theory with element reflection is a material set theory with urelements if and are both for all and , and element reflection is an injection, only if . The atoms or urelements are the elements which are not contained in the image of . The induced membership relation behaves as the global membership relation in an unsorted set theory, so one could work entirely in .
There are also two-sorted categorical set theories, such as the presentation of ETCS. In ETCS, there are two types, a set and a set representing sets and functions respectively, with functions and representing the domain and codomain of the function. (there might be a fiberwise set-truncation necessary in this definition) There is a set representing the singleton, the terminal object in . is true for all , but is only true for those functions whose source is the singleton terminal object . We define the membership relation to be
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 ,
the unique function into the singleton and out of , due to the universal property of the singleton, , where and
the unique function out of the empty set into , due to the universal property of the empty set, , where and
This in turn induces the following definitions of sets in itself:
sets as identity functions or
sets as functions out of the empty set ().
and the following definitions of membership relations on itself:
for sets as identity functions, the membership relation is defined as
for sets as functions into the singleton, the membership relation is defined as
for sets as functions out of the empty set, the membership relation is defined as
For the first two membership relations , the identity morphism of the singleton is a Quine atom, and any identity morphism of any set in bijection with 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.
Last revised on November 17, 2022 at 14:45:36. See the history of this page for a list of all contributions to it.