# ZF Extensionality axiom

To familiarize myself with axiomatic set theory, I am reading Kenneth Kunen's The Foundations of Mathematics that presents ZF set theory. I haven't gotten really far since I am stuck at the axiom of Extensionality, stated as follows:

$$\forall x,y \; [\forall z(z \in x \leftrightarrow z \in y) \rightarrow x = y]$$

As far as I understood it, the purpose of this axiom is to state that every two sets that have exactly the same members are the same set. In terms of the above formula, when antecedent is true, the consequent needs to be true. What confuses me here is the case when the antecedent is false. Then, the consequent can be false or true, i.e., we can't say much about the consequent. But, don't we really want to say that in that case those two sets are not equal? More precisely, shouldn't we use equivalence instead of implication? If not, what is the reason?

• The converse is a logical tautology, however. – Zhen Lin May 19 '13 at 23:06

The reason the converse is not part of the axiom is that it already follows from the axioms of first-order logic: $x = y \implies (\varphi(x) \iff \varphi(y))$ for any formula $\varphi$. This is known as the substitution property of equality.

Equality is often a part of the logical symbols, and if $x=y$ then for every relation $R$, and every $z$ we have $R(x,z)\leftrightarrow R(y,z)$ and $R(z,y)\leftrightarrow R(z,x)$.

In particular $\in$ is such relation.

In older texts, you can sometimes find that people don't assume that $=$ is part of the language and then we simply define $x=y$ as the formula $\forall w(w\in x\leftrightarrow w\in y)$, from which extensionality follows as a theorem. Then the language containing only the binary relation symbol $\in$ (without equality) is called the Language of Set Theory (often abbreviated as LST).

• Ha, I beat you for once (but only by a few seconds) – Trevor Wilson May 19 '13 at 23:09
• @Trevor: My girlfriend is somewhat ill, and sleeping in the other room. I was trying to type slowly as to not make a ruckus with my loud buckling spring mechanical keyboard. ;-) – Asaf Karagila May 19 '13 at 23:10
• Ah, I knew there must be a reason. Hope she is better soon. – Trevor Wilson May 19 '13 at 23:11
• She'll be fine by morning. It doesn't work, by the way. The keyboard is still as loud as the apocalypse. I love it! ;-) – Asaf Karagila May 19 '13 at 23:11
• I like them too. I have a collection of four model M's. – Trevor Wilson May 19 '13 at 23:14