# 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?

• See the post Why include equality in FOL for ZFC? We can use equality "inherited" from the underlying predicate logic (in which case we understood it as a general properties of every "object") or we can introduce it specifically for sets, in which case we define it in terms of the basic $\in$ relation and with Extensionality we prove that the defined $=$ relation has all the expected properties. Dec 22, 2021 at 14:15
• See also this post as well as this one. Dec 22, 2021 at 14:18

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.