The axiom of replacement is usually used to prove the existence of large sets, to provide a reflection principle, for transfinite recursion… However, I am wondering how it affects finite sets. Let me give two concrete questions (let S be ZF without replacement and without infinity, SF=S+replacement, Z=S+infinity):

  • Are there theorems in SF+“every set is finite” which cannot be proved in S+“every set is finite”? In an alternative formulation: Does S+“every set is finite” imply the axiom of replacement? If not: Is there some instructive construction which fails?
  • Assume we are working in Z or ZF and consider the set $HF$ of all hereditarily finite sets: Are there “natural” statements about $HF$ which can be proved in $ZF$ but not in $Z$? (of course there are such statements, namely in $ZF$ we can prove that $HF$ is a model of some first-order statements expressing that $Z$ plus any given finite fragment of $ZF$ is consistent (and some similar statements), but I am looking for different properties)

“Finite” should be defined using natural numbers, which are Dedekind finite ordinals. Feel free to use strong versions of foundation for the first question. If something interesting happens with the negation of such an axiom, it would be interesting, too.


  • 3
    $\begingroup$ One issue is that when you drop the axiom of infinity, then various ordinarily-equivalent formulations of foundation become inequavalent. For example, asserting that every set has a $\in$-minimal element is weaker than $\in$-induction scheme without infinity. The latter proves that every set has a transitive closure, but the former is consistent with the failure of this, by a theorem of Ali Enayat (mentioned elsewhere here on MO). So your descriptions of the theories may be ambiguous, unless you state exactly which formulations of the axioms you are using. $\endgroup$ Aug 7, 2013 at 1:05
  • $\begingroup$ See mathoverflow.net/a/63918/1946. $\endgroup$ Aug 7, 2013 at 1:08
  • 8
    $\begingroup$ I expect that, with a suitable formulation of finiteness, it should be possible to deduce replacement from "all sets are finite". Specifically, it should be possible to prove by induction on $n$ that replacement holds when the "domain" of the replacing "function" is an $n$-element set. $\endgroup$ Aug 7, 2013 at 1:10
  • $\begingroup$ Thanks for the comment, I had the “every set has a disjoint element”-formulation in mind. However, I think I will not stick to some formulation. I will add a remark in the question. $\endgroup$
    – The User
    Aug 7, 2013 at 1:15
  • $\begingroup$ One issue about notation, $Z$ usually denotes Zermelo's set theory which is $\sf ZF$ without regularity and replacement (but with separation). $\endgroup$
    – Asaf Karagila
    Aug 7, 2013 at 2:23

2 Answers 2


I claim that replacement is provable in the theory SF+"every set is finite". One proves any instance by induction on the size of the domain of the function. That is, a given instance of replacement says that if $A$ is a set and we have for every $a\in A$ a unique $b$ such that $\varphi(a,b)$, then the set $\{b\mid \exists a\in A\, \varphi(a,b)\}$ is a set. Suppose this is true for all sets smaller than $A$. Now, remove one element from $A$, apply the induction hypothesis, and then add in the missing $b$.

So the answer to your first question is yes.

  • $\begingroup$ Ah, I see upon posting my answer that Andreas made the same point in a comment... $\endgroup$ Aug 7, 2013 at 1:15

In his paper "Finite-to-one maps" [ Journal of Symbolic Logic 68 (4):1251-1253 (2003) ], Thomas Forster proves the following result:

If there exists a surjection from the power set of $X$ to $X$ with all fibres finite then $X$ is itself finite.

Forster proves this result in ${\bf ZF}$, by an argument which makes manifest use of Replacement. He poses the question as to whether or not this is in fact a theorem of $\bf Z$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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