# There is no infinite sequence $x_1 \ni x_2 \ni x_3 \ni …$

We take the "usual" axioms of Zermelo-Fraenkel set theory (axiom of extensionality, axiom of the unordered pair, axiom of the sum set, axiom of the power set, axiom of the empty set, axiom of choice et cetera.) and assume that every set only ever contains other sets (except for $\emptyset$).

Can we prove that there is no infinite sequence $x_1 \ni x_2 \ni x_3 \ni ...$?

• No, we can't prove it. – Crostul Mar 5 '15 at 7:42
• @Crostul: Actually, that depends on how you read the question. – Asaf Karagila Mar 5 '15 at 7:55
• Is the question ambiguous? – Achilles Mar 5 '15 at 8:10
• @Achilles: It could be interpreted as asking if given a model of $\sf ZF$ it could be that it is not well-founded (externally); however internally it is always well-founded, as my answer shows. Namely, if there is a decreasing sequence like that, then it is not witnessed inside the model. – Asaf Karagila Mar 5 '15 at 8:47
• @Asaf Karagila: Thank you! – Achilles Mar 5 '15 at 9:10

One of the "usual" axioms of $\sf ZF$ is the axiom of regularity which states that there if $X$ is non-empty, then there is some $y\in X$ such that $y\cap X=\varnothing$.
Suppose that such a sequence would exist. What would it mean? It means there is a function $F$ whose domain is $\omega$ and $F(n+1)\in F(n)$. Using replacement, take $X$ to be the range of $F$, then there is no element of $X$ which is disjoint from it. Contradiction.
One should point out, however, that it is possible that there is a model of $\sf ZF$ which does have such a decreasing chain, but the function $F$ as above can never be an element of the model.