set theory without the axiom of choice (AC) (usually denoted "ZF"). The full strength of AC is not needed to prove the equivalence; in fact, the equivalence of the two definitions is strictly weaker than the axiom of countable choice (CC). (See the references below.) 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 countably infinite subset; there exists an injective map from a countably infinite set to A; there is a function that is injective but not surjective; there is an injective function , where N denotes the set of all natural numbers; it is dually Dedekind-infinite if: there is a function 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. History The term is named after the German mathematician Richard Dedekind, who first explicitly introduced the definition. It is notable that this definition was the first definition of "infinite" that did not rely on the definition of the natural numbers (unless one follows Poincaré and regards the notion of number as prior to even the notion of set). Although such a definition was known to Bernard Bolzano, he was prevented from publishing his work in any but the most