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$?

-
What is $ZF\lnot\infty$? – Asaf Karagila Jan 20 '13 at 17:45
@AsafKaragila $ZF\neg\infty$ is ZF with the Axiom of Infinity replaced with its negation "$\omega\notin V$". – Mario Carneiro Jan 20 '13 at 17:48
You should be able to use a compactness argument to show that after appending to the language of set theory the constant symbols $c_0 , c_1 , \ldots$ and adding as new axioms the statements "$c_n = \{ c_{n+1} \}$" the resulting theory is consistent (if the original one was). – arjafi Jan 20 '13 at 18:40
@ArthurFischer Yes, but this is irrelevant, because the sequence you build this way cannot be seen from within the model. – Andrés E. Caicedo Jan 20 '13 at 19:07
Mario, you can still prove that the set theoretic rank of each set exists (and is a natural number). This solves the problem, as there can be no sequence as you fear, or its elements would have no rank. – Andrés E. Caicedo Jan 20 '13 at 19:37

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).

-
Talk about incentives to join Google+... :-) – Asaf Karagila Jan 31 '13 at 8:33
Showing that your model satisfies ${\sf ZF}^{\neg\infty}$ looks to be difficult, but to show that it satisfies $\neg{\sf TC}$, note that $F(n)=\{n+1\}$ implies that $n+1\in_F n$, so we get $0\ni_F 1\ni_F 2\ni_F\dots$, and so the transitive closure is $\omega\notin V_\omega$. Nice references! – Mario Carneiro Jan 31 '13 at 9:14
@MarioCarneiro It is actually not difficult: If $F:V_\omega\to V_\omega$ is any bijection, then defining $\in_F$ as above gives a model of $\mathsf{ZF}^{\lnot\infty}$, except for foundation. Care is needed only to ensure that foundation holds (as in the example given above). Many other examples, and related topics, are discussed in "$\omega$-models of finite set theory", by Enayat, Schmerl, and Visser. – Andrés E. Caicedo Feb 27 '13 at 16:45