0
$\begingroup$

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?

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ Dec 22, 2021 at 14:15
  • $\begingroup$ See also this post as well as this one. $\endgroup$ Dec 22, 2021 at 14:18

2 Answers 2

5
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .