What happens if "equality of sets" is regarded as a defined concept instead of a primitive notion?

Question

Formulation 1 below is the one used in the classical set theory (used in the traditional mathematics), right?

Formulation 1
Primitive notions: set, be element of, equality.
Axiom: A set $A$ is equal to a set $B$ if all elements of $A$ are elements of $B$ and vice-versa.

Instead of taking equality as a primitive notion, could it be considered a defined concept as in Formulation 2?

Formulation 2
Primitive notions: set, be element of.
Definition of equality: We say that a set $A$ is "equal" to a set $B$ if all elements of $A$ are elements of $B$ and vice-versa.

From the mathematical point of view, it seems there is no difference. The theorems will be proved the same way, right?

Is there any context where Formulation 2 is considered wrong or not equivalent to Formulation 1?

Answer 1

If one does not have equality as part of the underlying logic, then there is indeed a way of defining it inside set theory,

$x = y \overset{def}\Longleftrightarrow (\forall z(z \in x \iff z \in y) \land \forall z (x \in z \iff y \in z))$

which of course is just a modification of extensionality: the new bit about belonging to exactly the same sets is just so that one is able to recover the substitution principle of equality

$\forall x,y (x = y \implies (\varphi(x) \iff \varphi(y)))$

for any $\varphi(-)$, from separation/comprehension, which I suppose is not possible using only

$x = y \overset{def}\Longleftrightarrow \forall z(z \in x \iff z \in y)$

edit: if one defines equality by that first phrase up there, then it only makes sense that the 'new', appropriate axiom of extensionality is/becomes

Ax.Ex.: $\forall x,y (\forall z(z \in x \iff z \in y) \iff \forall z (x \in z \iff y \in z))$

Answer 2

In addition to @ac15's answer, you can prove $$\forall x\forall y (\forall z (x \in z \iff y \in z)) \implies (\forall z(z \in x \iff z \in y))$$ from comprehension and pairing. Assume $x, y$ are members of the same sets but don't have the same members. w.l.o.g. we may assume there exists $t\in x\setminus y$.

By pairing $$\forall x\forall y\exists Z (x\in Z\land y\in Z)\tag{1}$$ Let $Z_0$ be a $Z$ satisfying $(1)$ for the given $x,y$.

An instance of comprehension is $$\forall s\forall Z\exists u(\forall p (p\in u\iff p\in Z\land s\in p))\tag{2}$$ Specializing $(2)$ to $s=t, Z=Z_0$ we get $$\exists u(\forall p (p\in u\iff p\in Z_0\land t\in p))\tag{3}$$ Let $u_0$ be a $u$ satisfying $(3)$. Then $$\forall p (p\in u_0\iff p\in Z_0\land t\in p)\tag{4}$$

Now, from $(1)$, $x\in Z_0$ and from $(4)$, $x\in u_0$. OTOH, since $t\not\in y$ then $y\not\in u_0$. So there exists a set $u_0$ of which $x$ is a member and $y$ is not. This contradicts the assumption about $x, y$.

So for an axiom of extensionality it's enough to take $$\forall x\forall y (\forall z(z \in x \iff z \in y) \implies \forall z (x \in z \iff y \in z))$$ with the other direction following from pairing and comprehension.

Answer 3

As an addendum to everything that's been said so far, $=$ actually does not need to be interpreted as meta-level sameness. You can make $=$ follow other rules and get a semantics for first-order logic that's equivalent to the standard one.

This is less convenient than just making $=$ meta-level sameness. And, if done, you need to talk about meta-level sameness anyway via normal models. A normal model is just one where $=$ is interpreted as real sameness.

So, in a certain sense, sameness is unavoidable.

However, we can imagine taking first-order logic without equality and asking what we would have to assume about a binary relation $=$ in order to get it to behave as closely as possible to equality.

It must be a congruence with respect to every constant, function and relation symbol.

