Are finitely enumerated and subfinite sets Dedekind-finite?

Question

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.

So:

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.)

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.

Proof:

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.