First-order logic without equality and set theory

Question

Is it possible to build set theory on first-order logic without equality?

For example, how could one show that if $x_0=x_1$ then $\left\{x_0\}=\{x_1\right\}$, where $x_0$ and $x_1$ are two sets? And the other way around? In my opinion, it is impossible using only the following facts:

1. axiom of extensionality: $x_0=x_1\leftrightarrow\forall x_2\left(x_2\in x_0\leftrightarrow x_2\in x_1\right)$
2. reflexivity of equality: $x=x$
3. symmetry of equality: $x_0=x_1\rightarrow x_1=x_0$
4. transitivity of equality: $x_0=x_1\land x_1=x_2\rightarrow x_0=x_2$
5. class comprehension: $x\in\left\{y:\psi\left(y\right)\right\}\leftrightarrow\text{set}\left(x\right)\land\psi\left(x\right)$
6. definition of singleton: $\left\{x\right\}=\left\{y:y=x\right\}$
7. definition of sethood: $\text{set}\left(x_0\right)\leftrightarrow\exists x_1\left(x_0\in x_1\right)$

I hope I didn't forget any fact. Also, it would be better if I point out I'm using Morse-Kelley set theory.

If I use first-order logic with equality, I could prove the first part of the theorem because for any term $t_0$ and $t_1$, if $t_0=t_1$ then $f\left(t_0\right)=f\left(t_1\right)$ ($f$ is a unary logical function here). But how can I prove the other way around?

Thanks.

Answer 1

The converse direction fails because, in Morse-Kelley set theory plus your facts, $\{x\}$ is empty whenever $x$ is a proper class. So $\{x_0\}=\{x_1\}$ for any two proper classes.

The forward direction, on the other hand, seems to follow immediately from the facts you listed. If $x_0=x_1$ then, since facts 2, 3, and 4 make equality an equivalence relation, any $y$ will be equal to $x_0$ iff it is equal to $x_1$. So by facts 5 and 6, $\{x_0\}$ and $\{x_1\}$ have the same members. Then by fact 1, $\{x_0\}=\{x_1\}$.

Answer 2

The short answer to the original question is simply yes, but the initial list of "facts" obscured that by stating the axiom of extensionality using an = sign. The point would be that if you are in first-order logic without equality, then you don't have an = sign, not in your axiom of extensionality or anywhere else either -- at least, not until after you define = .

In MK, NBG, and similar theories, "everything" is a class. A set is just a small class. The definition of equality between classes is the same regardless of whether either class is large (proper) or small (a set).

In all these theories, x=y is eliminable; it is simply an abbreviation for $[ x \subseteq y ] \land [ y \subseteq x]$ , or, equivalently, for $\forall z [z \in x \leftrightarrow z \in y ]$. This remains true even if the background logic does contain equality.

Hatcher's use of two biconditionals for this elimination/definition is overkill -- mutual subsets are all that is happening.

In the case where the background logic does contain equality, the eliminability-criterion above simply implies that the sets are equal (that implication is the axiom of extensionality). In the case where the background logic does not contain equality, the same condition implies instead that x and y belong to the same sets. So regardless of whether you are using ZFC, MK, NBG, or anything similar, we have two versions of the axiom of extensionality: Sets with the same members...

(with equality): $\forall z [z \in x \leftrightarrow z \in y ] \rightarrow x = y $ (...are identical)

(w/o equality): $\forall z [z \in x \leftrightarrow z \in y ] \rightarrow \forall w [x \in w \leftrightarrow y \in w ]$ (...are members of the same sets)

It is an important strength of set theory that you don't need equality in the underlying logic in order to use it (that it is strong enough to define equality). This is a hurdle that some alternative theories are not always able to clear.

Answer 3

At least for ZFC, Wikipedia says we can just define two sets as equal if they have the same elements and belong in the same sets (with the axiom of extensionality then stating that the former implies the latter):

If the background logic does not include equality, x = y may be defined as an abbreviation for the following formula (Hatcher 1982, p. 138, def. 1): $\forall z [ z \in x \Leftrightarrow z \in y] \land \forall z [x \in z \Leftrightarrow y \in z]$.

I'm not really familiar with MK, but I don't immediately see why a similar definition couldn't work there as well.