Need example from number theory

[Mario Carneiro]

Here's an example that caused me significant difficulty when formalizing an
AC-free proof. It was trivial to derive the result using AC but rewriting
it to avoid AC involved formalizing a whole extra theory. It might be too
advanced for undergraduates though, depending on how much set theory they
have been exposed to.

It is known that for any infinite set X, X x X is equinumerous to X. In
this version, it is equivalent to the axiom of choice, but if we restrict
to well ordered sets or ordinals X then this is provable in ZF. The classic
proof due to Goedel is, for a cardinal number k, to construct an ordering
of k x k that has order type k, going by diagonals. This is then extended
to arbitrary ordinal numbers alpha by picking a bijection from alpha to
|alpha| and thus constructing a bijection from alpha x alpha to alpha.

So far, we've stayed in ZF. The hard part is now: construct a bijection
*uniformly* from alpha x alpha to alpha. One way to formalize this is to
say that we want to prove the existence of a family of bijections f(alpha)
such that for all infinite ordinals alpha < k (where k is some bound),
f(alpha) : alpha x alpha -> alpha is a bijection. This essentially requires
choice if you use the Goedel proof, because "pick a bijection" step can be
done in ZF for an individual ordinal alpha but needs choice to do the same
on a whole family.

However, the theorem is nevertheless true in ZF. The key is to write alpha
in cantor normal form and reverse all the factors, whereupon all addends
are absorbed into the last and you end up proving that alpha ~ omega^beta
for some beta (uniformly); then you can use the Goedel proof to show that
omega^beta x omega^beta ~ omega^beta (uniformly) and conclude. Formalizing
this proof requires lots of facts about cantor normal form that you would
never have guessed could get involved by looking at the Goedel proof.

Mario

On Sat, Aug 28, 2021 at 2:50 PM JOSEPH SHIPMAN <joeshipman at aol.com> wrote:

> What is an example of a theorem of number theory which has a well-known
> proof *suitable for undergraduates*, that uses the Axiom of Choice in a way
> that is not obviously unnecessary?
>
> We know that AC can be eliminated from the proof of any arithmetical
> statement, but I’d like an example I can easily explain.
>
> — JS
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210828/f261ecf5/attachment-0001.html>