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.

  • 1
    $\begingroup$ 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...) $\endgroup$ Jan 2, 2013 at 22:25
  • 3
    $\begingroup$ 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. $\endgroup$
    – Goldstern
    Jan 2, 2013 at 22:27
  • 1
    $\begingroup$ 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? $\endgroup$
    – Goldstern
    Jan 2, 2013 at 22:31
  • 1
    $\begingroup$ This question seems to be a great one. (I say "seems to be" only because I am not an expert in set theory.) But I request that you modify the title. Titles on MO can be as long as text messages, and proper style is to include in your title a complete short version of your question. The current title, "Explicit Infinite Set", says very little about the question. You could instead use something like "In a version of ZF without Replacement, can an explicit infinite set be constructed from its implicit existence?" Or perhaps some variation better captures your question... $\endgroup$ Jan 3, 2013 at 5:44
  • 1
    $\begingroup$ @Goldstern See Kunen, Chapter IV Exercise (9) $\endgroup$ Jan 3, 2013 at 23:40

1 Answer 1


The answer is no. Let ZC' be ZFC without replacement and infinity and with the assertion there is a Kuratowski infinite set. We will construct a model $M$ of ZC' such that only hereditarily finite elements of $M$ are fixed under all automorphisms of $M.$ The idea is generate a model from a $\mathbb{Z}^2$-array of objects, each of whose only element is the object below it in the array.

Define $M=\bigcup_{m<\omega} \bigcup_{n \in \mathbb{Z}} \mathcal{P}^m(\{\omega\} \times \mathbb{Z} \times [n, \infty)),$ where we adjust the $\mathcal{P}$ operator to replace each singleton of the form $\{(\omega, n_1, n_2)\}$ with $(\omega, n_1, n_2+1).$ (We use $\omega$ to differentiate the $\mathbb{Z}^2$ objects from the hereditarily finite sets).

Define a relation $E$ on $M$ by $E \restriction \mathbb{Z}^2=\{((\omega, n_1, n_2),(\omega, n_1, n_2+1)): n_1, n_2 \in \mathbb{Z}\}.$ Extending $E$ to the iterated power sets is done in the natural way. It is easy to see $(M, E)$ satisfies ZC'.

Notice that the map $(\omega, n_1, n_2) \mapsto (\omega, n_1, n_2+1)$ extends to a unique automorphism on $M,$ which only fixes hereditarily finite elements. Thus, none of the infinite sets in the model are first-order definable.

Update: The author of this question was curious whether there is such a model which also satisfies transitive containment (TC), the assertion that every set has a transitive closure. The answer is yes; here's a sketch of such a model.

Assume ZFC + "there are non-OD reals" in $V$ (or work in a ctm satisfying a sufficiently large finite fragment of this theory). We'll build an OD model $M$ of ZC'+TC such that, from every infinite element $x,$ we can define (in $V$) a non-OD real $r.$ Then $x$ is not definable in $M,$ or else we would have an ordinal definition for $r.$

For $r \in \mathbb{R} = \mathcal{P}(\omega),$ we recursively define $n_r$ by $0_r=\emptyset$ and $(n+1)_r =\{n_r\}$ if $n \not \in r,$ and $(n+1)_r = \{n_r, \emptyset\}$ if $n \in r.$ Basically, we're defining a new system of natural numbers for each real.

Let $M = \bigcup_{m=0}^{\infty} \bigcup_{S \in [\mathbb{R} \setminus OD]^{<\omega}} \mathcal{P}^m ( \{n_r: n<\omega, r \in S\} ).$

For each infinite $x,$ there are finitely many (and at least one) non-OD reals $r$ such that the transitive closure of $x$ contains every $n_r.$ The least such real is as desired. And it's routine to verify $M \models ZC'+TC.$

  • $\begingroup$ Hi, Eliot. Yes, one can build models of Z in this way. I arrived at a similar construction a few years after my post, but except for alluding to it here later on mathoverflow.net/questions/201718/… I never posted my own solution here. I did write up some notes, including the fiddly details about why the resulting structure is a model of Z. More generally, starting from any $\omega$-model of finite set theory (Z-Infinity+$\neg$Infinity), one may adjoin iterated powersets in a similar external fashion, $\endgroup$ Aug 5, 2019 at 19:58
  • $\begingroup$ possibly losing Foundation, of course, but when starting from a model built out of "hereditary singletons" one can cut back to the part whose "support" is bounded from below. Actually, what you write here mathoverflow.net/questions/314483/… is closer, since there you have only one chain of hereditary singletons. In your post above, you seem to have infinitely many such chains: is there a particular reason for this? $\endgroup$ Aug 5, 2019 at 20:19
  • $\begingroup$ I do think one needs to be a bit careful about specifying this adjusted $\mathcal P$ operation, since one must coherently perform the indicated replacements at every stage of the infinite process But it's straightforward to formulate and prove a lemma about extending an appropriate relational structure by an adjusted $\mathcal P$ operation, and then passing to the direct limit over $\omega$-many iterations. $\endgroup$ Aug 5, 2019 at 20:22
  • $\begingroup$ This past year I've been reorganizing my presentation as follows. Adjoin to Z an additional axiom $\mathfrak{S}\neq\emptyset \wedge \forall x\exists n\in\omega \bigcup^n x \subseteq \mathfrak{S}$ where $\mathfrak{S}$ is the class of hereditary singletons (and where $\omega$ may well be a proper class); note that this is a first-order assertion in the language of set theory. Then, much as you observe, the universe admits a definable automorphism which fixes only the elements of $V_\omega$ (the hereditarily finite sets, but this terminology clashes with my other use of "hereditary" $\endgroup$ Aug 5, 2019 at 20:37
  • 2
    $\begingroup$ The infinitely many chains might be extraneous. They're an artifact from a previous model. There should be models of ZC+TC without definable infinite sets. I'll email you a sketch I have in mind. $\endgroup$ Aug 6, 2019 at 11:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.