Different meanings of "=" in first-order logic and in set theory

In first-order logic, a primitive predicate "=" is introduced. As a result, "a = b" or "=(a,b)" is a primitive equal relation in first-order logic. In set theory, meanwhile, "=" can be defined as follows: $a = b$ if $$\forall x, x \in a \leftrightarrow x \in b.$$ I am wondering what is the meaning of the primitive equal sign, and what is the relation between the two equal signs respectively from first-order logic and set theory?


The axiom of extensionality is not a definition, it's an axiom. It states that if two sets have the same elements, they satisfy the property of equality from first order logic.


The only criteria for an equality predicate are that it follows the "rules of equality".

The rules of equality are (the universal closure of) the following:

  1. For every $n$-ary predicate symbol $P$, $(\bigwedge\limits_{i = 1}^n x_i = y_i) \land P(x_1, \ldots, x_n) \to P(y_1, \ldots, y_n)$
  2. For every $n$-ary function symbol $f$, $(\bigwedge\limits_{i = 1}^n x_i = y_i) \to f(x_1, \ldots, x_n) = f(y_1, \ldots, y_n)$
  3. $x = x$
  4. $a = b \to b = a$

From here, we can prove the following metatheorem:

Substitution Principle of Equality: For every proposition $\phi$ where $y$ does not occur bound, the universal closure of $x = y \land \phi \to \phi[x \mapsto y]$ holds. Here, $\phi[x \mapsto y]$ is $\phi$ with every free occurence of $x$ replaced by $y$.

The proof is a straightforward structural induction on $\phi$.

Generally, first-order logic will come with equality (and the above rules) built in. But it's certainly possible to consider a formal theory without built-in equality.

Let's consider your "definition" of equality in set theory, which is

$$x = y :\equiv \forall z (z \in x \iff z \in y)$$

Note that without assuming any axioms of set theory, this does not suffice as a definition of equality because it does not meet criterion 1. We would have to formulate the axiom of extensionality as (the universal closure of)

$$(\forall z (z \in x \iff z \in y)) \land x \in k \to y \in k$$

to force rule 1 to hold. At that point, the logic of set theory becomes completely identical to the normal first-order theory with $=$ built-in.