Axiom of extensionality

One of the axioms of set theory, asserting that two sets are equal if they contain the same elements:

$$\forall u\forall v(\forall x(x\in u\Leftrightarrow x\in v)\Rightarrow u=v).$$

In a language not containing the equality symbol and having only one predicate symbol $\in$, the axiom of extensionality has the form

$$\forall u\forall v(\forall x(x\in u\Leftrightarrow x\in v)\Rightarrow\forall z(u\in z\Leftrightarrow v\in z)).$$

The axiom of extensionality has no real importance for the formalization of mathematics in the Zermelo–Fraenkel system $\text{ZF}$. Anything that can be constructed within the system $\text{ZF}$ can be formalized in a system without the axiom of extensionality. Let $\text{ZF}^-$ be the system obtained from $\text{ZF}$ by removing the axiom of extensionality and by replacing formulas of the form $u=v$ in the remaining axioms by the formula

$$\forall x(x\in u\Leftrightarrow x\in v).$$

Then it can be shown that there exists an interpretation of $\text{ZF}$ in $\text{ZF}^-$. A similar assertion is valid for the theory of types.

For Quine's system $\text{NF}$, obtained from the theory of types by the "erasure" of the type indices, the situation is different: It is not possible to interpret $\text{NF}$ in $\text{NF}^-$. The system $\text{NF}^-$ ($\text{NF}$ without the axiom of extensionality) is a rather weak system, and its consistency can be proved in formal arithmetic. The system $\text{NF}$, however, is not weaker than the theory of types with the axiom of infinity.

References

[1]	J. Barwise (ed.) , Handbook of mathematical logic , North-Holland (1977)
[2]	M. Boffa, "The consistency problem for NF" J. Symbolic Logic , 42 : 2 (1977) pp. 215–220

References

[a1]	D.S. Scott, "More on the axiom of extensionality" Y. Bar-Hillel (ed.) E.I.J. Poznanski (ed.) M.O. Rabin (ed.) et al. (ed.) , Essays on the foundation of mathematics , North-Holland (1962)