The context of this question is constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in IZF.

Let us say that a set $X$ is:

  • finite when there exists a natural number $n$ and a bijection $\{1,\ldots,n\} \to X$,

  • finitely enumerated when there exists a natural number $n$ and a surjection $\{1,\ldots,n\} \to X$,

  • subfinite when there exists a natural number $n$ and a bijection $D \to X$ for some subset $D \subseteq \{1,\ldots,n\}$,

  • subfinitely enumerated when there exists a natural number $n$ and a surjection $D \to X$ for some subset $D \subseteq \{1,\ldots,n\}$,

  • Dedekind-finite when every injection $X\to X$ is, in fact, a bijection.

Clearly, finite sets are finitely enumerated and subfinite, and finitely enumerated or subfinite sets are subfinitely enumerated, and it is not hard to give Brouwerian counterexamples to show that there are no further implications between these four notions. (However, a set $X$ is finite iff it is finitely enumerated and discrete, where “discrete” means that the diagonal $\Delta \subseteq X^2$ is a decidable subset.)

Also, finite sets are Dedekind-finite. But this leaves the question of which of the three remaining notions imply Dedekind-finiteness.

Note that a subset or a quotient of a Dedekind-finite set need not be Dedekind-finite: this is shown (by constructing appropriate topoi) in Stout, “Dedekind finiteness in topoi”, J. Pure Appl. Algebra 49 (1987) 219–225, but this paper doesn't say whether a subset or a quotient of a finite set need be Dedekind-finite.


Question: Is a finitely enumerated set necessarily Dedekind-finite? Is a subfinite set necessarily Dedekind-finite? Is a subfinitely enumerated set necessarily Dedekind-finite?

(As usual, the answer “these are well-known open questions” will be deemed satisfactory, but the mere fact that the answer does not appear on the nLab page on the subject is not quite sufficient.)

  • 1
    $\begingroup$ Do you know if Dedekind-finiteness is equivalent to the property that every surjection $X \to X$ is a bijection? $\endgroup$ Commented Oct 26, 2022 at 4:31
  • $\begingroup$ @JamesHanson No -- see Example 3.2 in Stout's "Dedekind finiteness in topoi" linked in the question statement for a Dedekind-finite object with a non-bijective epimorphic endomorphism, and Example 3.3 for an object with no non-bijective epimorphic endomorphism which is not Dedekind-finite. (That is, neither implication holds.) $\endgroup$
    – Tim Campion
    Commented Oct 26, 2022 at 4:52
  • $\begingroup$ @JamesHanson: That not even true in ZF. $\endgroup$
    – Asaf Karagila
    Commented Oct 27, 2022 at 8:18
  • $\begingroup$ For completeness: to provide a reference for the claim made in the last comment by @AsafKaragila (that dual Dedekind-finiteness is not equivalent to Dedekind-finiteness even in ZF), see Goldstern, “Strongly Amorphous Sets and Dual Dedekind Infinity”, which is referenced in an answer to this question concerning forms of finiteness in ZF (note: dual Dedekind finiteness is not one of the forms considered in the question). $\endgroup$
    – Gro-Tsen
    Commented Oct 27, 2022 at 8:43

1 Answer 1


Edited (2022-10-27): I had initially written an answer for the “subfinite” case only. Below is an adaptation of the technique to the “subfinitely enumerated” case, thus fully answering my question (positively).

Claim: a subfinitely enumerated set is Dedekind-finite.


Let $X$ be subfinitely enumerated: witnessing this, let $D \subseteq \{1,\ldots,n\}$ a subset and $h\colon D\to X$ be surjective. So for every $x\in X$ there is $\tilde x\in D$ such that $h(\tilde x) = x$: we call this $\tilde x$ a “representative” of $x$.

We wish to show that $X$ is Dedekind-finite. So let $f\colon X\to X$ be injective. Our goal is to prove (constructively!) that $f$ is surjective.

Let $x\in X$: we want to show that there is $z\in X$ such that $f(z)=x$. We let $(x_i)$ be defined by induction by $x_0 = x$ and $x_{i+1} = f(x_i)$: this defines $x_i\in X$ for all $i \in \mathbb{N}$.

Each $x_i$ has a representative $\tilde x_i$ in $D$. Now we're not assuming the countable axiom of Choice so we can't state that there is a sequence $\tilde x_i$ of such representatives, but finite Choice¹ is a theorem (easily proved by induction), so we can assert the existence of representatives $\tilde x_0,\ldots,\tilde x_n$ (in $D$, hence in $\{1,\ldots,n\}$) of $x_0,\ldots,x_n$.

Now $\{1,\ldots,n\}$ is finite, so the standard pigeonhole result is constructively valid: there are $i<j$ in $\{0,\ldots,n\}$ such that $\tilde x_i = \tilde x_j$. In particular, we have $h(\tilde x_i) = h(\tilde x_j)$, that is, $x_i = x_j$. By injectivity of $f$ (and therefore of $f^{\circ i}$), we get $x_{j-i} = x_0$, in other words $f(x_{j-i-1})=x_0$.

So $z := x_{j-i-1} \in X$ is the desired preimage of $x$ and this proves surjectivity. ∎

  1. Lest there be any doubt, “finite Choice” is the statement that if $h\colon D\to X$ is surjective, and $F$ is finite (here we use $\{0,\ldots,n\}$), then the map $D^F \to X^F$ taking $(d_i)_{i\in F}$ to $(h(d_i))_{i\in F}$ is also surjective.
  • $\begingroup$ I should have mentioned before -- "subfinitely-enumerated" is often called "Kuratowski-finite". According to Stout (see p. 2 of his paper) Acuna-Ortega showed that every decidable Kuratowski-finite object in a topos is Dedekind-finite. So your result here drops the decidability hypothesis. (I think "decidable" is meant to mean that the diagonal is decidable? So it means "discrete" in the sense given in your question statement.) $\endgroup$
    – Tim Campion
    Commented Oct 27, 2022 at 18:30
  • $\begingroup$ If you have a surjective endomorphism of a Kuratowski-finite object, must it be a bijection? $\endgroup$
    – Tim Campion
    Commented Oct 27, 2022 at 18:38
  • $\begingroup$ @TimCampion I think Kuratowski-finite (or $K$-finite), at least as defined in the Elephant, is what I called “finitely enumerated”, and $\tilde K$-finite is what I called “subfinitely enumerated”. But whatever the terminology, it is indeed worth asking which of the four properties implies “dual-Dedekind-finite” (in the sense that every endo surjection is a bijection). I'll see if I can work this out too. $\endgroup$
    – Gro-Tsen
    Commented Oct 27, 2022 at 20:12
  • $\begingroup$ @TimCampion. No, because a subset of a Kuratowski-finite (=finitely enumerated as above) is only K-finite if it is a decidable subset. Consider subsets of the singleton. Kuratowski's beautiful short paper was in the first volume of the Polish journal Fundamenta Mathematicae. $\endgroup$ Commented Nov 1, 2022 at 13:58

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.