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?
-
2$\begingroup$ +1 for the word "booboo". $\endgroup$– Todd TrimbleCommented Sep 30, 2012 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 AtmaiCommented Sep 30, 2012 at 21:03
1 Answer
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.
-
$\begingroup$ Many thanks to both of you for clearing up this situation so well for me. I was not thinking of Frege-Russell 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$ Commented Oct 1, 2012 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 self-contained, but it does appeal to some basic results established in Rosser's NF-based textbook Logic for Mathematicians. $\endgroup$– Ed DeanCommented Oct 2, 2012 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$ Commented Aug 13, 2013 at 6:08