Does the axiom of choice have any use for finite sets?

Question

It is well known that certain properties of infinite sets can only be shown using (some form of) the axiom of choice. I'm reading some introductory lectures about ZFC and I was wondering if there are any properties of finite sets that only hold under AC.

Answer 1

There are two remarks that may be relevant here.

(1) This depends on what you mean by "finite sets". Even for (infinite setts of) pairs the axiom of choice is does not follow from ZF if one looks at an infinite collection. This is popularly known as the "pairs of socks" version of AC which is one of the weakest ones.

(2) If you mean that the family of sets itself is finite, then AC can be proved in ZF by induction, i.e., it is automatic, but this is only true if your background logic is classical. For intuitionistic logic, the axiom of choice can be very powerful even for finite sets. For example, there is a theorem that the axiom of choice implies the law of excluded middle; in this sense the introduction of AC "defeats" the intuitionistic logic and turns the situation into a classical one.

Answer 2

The usual properties of finite sets are still true without the axiom of choice.

1. If $A$ is a finite set, then every function $f\colon A\to A$ is injective iff it is surjecitve iff it is bijective.

2. If $A$ is a finite set of non-empty sets, then there is a choice function from $A$.

3. If $A$ is a finite set, then every partial order on $A$ has a maximal element; every two linear orders on $A$ are isomorphic; etc.

4. The power set of a finite set is finite, and a subset of a finite set is finite.

All these proofs don't use the axiom of choice at all. However the axiom of choice comes into play at two points:

1. You have an infinite family of finite sets. Then you might need the axiom of choice in order to say something. But this is because we left the realm of finite sets, the family of sets is now infinite.

2. There are characterizations of finiteness which are not necessarily true anymore. There might be an infinite set $A$ such that every $f\colon A\to A$ is injective if and only if it is bijective, and so on.

   So now there are several notions of finiteness. The term "finite" in choiceless contexts usually means a set which is in bijection with a bounded set of natural numbers. And we can talk about finiteness using Dedekind's characterization with injective functions (as above), and there is a whole spectrum in between.