Posted by AKG:
Don't confuse choice functions with wellorderings.

I knew I was!!!
Posted by AKG:
And the function I gave before defines a wellorder on Z, but it is not a choice function. Given a collection C of nonempty sets, a choice function maps each S in C to an element of S. You can regard Z as a collection of sets, but the function isn't supposed to map each integer to an element of itself. If it is a choice function, it's entirely a coincidence. It is just supposed to help define a wellorder. A wellorder is a binary relation satisfying some certain properties. Given the function I defined, we can now define a relation R by:

I always doubted that we had actually defined a choice function. I remember reading somewhere that it was impossible to define a choice function for the integers without resorting to the AoC. Somewhere along the way I was caught up in the wellordering/choice function trap.