Can it be proven in $\sf ZF^{\neg\infty}$ that the sets $x_n=\{x_{n+1}\}$ do not exist?

This question is my attempt to hone in on the problem of proving the strong form of the Axiom of Regularity $A\neq\emptyset\to\exists x\in A(x\cap A=\emptyset)$ (where $A$ is an arbitrary class) from the weak form $\forall a\!:a\neq\emptyset\to\exists x\in a(x\cap a=\emptyset)$. In ZF with the negation of the Axiom of Infinity (which I abbreviate as $\sf ZF^{\neg\infty}$), all sets have finitely many elements, and this allows us to prove that sets like $x=\{\{\{x\}\}\}$ do not exist, but I don't see how to prove that the infinite family $x_n=\{x_{n+1}\}$ does not exist, since I can't collect all the elements together and use regularity on that, since the resulting class is (provably) not a set.

My ultimate goal is to prove that every set has a transitive closure (that is a set), but these sets will foil my attempt if I can't prove their non-existence. Conversely, supposing I couldn't prove this, this would mean that $\infty$ is required for the proof, so could I turn it around and prove, given that every set has a transitive closure, that $\omega\in V$?

Mario,

I finally found a reference that addresses the issue you have identified.

("I found", he says. I asked at the Set Theory community on Google+, and was provided with a perfect reference.)

The theory you call $\mathsf{ZF}^{\lnot\infty}$ is not strong enough to prove the existence of transitive closures. This is the reason why the theory is usually formulated with foundation (regularity) replaced by its strengthening of $\in$-induction, namely the scheme that for every formula $\phi(x,\vec y)$ adds the axiom $$ \forall \vec y\,(\forall x\,(\forall z\in x\,\phi(z,\vec y)\to\phi(x,\vec y)\to\forall x\,\phi(x,\vec y)). $$

Over the base theory $\mathsf{BT}$ consisting of (the empty set exists), extensionality, pairing, union, comprehension, and replacement, one can prove that for any $x$, there is a transitive set containing $x$ iff there is a smallest such set, that is, there is a transitive set containing $x$ iff its transitive closure exists.

Over $\mathsf{BT}$ plus foundation, the scheme of $\in$-induction is equivalent to the statement $\mathsf{TC}$ that every set is contained in a transitive set.

Unfortunately, as I claimed above, $\mathsf{ZF}^{\lnot\infty}$ cannot prove the existence of transitive closures. To see this, start with $(V_\omega,\in)$, the standard model of $\mathsf{ZF}^{\lnot\infty}$. Let $$ \omega^\star=\{\{n+1\}\in V_\omega\mid n\in\omega\}. $$ Define $F:V_\omega\to V_\omega$ by $$ F(n)=\{n+1\},F(\{n+1\})=n $$ for $n\in\omega$, and $F(x)=x$ for $x\notin\omega\cup\omega^\star$. Now define a new "membership" relation by $$ x\in_F y\Longleftrightarrow x\in F(y) $$ for $x,y\in V_\omega$. It turns out that $$ (V_\omega,\in_F)\models\mathsf{ZF}^{\lnot\infty}+\lnot\mathsf{TC}. $$ In fact, $\emptyset$ is not contained in any transitive set in this structure. (Note that $\emptyset$ is not the empty set of this model.)

All this and much more is discussed in an excellent little paper

Richard Kaye and Tin Lok Wong. On interpretations of arithmetic and set theory, Notre Dame Journal of Formal Logic, 48 (4), (2007), 497–510. MR2357524 (2008i:03075).

(The pdf linked to above has some additional information than the version published at the Journal.) The result that $\mathsf{ZF}^{\lnot\infty}$ is consistent with $\lnot\mathsf{TC}$, and the proof just sketched, are due to Mancini. For additional details, Kaye-Wong refers to

Antonella Mancini and Domenico Zambella. A note on recursive models of set theories, Notre Dame Journal of Formal Logic, 42 (2), (2001), 109-115. MR1993394 (2005g:03061).