How would you prove in FOL that x is a member of {x} for all x?

Question

How can I formulate and prove the following in first-order logic?

$$\forall x (x\in \{x\})$$

I have the following two statements:

1. member(x,$\alpha$)
2. $\neg \exists y(\text{member}(y,\alpha )\land x\neq y)$

The latter means, of course, that there does not exist another member of $\alpha$ distinct from $x$. That is, $x$ is the only member of $\alpha$.

However, while this seems to establish $\alpha$ as {$x$}, it does not seem to get me any closer to proving that every x is a member of the set containing only itself.

What am I doing wrong? Do I need to use axioms of set theory in this proof? I am familiar with the NBG (Von Neumann–Bernays–Gödel) axioms. Which axioms are needed, and how?

Answer 1

Much of this comes down to exactly how you define $\{x\}$. In the usual formalization of set theory, the language does not actually contain the $\{$ and $\}$ symbols, and writing $x\in\{x\}$ is actually to be understood as an abbreviation for $$ \exists y(x\in y\land y=\{x\}) \qquad\text{or}\qquad \forall y(y=\{x\}\to x\in y) $$ where $y=\{x\}$ again abbreviates something like $\forall z(z\in y\leftrightarrow z=x)$ and the difference between the $\exists$ and $\forall$ versions is immaterial once you prove (from the axioms) that there is always exactly one $y$ such that $y=\{x\}$.

Thus, unfolded, the claim you want to prove is something like $\forall x \forall y(\forall z(z\in y\leftrightarrow z=x)\to x\in y)$ which is itself provable as a matter of logic, without needing any additional axioms.

---

However, usually one doesn't really do this. Instead one starts by proving a metatheorem about adding new function and predicate signs: If, using our axioms, we can prove $\forall x\exists_1 y(\varphi(x,y))$, then it is acceptable to add a new function symbol $f$ and the axiom $\forall x(\varphi(x,f(x))$. Here "acceptable" means that the extended theory is a conservative extension of the old, in that if the new theorem proves a sentence that doesn't involve $f$ then the original theory proves it too.

Now use the metatheorem on $\varphi(x,y)\equiv \forall z(z\in y\leftrightarrow z=x)$, and introduce a new function $f$, which for typographical convenience we write $\{\cdot\}$. Then we get the new axiom $$ \forall x\forall z(z\in\{x\}\leftrightarrow z=x) $$ If we instantiate both of $x$ and $z$ to the same variable $u$ (which will be allowed by whichever $\forall$-elimination rule your logic has) the axiom gives us $$ u\in\{u\}\leftrightarrow u=u $$ $u=u$ as a matter of logic, so we have $u\in\{u\}$ which we can generalize to get $\forall u(u\in\{u\})$, as desired.

---

In NBG, the defining property for $\{\cdot\}$ would include "... and $\{x\}$ is a set", but that doesn't fundamentally change the above discussion.

Answer 2

Along the lines suggested by Henning, we can let $U$ be domain of quantification. We can then think of $\{x\}$ as an operator/function mapping $U$ to the $P(U)$. Such a function can be constructed using the power set, Cartesian product and subset rules of ordinary set theory such that $\forall a,b\in U: [a\in \{b\}\iff a=b]$. Then, of course, $\forall x\in U: x\in \{x\}$ as required.