Editing Dedekind-infinite set (section)

==Dedekind-infinite sets in ZF==

A set ''A'' is '''Dedekind-infinite''' if it satisfies any, and then all, of the following equivalent (over '''ZF''') conditions:
*it has a [[countable set|countably infinite]] subset;
*there exists an injective map from a countably infinite set to ''A'';
*there is a [[function (mathematics)|function]] {{nowrap|''f'' : ''A'' → ''A''}} that is [[injective function|injective]] but not [[surjective function|surjective]];
*there is an injective function {{nowrap|''f'' : '''N''' → ''A''}}, where '''N''' denotes the set of all [[natural number]]s;
it is '''dually Dedekind-infinite''' if:
*there is a function {{nowrap|1=''f'' : ''A'' → ''A''}} that is surjective but not injective;
it is '''weakly Dedekind-infinite''' if it satisfies any, and then all, of the following equivalent (over '''ZF''') conditions:
*there exists a surjective map from ''A'' onto a countably infinite set;
*the powerset of ''A'' is Dedekind-infinite;
and it is '''infinite''' if:
*for any natural number ''n'', there is no bijection from {0, 1, 2, ..., n−1} to ''A''.

Then, '''ZF''' proves the following implications: Dedekind-infinite ⇒ dually Dedekind-infinite ⇒ weakly Dedekind-infinite ⇒ infinite.

There exist models of '''ZF''' having an infinite Dedekind-finite set.  Let ''A'' be such a set, and let ''B'' be the set of finite [[injective]] [[sequences]] from ''A''. Since ''A'' is infinite, the function  "drop the last element" from ''B'' to itself is surjective but not injective, so ''B'' is dually Dedekind-infinite.  However, since ''A'' is Dedekind-finite, then so is ''B'' (if ''B'' had a countably infinite subset, then using the fact that the elements of ''B'' are injective sequences, one could exhibit a countably infinite subset of ''A'').

When sets have additional structures, both kinds of infiniteness can sometimes be proved equivalent over '''ZF'''. For instance, '''ZF''' proves that a well-ordered set is Dedekind-infinite if and only if it is infinite.