What is the set-theoretic definition of a function? I'm reading through Asaf Karagila's answer to the question What is the Axiom of Choice and Axiom of Determinacy, and while reading the explanation of Bertrand Russell's analogy ("The Axiom of Choice is necessary to select a set from an infinite number of socks, but not an infinite number of shoes.") at the bottom, I realized I'm a little confused by what a function actually is in set-theoretic terms (and probably confused by some other things, too).
Basically, my confusion is this:


*

*I thought that a function was specified by a finite string.

*Thus, the reason that we need the Axiom of Choice to select a set from an infinite number of socks is that there's no way to define a choice function on an infinite number of socks using only a finite string.

*However, if our universe is the set of natural numbers, aren't there an uncountable number of functions defined on our universe, but only a countable number of finite strings?


Where am I going wrong? What's the precise definition of a function, and what's the problem with my thinking in my last bullet point?
 A: A function $f$ from $A$ to $B$ is usually defined as a subset of $A \times B$ with the property that for each $a \in A$ there is a unique $b \in B$ such that $(a,b)$ is in the subset. In symbols:
$$f \colon A \longrightarrow B \Leftrightarrow f \subset A \times B \land \forall a \in A \exists ! b \in B . (a,b) \in f.$$
In fact, sometimes a function is defined as a triple $(f,A,B)$ where $f$ is as before, i.e. it comes tagged with its domain and range; but this is not the usual definition in set theory.
If $A,B$ are proper sets then the set of all functions from $A$ to $B$ exists (axiom chase).
A definable function (in some context) is given by a "textual" definition, and there are only countably many of those. There are different definitions of definability, e.g. Gödel's one, computable functions (when it applies) and so on.
A: A common definition of function between two sets (or between two classes, when working in GBN) is based on the notion of "ordered pair". An ordered pair is some set-theoretic construction, denoted "$(a,b)$" where $a$ and $b$ are sets, with the property that
$(a,b)=(c,d)$ if and only if $a=c$ and $b=d$. There are many ways of achieving this; the most common is the Kuratowski definition of ordered pair:
Definition. If $a$ and $b$ are sets, then the ordered pair $(a,b)$ is the set
$$(a,b) = \Bigl\{ \{a\}, \{a,b\}\Bigr\}.$$
Note that $(a,b)$ is a set if $a$ and $b$ are sets. The Axiom of Pairing guarantees the existence of a set $P$ that contains $a$ and $b$ as elements; and then both $\{a\}$ and $\{a,b\}$ are elements of the power set of $P$, so $(a,b)$ is an element of the power set of the power set of $P$. Also:
Theorem. $(a,b) = (c,d)$ if and only if $a=c$ and $b=d$.
Proof. If $a=c$ and $b=d$, then $(a,b)=(c,d)$. Assume now that $(a,b)=(c,d)$. Then
$$\{a\} = \cap(a,b) = \cap(c,d) = \{c\},$$
so $a=c$. If $b=a$, then $(c,d) = (a,b) = \{\{a\}\}$, so $\{c,d\}=\{a\}$, hence $d=a=b=c$. Likewise, if $d=c$, then $a=b=c=d$. 
If $a\neq b$ and $c\neq d$, then $\{b\} = \cup(a,b) - \cap(a,b) = \cup(c,d)-\cap(c,d) = \{d\}$, so $b=d$. QED
Now let $A$ and $B$ be sets (classes if you are in GBN). The cartesian product $A\times B$ of $A$ and $B$ is defined to be
$$A\times B = \{ (a,b) \mid a\in A, b\in B\}.$$
If $A$ and $B$ are sets, then so is $A\times B$: it is an element of $\mathcal{P}(\mathcal{P}(\mathcal{P}(A\cup B)))$. 
Now we are ready:
Definition. Let $A$ and $B$ be sets (or classes). A function $f\colon A\to B$ is a subset (or subclass) $f\subseteq A\times B$ such that:


*

*For all $a\in A$ there exists $b\in B$ such that $(a,b)\in f$; and

*For all $a\in A$ and $b,b'\in B$, if $(a,b)\in f$ and $(a,b')\in f$, then $b=b'$.


The idea is that $f$ "assigns" $a\in A$ to $b\in B$ if and only if $(a,b)\in f$. In that case, we write $f(a)=b$ (to mean $(a,b)\in f$). 
The problem with your last bullet point is really the first bullet point. You seem to be confusing "function" with "function you can name".
The problem with the Axiom of Choice is more subtle than the notion of "being able to write down something". For example, if you restrict your universe to the "constructible sets" (see Wikipedia's article) of ZF (without assuming AC), then the Axiom of Choice is true for the constructible sets. 
A: Some authors say that the subset of $A\times B$ is the graph of a function and define a function to be an object with three parts as follows.


*

*A set $D$ called the domain

*A set $R$ called the range

*A rule f tying each element $x\in D$ to a specific $f(x)\in R$


In this case we write $f:D\rightarrow R$.
