ZF + (Weak Axiom) $\vdash$ Dedekind Finite Implies Finite (Direct Proof)

Question

I've seen the proof of the contrapositive in ZF using the axiom of countable choice, but I am wondering if direct proofs have been made with the help of some other 'weaker' axiom, perhaps one that a constuctivist might like.

Answer 1

It is true, ZF + "Every Dedekind finite set is finite" is not enough to prove the axiom of countable choice. But it is enough to prove that countable unions of finite sets is countable.

On the other hand, countable unions of countable sets are countable neither follow nor implies that every Dedekind-finite set is finite. In the Cohen model, there is a Dedekind-finite set of reals, but every countable union of countable sets is countable.

So the exact strength of this statement has no reasonable equivalent of choice principles. The proof using the axiom of countable choice is "not that direct", by the way. The natural and obvious proof is going through Dependent Choice, which is in fact strictly stronger.

The proof using countable choice would be as follows: If $A$ is an infinite set, look at $S_n$ the set of all injective functions from $n$ into $A$, by assumption of infinitude none of them are empty. Using countable choice, let $s$ be a choice function, so $s_n\in S_n$ is an injective function.

Finally, define by recursion $f(n)=s_n(k)$ where $k=\min\{i\mid s_n(i)\neq f(j),\forall j<n\}$. This is well-defined since $s_n$ is a sequence of length $n$, and until that point we only defined $n-1$ elements.