I have a question on the close links between extensionality and set equality in ZFC, with or without first order logic (FOL) equality as a primitive inherited by ZFC.
The former seems clear and is covered in Wikipedia and in several MSE posts (here, here, here, and here). We start with FOL equality and it’s substitution property and state that if two sets are equal the predicate formula for membership is true for one set if and only if it’s true for the other. For a predicate formula with two free variables $\phi(x,y)$, the substitution property of FOL equality can be stated as:
$$A=B\implies \forall x (\phi(x,A)\iff \phi(x,B))$$
If the predicate formula is the membership relationship $\phi(x,y)=x\in y$ we get the definition of set equality inherited from FOL equality.
$$A=B\implies \forall x (x\in A\iff x\in B)$$
This defines set equality but doesn’t establish extensionality because two sets with the same members could theoretically differ in other properties which make them unequal. Extensionality is established by stating the converse of the equality definition as the Axiom of Extensionality.
$$\forall x (x\in A\iff x\in B) \implies A=B$$
One can then combine these into the biconditional which nicely captures both extensionality and the inheritance of FOL equality into set equality, i.e.,the binding of $=$ and $\in$, in one tidy package.
$$A=B\iff \forall x (x\in A\iff x\in B)$$
So far so great.
Things get a bit more vague for me if one assumes FOL without equality (or chooses not to define set equality in terms of it). I understand most set theorists accept FOL with equality but I find it an interesting exercise to establish extensionality and define set equality without using FOL equality to define the latter. Again, Wikipedia and other MSE posts touch on this but don’t lock it down for me.
The first option appears to be to just accept the above biconditional as both the definition of set equality a statement in extensionality. Is this actually an axiom or just a definition of set equality in terms of the primitive membership relation? I am aware of the debates on whether definitions are just axioms so what I am really asking is whether extensionality is simply a byproduct of the definition of set equality or whether the Axiom of Extensionality is embedded in the biconditional as it was when we assumed FOL equality.
What intrigues me even more is the approach of stating the Axiom of extensionality without yet defining set equality.
$$\forall A \forall B (\forall X(X\in A \iff X\in B)\iff \forall Y(A\in Y \iff B \in Y))$$
Wikipedia states this without comment as do a few MSE posts linked above. One comment in one of the posts states that either way (i.e., whether you have FOL equality or not) one will eventually have to prove the above.
This idea that two sets have the same members if and only if they are members of the same sets seems pretty fundamental and interesting in its own right, but I have not been able to find any additional color online or in the standard set theory textbooks (Halmos, Hrbeck & Jech, Hatcher, Kunen, etc.). Wikipedia refers to it as merely the “substitution property” of equality but I don’t see that and it seems like it should have deeper meaning. An answer to this post proves it assuming FOL equality, which I get. I would appreciate one of the set theory gurus here explaining how to define set equality from above without using FOL equality, and if there is any deeper meaning to all this. Much appreciated.
Best Answer
We can find all the discussion regarding equality and extensionality in set theory into: Abraham Fraenkel & Yehoshua Bar-Hillel, Foundations of Set Theory, pages 29-33 of 1958 edition.
We may consider equality as primitive, assuming the relevant axioms: this is the case when set theory is based on predicate logic with equality.
Otherwise, we may introduce equality through a suitable definition based on the only primitive of the system (i.e. $\in$), in which case we have to check that the proposed definition ensure: reflexivity, symmetry, transitivity and substitution.
Regarding the second case, that we are interested in here, there are in turn two possibilities:
Thus, we have two choices:
$\text {Eq I}) \: \ x=y \text { iff } \ \forall z (x \in z \leftrightarrow y \in z)$, or
$\text {Eq II}) \: \ x=y \text { iff } \ \forall z (z \in x \leftrightarrow z \in y)$, that can be abbreviated, using the usual definition of $\subseteq$ with: $(x \subseteq y) \land (y \subseteq x)$.
Both definitions provide reflexivity, symmetry, transitivity and "right-substitution", i.e. substitution wrt the right argument of $\in$.
The tautology $x \in z \leftrightarrow x \in z$ gives us reflexivity, and the corresponding properties of $\leftrightarrow$ give symmetry and transitivity.
Regarding "right-substitutivity", i.e. $(z \in x \land x=y) \to (z \in y)$, it is obvious for $(\text {Eq II})$, while the proof is a little bit tricky for $(\text {Eq I})$.
The issue is that the above definition does not provide "left-substitutuvity"; in order to do this, we need a further axiom, that we will call Extensionality:
$\text {Ext I}) \: \ (x \subseteq y \land y \subseteq x) \to x=y$, or
$\text {Ext II}) \: \ (x \in z \land x=y) \to y \in z$.
Note: the proof that $(\text {Eq I})$ above implies substitutivity wrt the right argument may be found into: Abraham Robinson, On the Independence of the Axioms of Definiteness (Axiome Der Bestimmtheit), Jou Symb Log (1939) and it needs some more axioms of set theory.
We have to prove that $x \in z$ and $x=y$ imply $y \in z$.
Using either Pair or Power-set axioms we have that there is a set $t$ such that $x \in t$, and by $(\text {Eq I})$ we have that also $y \in t$.
Assume now that "right-substitutivity" does not hold, i.e. that $\exists r (r \in x \land r \notin y)$.
Applying Separation to $t$ in the form: $\exists w \forall z [z \in w \leftrightarrow (z \in t \land r \in z)]$, we have that there is the set $w$ of those $z$ of $t$ for which $r \in z$. But $x \in w$ and $.y \notin w$, contrary to $(\text {Eq I})$.