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 nonempty 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 nonempty subcllection 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 subcollections 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?

One can give stratified definitions for individual FregeRussell natural numbers, and then so too for the set $\mathbb{N}$ of all FregeRussell 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 Tarskiinfinite; 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 FregeRussell naturals is empty. But this is where Specker's 1953 heavy lifting comes into play; namely, his proof that the universe $V$ cannot be wellordered also implies that it is "Fregeinfinite," i.e. $\forall n\in\mathbb{N} (V\notin n)$, because NF can prove that all Fregefinite sets are wellordered. In turn, the fact that $V\notin n$ forall $n$ can be used to show that $n\ne\emptyset$ for all $n$, as required. 

