Jech's text on Set Theory states the following:
If X and Y have the same elements, then X = Y :
∀u(u ∈ X ↔ u ∈ Y ) → X = Y.
The converse, namely, if X = Y then u ∈ X ↔ u ∈ Y, is an axiom of predicate calculus. Thus we have
X = Y if and only if ∀u(u ∈ X ↔ u ∈ Y).
The axiom expresses the basic idea of a set: A set is determined by its elements.
To check my understanding, are the following true?
(1) The axiom of extension states only that if two sets have the same members, then those two sets equal.
(2) It is, on the other hand, an axiom of the language of set theory (i.e., predicate calculus) that if two sets equal, then they have the same members.
A third question:
(3) It seems that the axioms of ZFC are very much independent of the language being worked with. That is, the axioms of ZFC don't state we must be working in the language predicate calculus. Then I take it there exist languages we could be working with that don't have the property that if two sets are equal, they have the same members (so that we could only conclude if two sets have the same members, they are the same and not the reverse). Is this true? Do mathematicians ever work in languages besides predicate calculus?
(1) and (2) are correct.
As for (3), recall Leibniz's Law -- if $a$ and $b$ are one and the very same thing, then whatever property $a$ has $b$ must have too. Applied to sets, if $a$ and $b$ are one and the very same set, then whatever property $a$ has $b$ must have too. So in particular, if $a$ and $b$ are one and the very same set, if $a$ has the property of having $x$ as a member, $b$ has the property of having $x$ as a member. In symbols, if that helps, if $a = b$ then $x \in a \to x \in b$. And of course, we likewise have if $a = b$ then $x \in b \to x \in a$. So:
But $x$ was arbitrary, so there's implicit generalization here which we can make explicit, again borrowing logical notation
Now, in getting this far we are just using the informal Leibniz's Law, notation for set-membership, and some handy logical notation. We aren't appealing to a formal system; rather we are appealing to informal mathematical reasoning (the sort of reasoning that logic books aim to formalize using the classical predicate calculus). Because we do want the formal predicate calculus to replicate this informal mathematical reasoning, we will get -- inside the calculus, applied to a language with $\in$ available
But the ultimate grounds for this half of the formal version of the extensionality principle are the background informal reasoning using Leibniz's Law which we aim to regiment formally. What's going on here is not an arbitrary appeal to one formal calculus rather than another.