nLab axiom of extensionality

Redirected from "axiom of strong extensionality".
The axiom of extensionality

The axiom of extensionality

Idea

In material set theory, the axiom of extensionality says that the global membership relation \in 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.

Statements

Weak extensionality

In unsorted set theories

In any unsorted set theory, the axiom of weak extensionality states that given a set AA and a set BB, A=BA = B if and only if for all CC, CAC \in A if and only if CBC \in B.

If the set theory does not have equality as a primitive, we could define equality as the predicate

A=BC.(CA)(CB)A = B \coloneqq \forall C.(C \in A) \iff (C \in B)

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, 00 represents both the empty set and the identity function on the empty set, and 11 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 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

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

  • as functions from the empty set set(a)(dom(a)=0)\mathrm{set}(a) \coloneqq (\mathrm{dom}(a) = 0)

The elements are functions with domain 11, element(a)(dom(a)=1)\mathrm{element}(a) \coloneqq (\mathrm{dom}(a) = 1)

When sets are defined as functions into the singleton, the membership relation aba \in b is defined by the function aa being an element, the function bb being a set, and the codomain of aa being bb

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

Weak extensionality is a theorem in this case. By the universal property of the singleton, any two sets AA and BB with the same domain are equal to each other, which means that any proposition PP between AA and BB implies that A=BA = B, and thus that C.(CA)(CB)\forall C.(C \in A) \iff (C \in B) implies that A=BA = B. The converse follows from indiscernibility of identicals.

In two-sorted set theories

In any two-sorted set theory, the axiom of weak extensionality states that given a set A:SetA:Set and a set B:SetB:Set, A= SetBA =_{Set} B if and only if for all a:Elementa:Element, aAa \in A if and only if aBa \in B.

If the set theory does not have equality of sets as a primitive, we could define equality of sets as the predicate

A= SetBa:Element.(aA)(aB)A =_{Set} B \coloneqq \forall a:Element.(a \in A) \iff (a \in B)

Material strong extensionality

Let \sim be a bisimulation, a binary relation such that for all sets AA and BB such that ABA \sim B, the following conditions hold:

  • for all sets CC such that CAC \in A, there exists a set DD such that DBD \in B and CDC \sim D
  • for all sets DD such that DBD \in B, there exists a set CC such that CAC \in A and CDC \sim D

The axiom of strong extensionality states that for every bisimulation \sim and for every set AA and BB, ABA \sim B implies that A=BA = B.

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 \sim and for every set AA and BB, ABA \sim B implies that A=BA = B.

In any set theory with the axiom of foundation, the axiom of weak extensionality implies the axiom of strong extensionality.

Structural strong extensionality

In any structural set theory, the axiom of strong extensionality states that for all sets AA and BB with an injection i:ABi:A \hookrightarrow B, the two definitions of ii being a bijection are logically equivalent to each other:

  • there exists a function i 1:BAi^{-1}:B \to A such that for all elements aAa \in A and bBb \in B, i 1(i(a))=ai^{-1}(i(a)) = a and i(i 1(b))=bi(i^{-1}(b)) = b
  • for every element xBx \in B there exists an element yAy \in A such that i(y)=xi(y) = x.

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

In dependent type theory, it is possible to define a Tarski universe (V,)(V, \in) of pure sets which behaves as a material set theory. The universal type family of the Tarski universe is given by the type family x:V y:Vyxx:V \vdash \sum_{y:V} y \in x. The axiom of extensionality is given by the following inference rule:

ΓctxΓextensionality V: x:V y:V(x= Vy) z:V(zx)(zy)\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{extensionality}_V:\prod_{x:V} \prod_{y:V} (x =_V y) \simeq \prod_{z:V} (z \in x) \simeq (z \in y)}

Power sets

For power sets, the axiom of extensionality is a property of power sets, and states that given a type AA and subtypes B:𝒫(A)B:\mathcal{P}(A) and C:𝒫(A)C:\mathcal{P}(A), there is an equivalence of types between the identity type B= 𝒫(A)CB =_{\mathcal{P}(A)} C and the dependent function type x:A(x AB)(x AC)\prod_{x:A} (x \in_A B) \simeq (x \in_A C), where (Ω,El Ω)(\Omega, \mathrm{El}_\Omega) is the type of all propositions and x ABEl Ω(B(x))x \in_A B \coloneqq \mathrm{El}_\Omega(B(x)) is the local membership relation between elements x:Ax:A and subtypes B:𝒫(A)B:\mathcal{P}(A). The axiom of extensionality holds in the dependent type theory if and only if function extensionality holds.

See also

 References

Last revised on February 28, 2024 at 02:57:04. See the history of this page for a list of all contributions to it.