[Math] Should this “definition” of set equality be an axiom

axiomsfoundationslogic

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$.

Best Answer

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.

Related Question