I am wondering what is the best / agreed upon way to define functions of arbitrary arities in formal ZFC set theory, allowing also for higher levels of abstraction (e.g. arbitrary sequemces of functions, sequences of the sequences etc.). References are also good answers.
The formulations are needed to construct elementary mathematical objects such as the set of functions under function composition e.g. "all functions $f,h_i,g$ from naturals to naturals such that $f=g(h_1,...,h_n)$". A other example would be sentences of the form "There exists a primitive recursive function such that: $f(x_1,...,x_n)=g(x_1,..,x_n)$". Note that $x_1,...,x_n$ are not variables, but an object of the language, since such a sentence would be infinite.
I quickly present the standard theory from an axiomatic set theory class. First, ordered pair can be defined using Kuratowski's definition:
$$(a,b):= \{\{a\},{} \{a,b\}\}$$
A function is then simply a collection of pairs, where the first element of each gives the argument, the last giving the output. The operation is routinely definable in set theory,
One way to continue to higher arities is simply to define the higher arities as pairs of pairs, then a function of two arguments for example is given by a collection of elements of the form:
$$((a,b),c)$$
Continuing with the same principles, functions from naturals to naturals can be defined by first inductively defining $\mathbb N \times \mathbb N...$ using the pairs, and adding a condition that only functions are included. However, adding the condition or even in general working with this definition seems challenging. Defining a function that extracts ith argument of the pairs or arity of a function has not been presented. Does this approach work at all?
What seems to be a better approach is to define sequences of natural numbers for example as $\{(a_1,0),(a_2,1),...,(a_n,n-1)\}$. Now the arity can be easily defined as max of the right element of the pairs. A function then is a collection of sets $(a,b)$, where $a$ is a sequence of some arity (for multiple outputs, $b$ could also be a sequence). Now defining all functions from naturals to naturals and continuing with the abstraction seems much simpler than using the pairs.
Usually finite-arity functions are indeed presented in the "$\langle ...\langle\cdot,\cdot\rangle,\cdot\rangle, ...\rangle$" (iterated pairs) approach; the details are tedious, but not problematic, and make a good exercise.
However, this is a bad way of doing things, and not just because of simplicity concerns: rather, we often care about functions of infinite arity, and that doesn't really fit into the "iterated pairs" approach.
The second approach you mention is indeed the one we want. Writing "$A^B$" for the set of (unary) functions from $B$ to $A$, we say:
This reduces everything to the unary case, even for infinite arities - it even (in the absence of choice) makes sense for functions whose arity isn't well-orderable!
Note that this is just a special case of Cartesian products over arbitrary sets:
For $(X_i)_{i\in I}$ an indexed family of sets, we let $$\prod_{i\in I}X_i$$ be the set of functions $f$ from $I$ to $\bigcup_{i\in I}X_i$ satisfying $$f(i)\in X_i.$$
An $I$-ary function on $X$ is then just a function from $\prod_{i\in I}X$ to $X$ (that is, we take $X_i=X$ for each $i\in I$).