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?

2$\begingroup$ +1 for the word "booboo". $\endgroup$ – Todd Trimble♦ Sep 30 '12 at 19:05

2$\begingroup$ A proof that $V$ is infinite can be found in Tom Forster book Set Theory with a Universal Set, page 49, theorem 2.2.7. This proves the axiom of infinity. This is a theorem of Specker [1953]. $\endgroup$ – Rachid Atmai Sep 30 '12 at 21:03
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.

$\begingroup$ Many thanks to both of you for clearing up this situation so well for me. I was not thinking of FregeRussell natural numbers but rather of representing the natural numbers as finite towers of singletons starting with the singleton of the empty set. I have only one remaining question. Can Specker's proof be carried out within NF itself? $\endgroup$ – Garabed Gulbenkian Oct 1 '12 at 18:33

$\begingroup$ Yes, Specker carries out his proof within NF. His short paper on the matter is available online for free: pnas.org/content/39/9/972 It's fairly selfcontained, but it does appeal to some basic results established in Rosser's NFbased textbook Logic for Mathematicians. $\endgroup$ – Ed Dean Oct 2 '12 at 3:43

$\begingroup$ Quine was fond of pointing out that $V$ satisfied the Zermelo axiom of infinity by containing $\emptyset$ and $x \cup \{x\}$ for all $x$. The problem is that it's kind of a crap infinity if it doesn't satisfy something like the Dedekind or Tarski definition too. $\endgroup$ – Malice Vidrine Aug 13 '13 at 6:08