In material set theory, the axiom of extensionality says that the global membership relation is an extensional relation on the class of all pure sets.
Since any relation becomes extensional on its extensional quotient, one can interpret this axiom as a definition of equality. However, because the extensional quotient map need not reflect the relation, there is still content to the axiom: if two sets would be identified in the extensional quotient, then they must be members of the same sets and have the same sets as members.
If one models pure sets in structural set theory, then this property may be made to hold by construction.
In any unsorted set theory, the axiom of weak extensionality states that given a set and a set , if and only if for all , if and only if .
If the set theory does not have equality as a primitive, we could define equality as the predicate
The axiom of weak extensionality is a foundational axiom in most material set theories, such as Zermelo set theory and Mac Lane set theory, both which do not have the axiom of foundation, as well as ZFC which does have the axiom of foundation.
In fully formal ETCS, where the basic objects of the theory are functions, represents both the empty set and the identity function on the empty set, and represents the singleton, the identity function of the singleton, and the sole element of the singleton all at the same time, there are three possible notions of sets:
as identity functions or
as functions from the empty set
The elements are functions with domain ,
When sets are defined as functions into the singleton, the membership relation is defined by the function being an element, the function being a set, and the codomain of being
Weak extensionality is a theorem in this case. By the universal property of the singleton, any two sets and with the same domain are equal to each other, which means that any proposition between and implies that , and thus that implies that . The converse follows from indiscernibility of identicals.
In any two-sorted set theory, the axiom of weak extensionality states that given a set and a set , if and only if for all , if and only if .
If the set theory does not have equality of sets as a primitive, we could define equality of sets as the predicate
Let be a bisimulation, a binary relation such that for all sets and such that , the following conditions hold:
The axiom of strong extensionality states that for every bisimulation and for every set and , implies that .
If the set theory does not have equality as a primitive, we could define equality as the terminal bisimulation, as the bisimulation such that for every bisimulation and for every set and , implies that .
In any set theory with the axiom of foundation, the axiom of weak extensionality implies the axiom of strong extensionality.
In any structural set theory, the axiom of strong extensionality states that for all sets and with an injection , the two definitions of being a bijection are logically equivalent to each other:
Similar to how in material set theory one can use the axiom of extensionality to define equality of sets, in structural set theory one can use the axiom of strong extensionality to define bijection of sets.
In dependent type theory, it is possible to define a Tarski universe of pure sets which behaves as a material set theory. The universal type family of the Tarski universe is given by the type family . The axiom of extensionality is given by the following inference rule:
For power sets, the axiom of extensionality is a property of power sets, and states that given a type and subtypes and , there is an equivalence of types between the identity type and the dependent function type , where is the type of all propositions and is the local membership relation between elements and subtypes . The axiom of extensionality holds in the dependent type theory if and only if function extensionality holds.
Michael Shulman, Comparing material and structural set theories (arXiv:1808.05204)
Håkon Robbestad Gylterud, Elisabeth Bonnevier, Non-wellfounded sets in HoTT (arXiv:2001.06696)
Last revised on February 28, 2024 at 02:57:04. See the history of this page for a list of all contributions to it.