Essentially, I want to prove that $\forall x(x \notin x)$. I'm not sure where to begin with this. I have tried manipulating the axiom of specification to achieve this, as my guess is this is the axiom that enforces this (given it's purpose of eliminating Russell's paradox and the set of all sets, etc.).
In fact, I am trying to prove this statement as part of proving that the set of all sets doesn't exist. Here's my planned method:
- Assume that the set of all sets exist. From this I can derive $\exists x(x \in x)$
- Prove $\forall x(x \notin x)$, from which it follows that $\neg \exists x(x \in x)$
- A contradiction arises, disproving the assumption in 1.
I am working through a set theory book, and trying to write proofs to satisfy myself that various statements in the book are true. For all I know, this might be proven further in the book, and may require further axioms that I have not yet encountered. At this point the only axioms I have are extensionality and the axiom schema of specification. Perhaps I need other axioms not yet encountered?
You need the axiom of regularity to prove your statement. The axiom of regularity states every non-empty set has a $\in$-minimal element in the following sense: if $x\in A$ is a $\in$-minimal element of $A$ then no $y\in x$ satisfy $y\in A$.
Now you can prove your statement as follows: assume that there is $x$ such that $x\in x$. Take $A=\{x\}$, then $A$ must have a $\in$-minimal element. As $A$ is singleton, such $\in$-minimal element must be $x$. However it is impossible, since $x\in x$ satisfies $x\in A$.
(In fact, you can prove stronger theorem: the axiom of regularity proves there is no $\in$-descending chain. That is, there is no sequence $\langle x_n \mid n=0,1,2\cdots\rangle$ such that $x_0\ni x_1\ni x_2\ni\cdots$.)
Axiom of regulariry is necessary to prove the statement. Assuming there is a set $q$ such that $q=\{q\}$ does not derive any contradiction under ZFC without regularity. (A set $q$ such that $q=\{q\}$ is known as Quine atom.)