# axioms of equality

Every text I've come across uses the Axiom of Extensionality to describe the fact that sets are equal iff they contain each other's elements. $$(\forall x)(\forall y)\bigl((\forall a)(a\in x \iff a\in y) \implies (x=y)\bigr)$$ Some will regard this as an axiom, while some regard this as the very definition of equality (replacing the implication with a biconditional). Either way, the idea is that given two sets, regardless of how they were named, defined, or written, if they have exactly same elements, they are equal. A set can be described completely and only by its elements.

Another fun fact about sets is that equal sets are members of exactly the same collections. $$(\forall x)(\forall y)\bigl((x=y) \implies (\forall b)(x\in b \iff y\in b)\bigr)$$ I've always been comfortable with the idea that equal sets have the same elements, but the second fact is, to me at least, much more fascinating, and strikes a beautiful symmetry with the first.

If we choose to call the first fact the "Axiom of Extensionality" (which seems to be the convention), what is the name of the second fact? Is it another axiom, or can it be proven from the first? Are they logically equivalent? If we take Extensionality as a definition, then the second fact reduces to $$(\forall x)(\forall y)\bigl((\forall a)(a\in x \iff a\in y) \implies (\forall b)(x\in b \iff y\in b)\bigr)$$

Are there any texts that mention this? So far I have not seen it other than on Wikipedia.

• Quine was fond of taking the "axiom of extensionality" as the definition of "$=$", and adopting substitutivity/indiscernibility as an additional set theoretic axiom. But so far as I know he's just about the only author to arrange things this way. Commented Dec 15, 2013 at 3:50

The second formula is an axiom of the first order logic with equality, together with the following axioms about equality:

1. $x=x$.
2. $x=y\rightarrow(\varphi\leftrightarrow\psi)$, where and $y$ is free for $x$ in $\varphi$ and $\psi$ is replacing some free variable $x$ by $y$ in $\varphi$.

Unlike Extensionality, which is a proper axiom, these equality axioms are valid in every normal models, hence they deserve the name "logical axioms".

The second fact is a special case of the indiscernibility of identicals and is part of the definition of equality. The principle says, for all predicates $\phi (u, t_1, t_2, \ldots, t_n)$, $$\forall x . \forall y . (x = y) \to (\phi (x, t_1, t_2, \ldots, t_n) \leftrightarrow \phi (y, t_1, t_2, \ldots, t_n))$$ where $t_1, t_2, \ldots, t_n$ are arbitrary parameters. For the language of set theory in first-order logic without equality, the special case implies the general principle.

• I thought that was called the identity of indiscernibles?
– bof
Commented Dec 15, 2013 at 3:14
• That's the converse, also known as Leibniz's law. Commented Dec 15, 2013 at 3:23
• The first axiom schema in the OP is an instance of identity of indiscernibles, because it asserts that if x, y "look the same" from the perspective of set containment (a \in x), then they are equal. Wikipedia has an entry on these two principles.
– 0 _
Commented Jul 7, 2017 at 22:00