Should this "definition" of set equality be an axiom?

This question is about set equality, as it is presented in Chapter 3, Set Theory, Section 1, Fundamentals, of Terence Tao's textbook, Analysis I. However, I think it is prudent to begin earlier (technically, later) in the book, in Appendix A, the basics of mathematical logic, Section 7, Equality. On page 329, he writes,

Equality is a relation linking two objects $x$, $y$ of the same type $T$ (e.g., two integers, or two matrices, or two vectors, etc.). Given two such objects $x$ and $y$, the statement $x = y$ may or may not be true; it depends on the value of $x$ and $y$ and also on how equality is defined for the class of objects under consideration. [...]

How equality is defined depends on the class $T$ of objects under consideration, and to some extent is just a matter of definition. However, for the purposes of logic we require that equality obeys the following four axioms of equality:

• (Reflexive axiom). Given any object $x$, we have $x = x$.
• (Symmetry axiom). Given any two objects $x$ and $y$ of the same type, if $x = y$, then $y = x$.
• (Transitive axiom). Given any three objects $x$, $y$, $z$ of the same type, if $x = y$ and $y = z$, then $x = z$.

• (Substitution axiom). Given any two objects $x$ and $y$ of the same type, if $x = y$, then $f(x) = f(y)$ for all functions or operations $f$.

  Similarly, for any property $P(x)$ depending on $x$, if $x = y$, then $P(x)$ and $P(y)$ are equivalent statements.

Based on the information in this appendix, it appears to me that Tao is developing a theory of objects, where objects may be of different types or classes (in other words, his logic is many-sorted). Returning to Chapter 3, Set Theory, he asserts that sets are a type of object, and that the $\in$ predicate can be used to form a proposition about any pair of objects, where the second object is a set: he writes, on page 34,

We first clarify one point: we consider sets themselves to be a type of object.

Axiom 3.1 (Sets are objects). If $A$ is a set, then $A$ is also an object. In particular, given two sets $A$ and $B$, it is meaningful to ask whether $A$ is also an element of $B$.

[...]

To summarize so far, among all the objects studied in mathematics, some of the objects happen to be sets; and if $x$ is an object and $A$ is a set, then either $x \in A$ is true or $x \in A$ is false.

On page 35, he presents the definition of equality for sets:

Definition 3.1.4 (Equality of sets). Two sets $A$ and $B$ are equal, $A = B$, iff every element of $A$ is an element of $B$ and vice versa. To put it another way, $A = B$ if and only if every element $x$ of $A$ belongs also to $B$, and every element $y$ of $B$ belongs also to $A$.

[...]

One can easily verify that this notion of equality is reflexive, symmetric, and transitive (Exercise 3.1.1). Observe that if $x \in A$ and $A = B$, then $x \in B$, by Definition 3.1.4. Thus the "is an element of" relation $\in$ obeys the axiom of substitution (see Section A.7). Because of this, any new operation we define on sets will also obey the axiom of substitution, as long as we can define that operation purely in terms of the relation $\in$.

I feel that the statement in Definition 3.1.4 should be considered an axiom, rather than a definition, since the $=$ predicate was already axiomatized in section A.7 as part of his background logic. The exercise to "verify that this notion of equality is reflexive, symmetric, and transitive" could then be understood as a verification that the axiom for equality of sets is consistent with the axioms of equality from section A.7 (is "consistent" the correct word to use here?). Am I correct in thinking that his definition for equality of sets should actually be an axiom? More generally, how should one go about distinguishing whether a statement should be an axiom or a definition?

Added in update: I guess it comes down to whether we are using first-order logic with equality; as stated here, the first possibility is that we assume the axioms listed in the appendix for the $=$ predicate, including the substitution axioms for $\in$ with regards to sets:

• For all sets $x$ and $y$, if $x = y$, then for all objects $z$, $z\in x$ if and only if $z\in y$.

• For all objects $x$ and $y$, if $x = y$, then for all sets $z$, $x\in z$ if and only if $y\in z$.

Then we add in the axiom of extensionality for FOL with equality:

• For all sets $x$ and $y$, if for all objects $z$, $z\in x$ if and only if $z\in y$, then $x = y$.

On the other hand, the second possibility, which appears to be the case in Tao's text (since he asks us to prove that equality of sets obeys the reflexive, symmetric, and transitive axioms), is that we don't axiomatize anything about the $=$ predicate until we get to this point, and then "define" it for sets with the axiom:

• For all sets $x$ and $y$, $x = y$ if and only if, for all objects $z$, $z\in x$ if and only if $z\in y$.

The axioms of equality in the appendix then serve more as a "checklist" of what we want equality of sets to satisfy; as explained in this answer to another question about Tao's definition of equality,

[...] in set theory, these "axioms" are not the definition of equality. Rather, equality is defined via the formula above: two sets are equal when they consist of identical elements. But when we define equality in this way, there is a natural question: why we are naming this as "equality" at all? This is why we prove "axioms of equality", which we are already used to, to show that the naming "equality" is adequate. And when we prove them, they become theorems of set theory and properties of equality rather than axioms. [...]

Note. While there isn't at this point any assumption about the $=$ relation for objects of other types, he does appear to rely on it existing for his statement of the axiom of pairing on page 36:

[...] if $a$ and $b$ are objects, then there exists a set $\{a, b\}$ whose only elements are $a$ and $b$; i.e., for every object $y$, we have $y \in \{a, b\}$ if and only if $y = a$ or $y = b$ [...]

Also, while he never explicitly states it, I think he probably assumes the axiom of extensionality for FOL without equality:

