Namespaces
Variants
Actions

Difference between revisions of "Axiom of extensionality"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
(TeX)
 
Line 1: Line 1:
 +
{{TEX|done}}
 
One of the axioms of set theory, asserting that two sets are equal if they contain the same elements:
 
One of the axioms of set theory, asserting that two sets are equal if they contain the same elements:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a0142801.png" /></td> </tr></table>
+
$$\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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a0142802.png" />, the axiom of extensionality has the form
+
In a language not containing the equality symbol and having only one predicate symbol $\in$, the axiom of extensionality has the form
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a0142803.png" /></td> </tr></table>
+
$$\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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a0142805.png" />. Anything that can be constructed within the system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a0142806.png" /> can be formalized in a system without the axiom of extensionality. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a0142808.png" /> be the system obtained from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a0142809.png" /> by removing the axiom of extensionality and by replacing formulas of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a01428010.png" /> in the remaining axioms by the formula
+
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
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a01428011.png" /></td> </tr></table>
+
$$\forall x(x\in u\Leftrightarrow x\in v).$$
  
Then it can be shown that there exists an [[Interpretation|interpretation]] of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a01428012.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a01428013.png" />. A similar assertion is valid for the theory of types.
+
Then it can be shown that there exists an [[Interpretation|interpretation]] of $\text{ZF}$ in $\text{ZF}^-$. A similar assertion is valid for the theory of types.
  
For Quine's system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a01428015.png" />, obtained from the theory of types by the  "erasure"  of the type indices, the situation is different: It is not possible to interpret <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a01428016.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a01428017.png" />. The system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a01428019.png" /> (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a01428020.png" /> without the axiom of extensionality) is a rather weak system, and its consistency can be proved in formal arithmetic. The system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a014/a014280/a01428021.png" />, however, is not weaker than the theory of types with the axiom of infinity.
+
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====
 
====References====

Latest revision as of 12:02, 9 April 2014

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


Comments

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)
How to Cite This Entry:
Axiom of extensionality. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Axiom_of_extensionality&oldid=16856
This article was adapted from an original article by V.N. Grishin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article