A question about Quine's set theory NF. This question might not really be considered appropriate for mathoverflow.net but
I'll risk asking it and apologize in advance if I have commited a booboo. It is often
said that in NF one can prove the existence of infinite sets without the help of any
special axiom of infinity. Now Tarski's definition of an infinite set (which includes
more sets than Dedekind's definition when the axiom of choice is not available) states
that a set X is infinite just in case there exists a non-empty set T of subsets of X
such that if we are given any element u of T there is an element v of T which is a
proper subset of u. In order to prove that even the universal set V is infinite one
would need to exhibit a specific non-empty sub-cllection V* of V which is certified
to be a set in NF and is such that for every element y of V* there is an element z
of V* which is a proper subset of y. I have never seen a specific example of such a set
V* and cannot think of how to define one. Note that most infinite sub-collections of V
are not sets in NF because of the stratification requirements. Is there (an example of)
such a V* and if not how can one really say that NF proves the existence of infinite sets? 
 A: One can give stratified definitions for individual Frege-Russell natural numbers, and then so too for the set $\mathbb{N}$ of all Frege-Russell naturals, so that exists in NF. One can then check that the set $$\mathcal{T} = \{X\subseteq\mathbb{N} : \exists n\in\mathbb{N} (X = \mathbb{N}\setminus\{0,\dots,n\})\}$$ has a stratified definition, and so it too provably exists in NF. This $\mathcal{T}$ is the obvious candidate for witnessing that $\mathbb{N}$ is Tarski-infinite; we just need to know that NF proves it has the desired property.
The only sticking point for that would be showing that $$\mathbb{N}\setminus\{0,\dots,n+1\} \subsetneq \mathbb{N}\setminus\{0,\dots,n\}$$ for all $n$, and specifically that the inclusion really is proper, i.e. that none of our Frege-Russell naturals is empty. But this is where Specker's 1953 heavy lifting comes into play; namely, his proof that the universe $V$ cannot be well-ordered also implies that it is "Frege-infinite," i.e. $\forall n\in\mathbb{N} (V\notin n)$, because NF can prove that all Frege-finite sets are well-ordered. In turn, the fact that $V\notin n$ forall $n$ can be used to show that $n\ne\emptyset$ for all $n$, as required.