This condition can be imposed with some assumptions that can be encoded as first-order sentences.

1. $=$ is an equivalence relation.
2. For all constant symbols $c$, it holds that $[\forall x y](x = y \to (x = c \leftrightarrow y = c))$. (This is actually a consequence of $=$ being an equivalence relation, but is nice to call out explicitly)
3. For all relation symbols $R$ it holds that $[\forall \vec{x} \vec{y}](\vec{x} = \vec{y} \to (R(\vec{x}) \leftrightarrow R(\vec{y})))$, where $\vec{x} = \vec{y}$ abbreviaties $\vec{x}_1 = \vec{y}_1 \land \cdots \land \vec{x}_n = \vec{y}_n$
4. For all function symbols $f$ it holds that $[\forall \vec{x} \vec{y}](\vec{x} = \vec{y} \to f(\vec{x}) = f(\vec{y}))$.

The language of set theory has a single binary relation $\in$.

So, in a certain sense, extensionality alone doesn't nail down $=$ enough. We also need $=$ to be an equivalence relation and we need the following to hold:

$$ [\forall x y z w] ((x = y \land z = w) \to (x \in z \leftrightarrow y \in w)) $$

Answer 4

Seems like a key issue here is whether it’s allowed that two distinct sets compare as equal (C++ programming analogy: two instances of the std::complex type, at different memory locations, which compare as equal because they represent the same complex number)

In normal set theory (and hence OP’s Formulation 1) I believe this is impossible by definition, c.f. Suppes, Axiomatic Set Theory, section 1.2:

‘=‘ is taken as the sign of identity. The formula ‘x=y’ may be read as ‘x is the same as y’, ‘x is identical with y’…it is understood that equality means sameness of identity.

Or more concisely here:

If two terms are equal (i.e. they refer to the same object)

If the OP’s Formulation 2 actually is intended to allow two distinct sets to compare as equal, then it would imply the possibility that:

• $a \in X$ and $b = a$, but $b \notin X$

which would be a very weird new kind of set theory.

But if that’s not the intent, then the two formulations seem equivalent to me (though Formulation 1 seems a lot clearer)

Answer 5

Note: This answer is wrong, but I'll leave it here anyway because of the great comments of @Z.A.K.

You might be interested in first order logic and the ZF axioms of set theory, under which your Formulation 2 becomes the standard.

Equality becomes a logical notion. The ZF axiom of extensionality characterizes the notion of equality in set theory.

Answer 6

What's the definition of Primitive Notion? I'm inclined to say Set Equality is not a Primitive Notion if the latter is defined as the most primitive terms in an axiomatic system.

Any axiomatic system will have fundamental terms which can't be defined, otherwise you get an infinite regress. Further, you can't get more fundamental than the undefined terms. Consider defining Point, Set, and Plane in Euclidean Geometry.

In matters of set theory, we accept as undefined terms Set, Member/Element of. You can't get more primitive than that.

The question can be rephrased, is Set Equality as primitive as "Set"?

Both Formulation 1 and Formulation 2 stipulate a relationship using undefined terms. I'm thinking the need of stipulating the notion of Set Equality with those undefined terms necessarily implies the notion is less primitive than those basic terms. Thus we have Set Equality as a definition and not a Primitive Notion.

Other answers tell us that Set Equality can be represented as a modification of Extensionality, but Extensionality itself is stated in terms of more fundamental notions.

Definitions name a relationship between undefined terms necessarily specifying a subset of the fundamental structures involved.

Axioms establish relationships between fundamental entities without necessarily specifying a new term for entities.

So both Definitions and Axioms are less primitive than the undefined terms.

Theorems are proven using references to Definitions and Axioms, so they are less primitive than those.

So Set Equality is not among the most primitive notions in Set Theory, but is more primitive than any theorems.

I'm inclined to think Formulation 2 is unavoidable. Again, this all rests on the definition of "Primitive Notion".