Different axiomatizations of set equality

I've seen two definitions (or axioms?) of set equality:

1. $a=b \Leftrightarrow (\forall x : x \in a \Leftrightarrow x \in b)$
2. $a=b \Leftrightarrow (\forall x : a \in x \Leftrightarrow b \in x)$

That is, two sets are considered equal, if

1. They contain the same sets
2. They are contained in the same sets

ZFC seems to include the first version.

My question is: what is the connection between these? Does one follow from another?

I suspect the first version to be an axiom of (any) set theory, while the second is a consequence of first-order axioms for equality, like $a=b \Leftrightarrow [\phi(a) \leftrightarrow \phi(b)]$. In this case, why we need a special axiom in set theory? Doesn't it follow from equality axioms?

• Where have you seen (2) as an axiom? Not a theorem, an axiom. – David C. Ullrich Feb 7 '16 at 18:19
• @DavidC.Ullrich I've seen that far more rarely than the first version, but wikipedia mensions it as an axiom: en.wikipedia.org/wiki/… – lisyarus Feb 7 '16 at 18:22
• If I'm reading that article correctly, under "FOL with equality" it's said to be a "Logic axiom", by which they mean it follows from standard FOL with equality, as it should, not that it's an axiom of set theory. I see it listed as a "set theory axiom" under FOL without equality. If for whatever reason we want to talk aobut equality of sets in FOL wihtout equality then yes of course we need to add it as an axiom to our set theory. – David C. Ullrich Feb 7 '16 at 18:38
• The second axiom is the Leibnizian principle of Identity of indiscernibles. – Pedro Sánchez Terraf Feb 7 '16 at 19:46
• You may want to take a look at page 29 of Schechter’s Handbook of Analysis and its Foundations. He discusses more in depth the two approaches from the Wikipedia page: (a) starting from a first-order theory with equality and requiring that this equality coincides with (one of) the equality induced by $\in$; (b) starting from a first-order theory without equality, defining the equality to be the one induced by $\in$ and requiring that it behaves like a proper equality. – Vej Kse Feb 14 '16 at 15:25

The situation is rather simple at a higher level of abstraction. We are interested here in a collection of objects U, equipped with some binary relation $\prec$, from which we can define two equivalence relations on U:

• $b_0\simeq b_1$ iff $\forall a, a \prec b_0 \iff a \prec b_1$;
• $a_0\backsimeq a_1$ iff $\forall b, a_0 \prec b \iff a_1 \prec b$.

An equality on U must be an equivalence relation $=$ for which all formulae all stable under substitution of equals by equals. In general, we would require that all operations preserve the equality and all relations are invariant under it. Here, we just need $\prec$ to be invariant under $=$, i.e.:

1. $b_0 = b_1 \Longrightarrow b_0 \simeq b_1$;
2. $a_0 = a_1 \Longrightarrow a_0 \backsimeq a_1$.

These are the left-to-right directions of your conditions 1 and 2.

Now, it’s obvious that doing the following is equivalent:

• Start from $U$, $\prec$ and an equality $=$ (satisfying 1 and 2), and require that $=$ coincides with $\simeq$ (i.e. the reverse of 1 holds).
• Start from $U$, $\prec$, define $=$ to be $\simeq$ (so that 1 and its reverse hold) and, to ensure that it is a proper equality, require condition 2.

Most often, people do the first and call the reverse of 1 (or the equivalence) the Axiom of Extensionality; some (like Takeuti and Zaring in Introduction to Axiomatic Set Theory, pp. 7-8 or Schechter in Handbook of Analysis and its Foundations, p. 29) do the second and call 2 the Axiom of Extensionality.

As Eric Wofsey mentions, the reverse of 2 holds if singletons exist, i.e. if for any $a$, there is a $b$ such that $x \prec b$ iff $x = a$: we apply the definition of $a_0 \backsimeq a_1$ to that singleton $b$ obtained from $a_0$ (or $a_1$). If we add everywhere the assumption of the existence of singletons, the two approaches above are thus also equivalent to

• Start from $U$, $\prec$, define $=$ to be $\backsimeq$ (so that 2 and its reverse hold), and require 1 and its reverse.

The equality axioms of first-order logic are $a=b \Rightarrow [\phi(a) \Leftrightarrow \phi(b)]$, not $a=b \Leftrightarrow [\phi(a) \Leftrightarrow \phi(b)]$. So only the $\Rightarrow$ direction of (1) and (2) follows from general first order-logic, whereas the $\Leftarrow$ direction has real content specific to set theory. I've never seen (2) actually stated as an axiom of set theory. However, it follows from the usual axioms of set theory. For instance, Pairing says that for any $a$, there exists a set $x$ such that for all $c$, $c\in x \Leftrightarrow (c=a\vee c=a)$. If $a\in x\Leftrightarrow b\in x$, plugging in the $x$ obtained from Pairing above gives that $b\in x$ and hence $b=a$. This gives the $\Leftarrow$ direction of (2); as mentioned before, the $\Rightarrow$ direction is just part of first-order logic and has nothing to do with set theory in particular.

Note, however, that (2) does not imply (1), even in the presence of all the other axioms of set theory (and thus by symmetry, (1) does not imply (2) without assuming any additional axioms). Indeed, (2) follows from Pairing and no other axioms, so any model of all the axioms of set theory except (1) will still satisfy (2).