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?


  • $\begingroup$ If equality is a congruence relation w.r.t. the symbols of the language, then the first direction follows. The other direction is obvious (unless I am missing something), if for all terms $t$ we have $t[x/x_0]=t[x/x_1]$, then the term $x$ will give $x_0=x_1$. $\endgroup$ – Kaveh Aug 2 '10 at 22:44
  • $\begingroup$ On the other hand, if by the other direction you mean that $t[x/x_0]=t[x/x_1]$ for some specific term $t$ and not for all terms, then this direction is equivalent to that term being one-to-one and therefore this direction works only for those terms. In your example $t=\left\{x\right\}$, the term $t$ is a one-to-one function of $x$ and this can be proven in MK. $\endgroup$ – Kaveh Aug 2 '10 at 22:50

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\}$.

  • $\begingroup$ Thank you, I finally managed to write down a proof in the forward direction. But now, what about the other way around when $x_0$ and $x_1$ are two sets? $\endgroup$ – Francesco Turco Aug 2 '10 at 17:23
  • 3
    $\begingroup$ If $x_0$ and $x_1$ are sets and $\{x_0\}=\{x_1\}$ then $x_0\in\{x_0\}$ by 2,5,6; then $x_0\in\{x_1\}$ by 1; and then $x_0=x_1$ by 5,6. $\endgroup$ – Andreas Blass Aug 2 '10 at 19:19

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.

  • $\begingroup$ So defining $x=y$ as $\forall z\left(z\in x\leftrightarrow z\in y\right)$ is not enough? Should I say that two classes are equal if they also belong to the same classes, too? $\endgroup$ – Francesco Turco Aug 2 '10 at 17:27
  • $\begingroup$ @Francesco: that formula will still be enough in MK. It's automatic that two classes belong to the same classes, since classes can't belong to anything! To see why this formula works, note that without equality $- \in -$ is the only atomic formula, and so this says that $x$ and $y$ satisfy exactly the same atomic formulas, and hence satisfy all the same formulas; so this formula satisfies all the deductive rules for $=$ in FOL-with-equality; now use this fact to connect proofs in the standard set theory and proofs in a version where equality is defined by this. $\endgroup$ – Peter LeFanu Lumsdaine Aug 3 '10 at 0:05
  • 1
    $\begingroup$ @Francesco: I believe the only problem with your shorter definition of equality is that it turns the axiom of extensionality, as usually written, into a tautology. It should be sufficient if you also rewrite that axiom as $\forall x \forall y ( \forall z (z \in x \leftrightarrow z \in y) \rightarrow \forall w (x \in w \leftrightarrow y \in w) )$. Otherwise, though, you could end up with sets x and y and a set (or, in MK, a class) w such that x = y (according to your definition of "="), $x \in w$ but $y \not\in w$. That would not be good. $\endgroup$ – Ilmari Karonen Aug 3 '10 at 8:35

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.

  • $\begingroup$ Of course set theory, being a first-order theory, is not strong enough to define the true equality relation, it is just able to define an equivalence relation with many of the same properties, including substitutability of equals for equals. $\endgroup$ – Carl Mummert Nov 25 '12 at 13:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.