• For all objects $x$ and $y$, if $x = y$, then for all sets $z$, $x\in z$ if and only if $y\in z$.

A good observation, but note that the $=$ predicate was not axiomatized previously. In fact, Tao explicitly says: "how equality is defined depends on the class $T$ of objects under consideration". The axioms listed in that section describe the behavior of all $=$ predicates, but certainly do not define any of them! It's analogous to the axiom "all positive divisors of $p$ are either $1$ or $p$"; this correctly describes all primes, but does not define a particular prime.

Some axioms are 'definitional axioms' ... they are axioms and definitions at the same time. So, when the book defines set equality, we could capture that using a definitional axiom, such as: for any sets $x$ and $y$:

$$x = y \leftrightarrow \forall z (z \in x \leftrightarrow z \in y)$$

The fact that $\leftrightarrow$ was used is often indicative of such definitional axioms.

Also: the fact that $=$ was already used as a logical symbol, having the properties of reflexivity, symmetry, transitivity, and indiscernability (what the book calls the Substitution axiom) does not mean that set equality had to obey this: we could have chosen a different symbol specific for 'set equality', and we could have defined it in such a way that in fact it did not have all these properties, had we wanted to. Notice, for example, how we don't use the $=$ symbol for 'cardinality-equality' or 'equinumerosity'. So, to avoid confusion, maybe we should have used a special symbol for 'set-equality' as well.

Indeed, to say that sets are equal when they have the same elements is to have an 'extensional' view on sets, which is different from an 'intensional' view, where sets can have the same elements but still not be the same set. For example, suppose that all and only people whose favorite color is green are people whose middle name start with a 'J'. Then on the extensional view, the set of 'all people whose favorite color is green' equals the set of 'all people whose middle name starts with a 'J'. But on the intensional view, the two sets just happen to have the same members, but are still considered different sets. So we could have defined sets that way, and in that case, the 'has-the-same-members-as' predicate would definitely have needed a symbol other than $=$.

While Tao overloads the equality symbol here to ambiguously mean either the logical equality or set equality (at the sort of sets), he does not equate them. To do that would indeed require an axiom. Instead what he states is if we carefully articulate everything in terms of the membership relation then it would be admissible to add an axiom identifying logical equality at sets with the definition he provided. To put it another way, if he was taking the conflation as an axiom the qualification in the sentence "Because of this, any new operation we define on sets will also obey the axiom of substitution, as long as we can define that operation purely in terms of the relation $\in$." would have been unnecessary. Instead, if the statement was an axiom it would be inconsistent to have an operation that didn't obey the axiom of substitution. Tao's use of the same symbol for logical equality (at sets) and set equality is only justifiable though, if he does guarantee every definition satisfies all the expressible instances of the axiom of substitution with respect to set equality. This is a metalogical exercise.

While I'm pretty sure it's not important for Tao's purposes, there are differences between axiomatically asserting that these equalities coincide and not asserting that even in the case where the axiom is admissible. I was originally going to just talk about this as an aside, but with your update to the question it's more directly relevant. Tao is working in a first-order logic with equality (at least for the purpose of talking about the "axioms of equality"). Just because our logic has equality doesn't mean we can't take the second option in the link you provided and define an equivalence relation that represents set equality, though you definitely should use a different symbol in that case. This is what Tao is doing. By an abuse of notation, he's using the same symbol. This is justified by having the first option in that link — identifying the logical equality and the defined set theoretic equality — be admissible.

So what's the difference? With a logical notion of equality, the semantics of equality is equality of the interpretations. The Substitution Axiom is not a theorem you can prove (or even state) in first-order logic about any relation. In this sense, logical equality is on par with other logical connectives as talking about an operation on interpretations. For a defined notion of "equality", you are simply introducing a new relation symbol and proving some properties about it. For the Substitution Axiom you must metalogically prove that it holds for all predicates/operations that you can write down.

However, this just says you can't write down anything that distinguishes objects related by this equivalence relation; there could still be things that can distinguish those objects. Semantically, this means the interpretation of this defined "equality" is an equivalence relation that is respected by all the defined predicates and operations, but there could be other functions in the interpretation that don't respect that equivalence relation. For example, I could interpret "sets" as pairs of sets and membership as membership in only the first component of the pair. The condition for the substitution would then, at the semantic level, look like the following for predicates (which get interpreted as subsets): $(x,y)\in P\Leftrightarrow \forall z.(x,z)\in P$. The identifying of logical equality with the defined "equality" would be admissible for the definition of set "equality" Tao provided if there was an interpretation that made the above condition true (and a similar one for operations). Whether such an interpretation exists depends on the predicates, operations, and axioms we assert. Of course, there exist subsets that don't satisfy the above, so if we did assert the axiom identifying the two forms of equality, the above would no longer be a valid interpretation.

Ultimately, in a fixed theory where axiomatically asserting a given equivalence relation coincides with logical equality is admissible we can't tell the difference between whether that equivalence relation is logical equality or not at the level of logic/syntax. I assume Tao isn't concerned with interpretations of the theory he's building up, and he's saying that he'll maintain this admissibility property as he extends the theory. To the extent that you want an explicit formula for equality, the work is the same either way. Either you have the axiom and you must check that the logic is (relatively) consistent, or you have to check admissibility of the axiom which is checking that it would be consistent to add the axiom. The only difference between him working in FOL with or without equality is in the latter case he is obligated to provide an explicit definition of "equality" (if he uses it). Explicitly defining a notion of equality and showing that it is admissible to have it be the (logical) notion of equality for a sort as Tao does is a good bit of logical hygiene which I recommend.