Are there functions that meet the function definition but cannot be written as a formula or expression?

Take two sets A and B. A function f: A -> B is nothing more than a subset of the Cartesian product A x B satisfying a certain simple condition (every input has exactly one associated output). So every choice of such a subset gives a function.

I emphasized the word choice because this is a strange thing to describe in set theory. In fact, even in the “simple” case where A and B are both the set N of natural numbers, we need the axiom of choice to guarantee the existence of most functions.

Said differently, it is a happy accident that some functions between infinite sets can be described algorithmically. The overwhelming majority only exist due to the axiom of choice - math is actually weirder and harder if they don’t exist, so we insist that they do.

/r/math Thread