# Why isn't the equal sign part of the set theory language?

Many books define the language of set theory only based on $$\in$$. What about the binary relation '$$=$$'? Why is it not mentioned as a symbol of the language? Yes, it is part of first-order logic, but to me its meaning seems to depend on the interpretation which in turn depends on axioms (like extensionality) that must be satisfied.

• Two sets are equal if they are subsets of one another. so set equality is defined in terms of membership. Aug 12 at 14:50
• @NapD.Lover No, you are wrong. Set equality is not neccessarily defined in terms of membership. Check out systems without the axiom of extensionality and the existence of urelemente. Please note that my question is not constrained by any axiomatic system like ZFC. Aug 12 at 15:24
• Aug 12 at 15:38
• What is the content of the Axiom of Extensionality if equality is not a primitive notion? Aug 12 at 15:57
• @NapD.Lover Even in the context of ZFC, equality is not defined in terms of membership - it is a primitive notion in first-order logic. Aug 12 at 23:46

There are (at least) three ways to handle equality in set theory. The most common nowadays is to work in a logic (usually first-order logic) that has equality built in. In this approach, one adopts an axiom of extensionality saying that, if two sets have the same members, then they are equal. (The converse implication is a logical validity, so it does not need to be assumed.)

A second approach, more common many decades ago, works in logic without equality. In this approach, equality is defined by saying two sets are equal iff they have the same members. Then one needs to assume an axiom saying that, if two sets are equal in this sense, then they are members of the same sets.

A third approach also works in logic without equality, but it defines two sets to be equal iff they are members of the same sets. It is then necessary either to assume that equal sets have the same members or to assume enough set-existence axioms to prove this fact. A possible advantage of this third approach is that the same definition can be used for equality of things other than sets (as long as you have enough set-existence axioms).

A variant of the third approach can be used in the context of higher-order logic: Two things are equal iff they have the same properties.

Ultimately, these approaches are equivalent, in the sense that they give the same information about equality. They differ only in how they split this information up into logical axioms, set-theoretic axioms, theorems, and definitions.

Equality is part of the background (first-order) logic, so it is included, but there is no need to mention it. The situation is the same in many other theories. If you want to work in a language without equality, on the other hand, then this is mentioned explicitly.

It is true that from extensionality (and logical axioms), one can prove that two sets are equal if and only if they have precisely the same elements, but this is a separate issue. You could use this to provide a different "set-theoretic" presentation of logic, but under the standard approach, the membership symbol is "non-logical".

The standard presentation of first-order structures interprets the equality symbol as true equality (or, if this is philosophically bothersome, you could treat equality as a primitive and its meaning is unspecified, with everything else interpreted in terms of this primitive). You could work with structures where equality is interpreted as an equivalence relation satisfying some constraints, and recover true equality by passing to a quotient space, but (although useful, and used) these are not the standard first-order structures one means when the term is mentioned. In particular, when you talk in your question of the "meaning" of equality, this is not the standard approach.

• "It is true that from extensionality (and logical axioms), one can prove that two sets are equal if and only if they have precisely the same elements" - I don't follow this. Isn't that exactly what extensionality says? What is there to prove? I must be missing something... Aug 12 at 21:19
• Extensionality is sometimes stated as saying that sets with the same elements are equal -- an implication, rather than an equivalence. The equivalence follows from (axiomatics) properties of equality. Aug 13 at 5:28
• (@bof Oops. Thanks!) Aug 13 at 5:39

In standard formulations of set theory, equality can be defined in terms of set membership, and so there's no "need" to include it as part of the language (it is, in a sense, redundant).

This is similar to the situation we have in formal logic, where we can technically define all connectives in terms of, say, NAND, and leave out everything else. The "language" of formal logic only really requires a single logical connective - all the others (AND, OR, NOT, etc) are redundant.

Of course, there's no fundamental reason why a formal language cannot contain redundant symbols, so I wouldn't read too much into this.

• It's not enough to just define equality in terms of set membership. You also want equality to have all of the expected properties of equality - in particular, the substitution property. For that you need to either have equality as a primitive notion, or else have an axiom of substitution. See wikipedia Aug 12 at 16:14

I just want to add that by including identity as an atomic formula (not just another predicate relation) in underlying logic, say the usual first order logic, then it's much more efficient than push this to set theory or any other axiomatic deductive system. Also by doing so its language becomes much more expressive For example, below inference will be invalid during natural deduction if there's no built-in identity atomic wff in FOL $$∀x (Triangle(x) ↔ Same(x, c)) ⊢ Triangle(c)$$

We have to add an additional semantic axiom $$∀x Same(x, x)$$ every time we want to deduce $$Triangle(c)$$.

Another example to show it's better for first order logic to include identity. Everyone has only one father, if this sentence is translated to FOL sentence with no function symbols allowed it will become $$∀x ∃y [FatherOf(y, x) ∧ ∀z [FatherOf(z, x) → y = z]]$$

Imagine if FOL doesn't have identity atomic formula definition (=) built in, it may be impossible to describe such a restricted case.

So by the identity built-in feature as an atomic wff of first order logic, it saves lots of identity semantic axioms or meaning postulates as additional ZFC definitions for math where identity is everywhere and also its language becomes much more expressive.