Axiom of extensionality

In ZF set theory

In the formal language of the Zermelo–Fraenkel axioms, the axiom reads:

${\displaystyle \mathrm{\forall }x\mathrm{\forall }y[\mathrm{\forall }z(z\in x\leftrightarrow z\in y)\to x=y]}$

or in words:

If the sets ${\displaystyle x}$ and ${\displaystyle y}$ have the same members, then they are the same set.

In pure set theory, all members of sets are themselves sets, but not in set theory with urelements. The axiom's usefulness can be seen from the fact that, if one accepts that ${\displaystyle \mathrm{\exists }A\mathrm{\forall }x(x\in A⟺\mathrm{\Phi }(x))}$, where ${\displaystyle A}$ is a set and ${\displaystyle \mathrm{\Phi }(x)}$ is a formula that ${\displaystyle x}$ occurs free in but ${\displaystyle A}$ doesn't, then the axiom assures that there is a unique set ${\displaystyle A}$ whose members are precisely whatever objects (urelements or sets, as the case may be) satisfy the formula ${\displaystyle \mathrm{\Phi }(x)}$.

The converse of the axiom, ${\displaystyle \mathrm{\forall }x\mathrm{\forall }y[x=y\to \mathrm{\forall }z(z\in x\leftrightarrow z\in y)]}$, follows from the substitution property of equality. Despite this, the axiom is sometimes given directly as a biconditional, i.e., as ${\displaystyle \mathrm{\forall }x\mathrm{\forall }y[\mathrm{\forall }z(z\in x\leftrightarrow z\in y)\leftrightarrow x=y]}$.

In NF set theory

Quine's New Foundations (NF) set theory, in Quine's original presentations of it, treats the symbol ${\displaystyle =}$ for equality or identity as a shorthand with a definition in terms of ⁠${\displaystyle \in }$⁠, instead of a primitive symbol of the formal language like in the usual presentation of the ZF set theory. There are two variants of such a definition, one needing a separate axiom of extensionality and the other already representing the principle of extensionality in itself.

In Quine's New Foundations for Mathematical Logic (1937), the original paper of NF, the definition D8 defines ⁠${\displaystyle x=y}$⁠ as shorthand for ⁠${\displaystyle \mathrm{\forall }z(x\in z\to y\in z)}$⁠. This definition is based more on intension rather than extension, as it can be read as "two objects are equal if one belongs to all sets that the other belongs to (i.e., has all the properties that the other has)". This definition, as well as a variant that replaces the conditional by the biconditional, was common in Quine's time. The name "principle of extensionality" is then given to the postulate P1, ${\displaystyle x\subset y\to (y\subset x\to x=y)}$, which is logically equivalent to the ZF axiom of extensionality.

In his Mathematical Logic (1951), Quine defines ⁠${\displaystyle x=y}$⁠ as ⁠${\displaystyle \mathrm{\forall }z(z\in x\leftrightarrow z\in y)}$⁠ (definition D10)., exactly equivalent to the antecedent of the ZF axiom of extensionality. This is based on the principle that "classes are the same when their members are the same", although Quine seems to have taken this principle for granted at this point and does not explicitly discuss "extensionality". This definition change was motivated by a desire to be compatible with proper classes. Quine also has to introduce a substitutivity axiom

If ⁠${\displaystyle \varphi }$⁠ is atomic, and ⁠${\displaystyle {\varphi }^{\prime }}$⁠ is formed from ⁠${\displaystyle \varphi }$⁠ by putting ⁠${\displaystyle {\alpha }^{\prime }}$⁠ for an occurrence of ⁠${\displaystyle \alpha }$⁠, then ⁠${\displaystyle ⊢⌜\alpha ={\alpha }^{\prime }.\supset .\varphi \supset {\varphi }^{\prime }⌝}$⁠

to compensate for this definition change.

Modern accounts of NF usually are based on first-order logic with equality (where the ⁠${\displaystyle =}$⁠ symbol is automatically primitive) and thus admit the axiom of extensionality in its ZF form.

In ZU set theory

In the Scott–Potter (ZU) set theory, the "extensionality principle" ${\displaystyle (\mathrm{\forall }x)(x\in a\iff x\in b)\Rightarrow a=b}$ is given as a theorem rather than an axiom, which is proved from the definition of a "collection".

In set theory with ur-elements

An ur-element is a member of a set that is not itself a set. In the Zermelo–Fraenkel axioms, there are no ur-elements, but they are included in some alternative axiomatisations of set theory. Ur-elements can be treated as a different logical type from sets; in this case, ${\displaystyle B\in A}$ makes no sense if ${\displaystyle A}$ is an ur-element, so the axiom of extensionality simply applies only to sets.

Alternatively, in untyped logic, we can require ${\displaystyle B\in A}$ to be false whenever ${\displaystyle A}$ is an ur-element. In this case, the usual axiom of extensionality would then imply that every ur-element is equal to the empty set. To avoid this consequence, we can modify the axiom of extensionality to apply only to nonempty sets, so that it reads:

${\displaystyle \mathrm{\forall }A\mathrm{\forall }B(\mathrm{\exists }X(X\in A)⟹[\mathrm{\forall }Y(Y\in A⟺Y\in B)⟹A=B]).}$

That is:

Given any set A and any set B, if A is a nonempty set (that is, if there exists a member X of A), then if A and B have precisely the same members, then they are equal.

Yet another alternative in untyped logic is to define ${\displaystyle A}$ itself to be the only element of ${\displaystyle A}$ whenever ${\displaystyle A}$ is an ur-element. Such a set ${\displaystyle A}$ is known as a Quine atom. While this approach can serve to preserve the axiom of extensionality, the axiom of regularity will need an adjustment instead.