# Can one exhibit an explicit Kuratowski infinite set without invoking Replacement?

The customary formulation of the Axiom of Infinity within Zermelo-Fraenkel set theory asserts the existence of an inductive set: a set $I$ with $\varnothing\in I$ such that $x\in I$ implies $x\cup\{x\}\in I$. Since the intersection of any nonempty set of inductive sets is itself inductive, an instance of the Axiom Schema of Separation implies the existence of a smallest inductive set, namely the set of von Neumann naturals $$\mathbb{N}_{\bf vN} = \{\varnothing, \{\varnothing\},\{\varnothing,\{\varnothing\}\},\ldots\}.$$

Any inductive set is infinite (in fact, Dedekind infinite) but this formulation of the axiom asserts more, namely the existence of a specific countably infinite set. Given one such set, the existence of others, for example the set of Zermelo naturals $$\mathbb{N}_{\bf Zer}=\{\varnothing,\{\varnothing\},\{\{\varnothing\}\},\ldots\}$$ follows from appropriate instances of the Axiom Schema of Replacement.

Consider the subsystem of Zermelo-Fraenkel set theory with axioms Extensionality, Separation Schema, Union, Power Set, Pair. Augment this Basic System with an Axiom of Infinity which asserts the existence of an infinite set, but not any particular one. Such a formulation requires that the notion of 'finite' be defined prior to that of 'natural number', following Kuratowski for example. Any infinite set $I$ determines a Dedekind-infinite set of local naturals $$\mathbb{N}_I=\{\mbox{equinumerosity classes of finite subsets of } I\}$$ which (duly equipped with initial element and successorship) yields a Lawvere natural number object, as in the Recursion Theorem. The existence of $\mathbb{N}_{\bf vN}$ and $\mathbb{N}_{\bf Zer}$ then follow from appropriate instances of Replacement.

One might wonder if there is some clever way to specify an infinite set without recourse to Replacement. That is, does there exist (in the language of set theory) a formula $\boldsymbol \phi$ with one free variable $x$ such that
$$\mbox{Basic+Infinity+Foundation } \vdash\; \exists y ( \forall x (x\in y \leftrightarrow \boldsymbol \phi)\,\wedge \, y \mbox{ is infinite})\>?$$

I'm inclined to guess no, on the following circumstantial grounds:

• For $\mathbb{N}_{\bf vN}$ and $\mathbb{N}_{\bf Zer}$ the use of Replacement is essential: Mathias has shown (Theorem 5.6 of Slim Models of Zermelo Set Theory that there exist transitive models ${\mathfrak M}_{\bf vN}$ and ${\mathfrak M}_{\bf Zer}$ of Basic+Infinity+Foundation with ${\mathbb N}_{\bf vN}\in {\mathfrak M}_{\bf vN}$ and ${\mathbb N}_{\bf Zer}\in{ \mathfrak M}_{\bf Zer}$, but such that every element of ${\mathfrak M}_{\bf vN}\cap {\mathfrak M}_{\bf Zer}$ is hereditarily finite.

• The usual definitions of $\mathbb{N}_{\bf vN}$ and $\mathbb{N}_{\bf Zer}$ involve unstratified formulas. Coret has shown (Corollary 9 of Sur les cas stratifiés du schéma du replacement) that this is unavoidable: $$\mbox{Basic+Infinity } \vdash\; \forall y ( \forall x (x\in y \leftrightarrow \boldsymbol \phi)\,\rightarrow \, y \mbox{ is hereditarily finite})$$ for any stratified $\boldsymbol \phi$. Using the same technique he has shown (Corollary 10) that Basic+Infinity proves every stratified instance of Replacement.

-
Could you clarify what precisely the notion of finite is that you use in stating your axiom of Infinity? (You say "following Kuratowski", but I'm not sure exactly what you mean...) – Joel David Hamkins Jan 2 '13 at 22:25
A natural definition for finiteness of $X$ (equivalent to the usual characterisation by natural numbers, without AC) is the one defined by Tarski: Every nonempty subset of the power set has a maximal element. – Goldstern Jan 2 '13 at 22:27
Can you motivate why you would be interested in such a system that appears to be too weak to prove the existence of certain very basic and natural objects? – Goldstern Jan 2 '13 at 22:31
Kurotowski finite. Thanks for the edits, Sev. Could you or someone fix the last bit of latex? I'm afraid I'm still new to this. – Adam Epstein Jan 2 '13 at 22:33
Sorry if I stepped on anyone else's edits, but I wanted to help out and fix the LaTeX. Adam, you need to use markdown formatting ( stackoverflow.com/editing-help ) to do things with text, only a limited set of LaTeX commands are available in MathJax ( mathjax.org ). – Zev Chonoles Jan 2 '13 at 22:35